We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:

References & Citations

DBLP - CS Bibliography


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: The Image of the Process Interpretation of Regular Expressions is Not Closed under Bisimulation Collapse

Abstract: Axiomatization and expressibility problems for Milner's process semantics (1984) of regular expressions modulo bisimilarity have turned out to be difficult for the full class of expressions with deadlock 0 and empty step~1. We report on a phenomenon that arises from the added presence of 1 when 0 is available, and that brings a crucial reason for this difficulty into focus. To wit, while interpretations of 1-free regular expressions are closed under bisimulation collapse, this is not the case for the interpretations of arbitrary regular expressions.
Process graph interpretations of 1-free regular expressions satisfy the loop existence and elimination property LEE, which is preserved under bisimulation collapse. These features of LEE were applied for showing that an equational proof system for 1-free regular expressions modulo bisimilarity is complete, and that it is decidable in polynomial time whether a process graph is bisimilar to the interpretation of a 1-free regular expression.
While interpretations of regular expressions do not satisfy the property LEE in general, we show that LEE can be recovered by refined interpretations as graphs with 1-transitions refined interpretations with 1-transitions (which are similar to silent steps for automata). This suggests that LEE can be expedient also for the general axiomatization and expressibility problems. But a new phenomenon emerges that needs to be addressed: the property of a process graph `to can be refined into a process graph with 1-transitions and with LEE' is not preserved under bisimulation collapse. We provide a 10-vertex graph with two 1-transitions that satisfies LEE, and in which a pair of bisimilar vertices cannot be collapsed on to each other while preserving the refinement property. This implies that the image of the process interpretation of regular expressions is not closed under bisimulation collapse.
Comments: Report (14 pages, 9 pages appendix) written for a submission in January 2021 (now slightly adapted, with added explanation of the relation with subsequent work that was published earlier) concerning the crucial observation underlying the crystallization process described in arXiv:2209.12188
Subjects: Logic in Computer Science (cs.LO); Computation and Language (cs.CL)
ACM classes: F.4.1
Cite as: arXiv:2303.08553 [cs.LO]
  (or arXiv:2303.08553v1 [cs.LO] for this version)

Submission history

From: Clemens Grabmayer [view email]
[v1] Wed, 15 Mar 2023 12:13:30 GMT (248kb)

Link back to: arXiv, form interface, contact.