Robin Milner (1984) gave a sound proof system for bisimilarity of regular expressions interpreted as processes: Basic Process Algebra with unary Kleene star iteration, deadlock 0, successful termination 1, and a fixed-point rule. He asked whether this system is complete. Despite intensive research over the last 35 years, the problem is still open.
This paper gives a partial positive answer to Milner's problem. We prove that the adaptation of Milner's system over the subclass of regular expressions that arises by dropping the constant 1, and by changing to binary Kleene star iteration is complete. The crucial tool we use is a graph structure property that guarantees expressibility of a process graph by a regular expression, and is preserved by going over from a process graph to its bisimulation collapse.
We prove that the bisimulation-invariant fragment of weak monadic second-order logic (WMSO) is equivalent to the fragment of the modal $μ$-calculus where the application of the least fixpoint operator $μp.φ$ is restricted to formulas $φ$ that are continuous in $p$. Our proof is automata-theoretic in nature; in particular, we introduce a class of automata characterizing the expressive power of WMSO over tree models of arbitrary branching degree. The transition map of these automata is defined in terms of a logic $\mathrm{FOE}_1^\infty$ that is the extension of first-order logic with a generaliz…
The languages accepted by finite automata are precisely the languages denoted by regular expressions. In contrast, finite automata may exhibit behaviours that cannot be described by regular expressions up to bisimilarity. In this paper, we consider extensions of the theory of regular expressions with various forms of parallel composition and study the effect on expressiveness. First we prove that adding pure interleaving to the theory of regular expressions strictly increases its expressiveness up to bisimilarity. Then, we prove that replacing the operation for pure interleaving by ACP-style p…
In this paper we investigate the equational theory of (the restriction, relabelling, and recursion free fragment of) CCS modulo rooted branching bisimilarity, which is a classic, bisimulation-based notion of equivalence that abstracts from internal computational steps in process behaviour. Firstly, we show that CCS is not finitely based modulo the considered congruence. As a key step of independent interest in the proof of that negative result, we prove that each CCS process has a unique parallel decomposition into indecomposable processes modulo branching bisimilarity. As a second main contri…
This note shows that split-2 bisimulation equivalence (also known as timed equivalence) affords a finite equational axiomatization over the process algebra obtained by adding an auxiliary operation proposed by Hennessy in 1981 to the recursion, relabelling and restriction free fragment of Milner's Calculus of Communicating Systems. Thus the addition of a single binary operation, viz. Hennessy's merge, is sufficient for the finite equational axiomatization of parallel composition modulo this non-interleaving equivalence. This result is in sharp contrast to a theorem previously obtained by the s…
A landmark result in the study of logics for formal verification is Janin & Walukiewicz's theorem, stating that the modal $μ$-calculus ($μ\mathrm{ML}$) is equivalent modulo bisimilarity to standard monadic second-order logic (here abbreviated as $\mathrm{smso}$), over the class of labelled transition systems (LTSs for short). Our work proves two results of the same kind, one for the alternation-free fragment of $μ\mathrm{ML}$ ($μ_D\mathrm{ML}$) and one for weak $\mathrm{mso}$ ($\mathrm{wmso}$). Whereas it was known that $μ_D\mathrm{ML}$ and $\mathrm{wmso}$ are equivalent modulo bisimilarity on…
We propose reactive Turing machines (RTMs), extending classical Turing machines with a process-theoretical notion of interaction, and use it to define a notion of executable transition system. We show that every computable transition system with a bounded branching degree is simulated modulo divergence-preserving branching bisimilarity by an RTM, and that every effective transition system is simulated modulo the variant of branching bisimilarity that does not require divergence preservation. We conclude from these results that the parallel composition of (communicating) RTMs can be simulated b…
Milner (1984) defined a process semantics for regular expressions. He formulated a sound proof system for bisimilarity of process interpretations of regular expressions, and asked whether this system is complete. We report conceptually on a proof that shows that Milner's system is complete, by motivating, illustrating, and describing all of its main steps. We substantially refine the completeness proof by Grabmayer and Fokkink (2020) for the restriction of Milner's system to `1-free' regular expressions. As a crucial complication we recognize that process graphs with empty-step transitions tha…
By adapting Salomaa's complete proof system for equality of regular expressions under the language semantics, Milner (1984) formulated a sound proof system for bisimilarity of regular expressions under the process interpretation he introduced. He asked whether this system is complete. Proof-theoretic arguments attempting to show completeness of this equational system are complicated by the presence of a non-algebraic rule for solving fixed-point equations by using star iteration. We characterize the derivational power that the fixed-point rule adds to the purely equational part $\text{Mil$^{\b…
A (fragment of a) process algebra satisfies unique parallel decomposition if the definable behaviours admit a unique decomposition into indecomposable parallel components. In this paper we prove that finite processes of the pi-calculus, i.e. processes that perform no infinite executions, satisfy this property modulo strong bisimilarity and weak bisimilarity. Our results are obtained by an application of a general technique for establishing unique parallel decomposition using decomposition orders.
Branching bisimilarity on normed Basic Process Algebra (BPA) was claimed to be EXPTIME-hard in previous papers without any explicit proof. Recently it is reminded by Jančar that the claim is not so dependable. In this paper, we develop a new complete proof for EXPTIME-hardness of branching bisimilarity on normed BPA. We also prove the associate regularity problem on normed BPA is PSPACE-hard and in EXPTIME. This improves previous P-hard and NEXPTIME result.
Burkart, Caucal, Steffen (1995) showed a procedure deciding bisimulation equivalence of processes in Basic Process Algebra (BPA), i.e. of sequential processes generated by context-free grammars. They improved the previous decidability result of Christensen, Hüttel, Stirling (1992), since their procedure has obviously an elementary time complexity and the authors claim that a close analysis would reveal a double exponential upper bound. Here a self-contained direct proof of the membership in 2-ExpTime is given. This is done via a Prover-Refuter game which shows that there is an alternating Turi…
We develop a (co)algebraic framework to study a family of process calculi with monadic branching structures and recursion operators. Our framework features a uniform semantics of process terms and a complete axiomatisation of semantic equivalence. We show that there are uniformly defined fragments of our calculi that capture well-known examples from the literature like regular expressions modulo bisimilarity and guarded Kleene algebra with tests. We also derive new calculi for probabilistic and convex processes with an analogue of Kleene star.
Milner (1984) introduced a process semantics for regular expressions as process graphs. Unlike for the language semantics, where every regular (that is, DFA-accepted) language is the interpretation of some regular expression, there are finite process graphs that are not bisimilar to the process interpretation of any regular expression. For reasoning about graphs that are expressible by regular expressions modulo bisimilarity it is desirable to have structural representations of process graphs in the image of the interpretation. For `1-free' regular expressions, their process interpretations sa…
An open problem posed by Milner asks for a proof that a certain axiomatisation, which Milner showed is sound with respect to bisimilarity for regular expressions, is also complete. One of the main difficulties of the problem is the lack of a full Kleene theorem, since there are automata that can not be specified, up to bisimilarity, by an expression. Grabmayer and Fokkink (2020) characterise those automata that can be expressed by regular expressions without the constant 1, and use this characterisation to give a positive answer to Milner's question for this subset of expressions. In this pape…
Milner (1984) introduced a process semantics for regular expressions as process graphs. Unlike for the language semantics, where every regular (that is, DFA-accepted) language is the interpretation of some regular expression, there are finite process graphs that are not bisimilar to the process interpretation of any regular expression. For reasoning about graphs that are expressible by regular expressions modulo bisimilarity it is desirable to have structural representations of process graphs in the image of the interpretation. For '1-free' regular expressions, their process interpretations sa…
Monitors are a key tool in the field of runtime verification, where they are used to verify system properties by analyzing execution traces generated by processes. Work on runtime monitoring carried out in a series of papers by Aceto et al.$~$has specified monitors using a variation on the regular fragment of Milner's CCS and studied two trace-based notions of equivalence over monitors, namely verdict and $ω$-verdict equivalence. This article is devoted to the study of the equational logic of monitors modulo those two notions of equivalence. It presents complete equational axiomatizations of v…
We show that the axioms of Weak Kleene Algebra (WKA) are sound and complete for the theory of regular expressions modulo simulation equivalence, assuming their completeness for monodic trees (as conjectured by Takai and Furusawa).
