Search

Communication with value passing has received ample attention in process theory. Value passing through a sequential composition has received much less attention. In recent work, we found that sequential value passing is the essential ingredient to prove the analogue of the classical theorem of the equivalence of pushdown automata and context-free grammars in a setting of interactive processes and bisimulation. Subsequently, we found that the treatment of sequential value passing in the process setting can be simplified considerably. We report on this simplification here, and find another application of sequential value passing, viz. a Kleene theorem for processes.

A classical theorem states that the set of languages given by a pushdown automaton coincides with the set of languages given by a context-free grammar. In previous work, we proved the pendant of this theorem in a setting with interaction: the set of processes given by a pushdown automaton coincides with the set of processes given by a finite guarded recursive specification over a process algebra with actions, choice, sequencing and guarded recursion, if and only if we add sequential value passing. In this paper, we look what happens if we consider parallel pushdown automata instead of pushdown automata, and a process algebra with parallelism instead of sequencing.

The Turing machine models an old-fashioned computer, that does not interact with the user or with other computers, and only does batch processing. Therefore, we came up with a Reactive Turing Machine that does not have these shortcomings. In the Reactive Turing Machine, transitions have labels to give a notion of interactivity. In the resulting process graph, we use bisimilarity instead of language equivalence. Subsequently, we considered other classical theorems and notions from automata theory and formal languages theory. In this paper, we consider the classical theorem of the correspondence between pushdown automata and context-free grammars. By changing the process operator of sequential composition to a sequencing operator with intermediate acceptance, we get a better correspondence in our setting. We find that the missing ingredient to recover the full correspondence is the addition of a notion of state awareness.

The Turing machine models an old-fashioned computer, that does not interact with the user or with other computers, and only does batch processing. Therefore, we came up with a Reactive Turing Machine that does not have these shortcomings. In the Reactive Turing Machine, transitions have labels to give a notion of interactivity. In the resulting process graph, we use bisimilarity instead of language equivalence. Subsequently, we considered other classical theorems and notions from automata theory and formal languages theory. In this paper, we consider the classical theorem of the correspondence between pushdown automata and context-free grammars. By changing the process operator of sequential composition to a sequencing operator with intermediate acceptance, we get a better correspondence in our setting. We find that the missing ingredient to recover the full correspondence is the addition of a notion of state awareness.

The Theory of Sequential Processes includes deadlock, successful termination, action prefixing, alternative and sequential composition. Intermediate acceptance, which is important for the integration of classical automata theory, can be expressed through a combination of alternative composition and successful termination. Recently, it was argued that complications arising from the interplay between intermediate acceptance and sequential composition can be eliminated by replacing sequential composition by sequencing. In this paper we study the equational theory of the recursion-free fragment of the resulting process theory modulo bisimilarity, proving that it is not finitely based, but does afford a ground-complete axiomatisation if a unary auxiliary operator is added. Furthermore, we prove that bisimilarity is decidable for processes definable by means of a finite guarded recursive specification over the process theo

The standard operational semantics of the sequential composition operator gives rise to unbounded branching and forgetfulness when transparent process expressions are put in sequence. Due to transparency, the correspondence between context-free and pushdown processes fails modulo bisimilarity, and it is not clear how to specify an always terminating half counter. We propose a revised operational semantics for the sequential composition operator in the context of intermediate termination. With the revised operational semantics, we eliminate transparency, allowing us to establish a close correspondence between context-free processes and pushdown processes. Moreover,we prove the reactive Turing powerfulness of TCP with iteration and nesting with the revised operational semantics for sequential composition.

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 modulo bisimilarity. Then, we prove that replacing the operation for pure interleaving by ACP-style parallel composition gives a furth

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 modulo bisimilarity. Then, we prove that replacing the operation for pure interleaving by ACP-style parallel composition gives a further increase in expressiveness, still insufficient, however, to facilitate the expression of all finite automata up to bisimilarity. Finally, we prove that the theory of regular expressions with ACP-style parallel composition and encapsulation is expressive enough to express all finite automata up to bisimilarity. Our results extend the expressiveness results obtained by Bergstra, Bethke and Ponse for process algebras with (the binary variant of) Kleene’s star operation.

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 by a single RTM. We prove that there exist universal RTMs modulo branching bisimilarity, but these essentially employ divergence to be able to simulate an RTM of arbitrary branching degree. We also prove that modulo divergence-preserving branching bisimilarity there are RTMs that are universal up to their own branching degree. We establish a correspondence between executability and finite definability in a simple process calculus. Finally, we establish that RTMs are at least as expressive as persistent Turing machines.

We enhance the notion of a computation of the classical theory of computing with the notion of interaction from concurrency theory. In this way, we enhance a Turing machine as a model of computation to a Reactive Turing Machine that is an abstract model of a computer as it is used nowadays, always interacting with the user and the world.

We describe a translation of a subset of executable UML (xUML) into the process algebraic specification language mCRL2. This subset includes class diagrams with class generalisations, and state machines with signal and change events. The choice of these xUML constructs is dictated by their use in the modelling of railway interlocking systems. The long-term goal is to verify safety properties of interlockings modelled in xUML using the mCRL2 and LTSmin toolsets. Initial verification of an interlocking toy example demonstrates that the safety properties of model instances depend crucially on the run-to-completion assumptions.

The language χ is a modeling and simulation language which is currently mainly used to analyse and optimize the performance of industrial systems. To be able to also verify functional properties of a system using a χ model, part of the language has been given a formal semantics. Rather than implementing a new model checker for χ, the philosophy is to provide automatic translations from χ into the specification languages of existing state-of-the-art model checkers such as, e.g., spin and uppaal. In this paper, we propose for χ a notion of stuttering congruence, which is an adaptation of the notion of stuttering equivalence. We prove that our notion preserves the validity of ctl∗–× formulas, that it preserves deadlock, and that it is indeed a congruence with respect to the constructs of χ. We also indicate how our notion is to be used to establish confidence in the correctness of a translation from χ into promela

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 same authors to the effect that the same language is not finitely based modulo bisimulation equivalence.

We discuss unique decomposition in partial commutative monoids. Inspired by a result from process theory, we propose the notion of decomposition order for partial commutative monoids, and prove that a partial commutative monoid has unique decomposition iff it can be endowed with a decomposition order. We apply our result to establish that the commutative monoid of weakly normed processes modulo bisimulation definable in ACPe with linear communication, with parallel composition as binary operation, has unique decomposition. We also apply our result to establish that the partial commutative monoid associated with a well-founded commutative residual algebra has unique decomposition

We consider the process theory $PA$ that includes an operation for parallel composition, based on the interleaving paradigm. We prove that the standard set of axioms of $PA$ is not $omega$-complete by providing a set of axioms that are valid in $PA$, but not derivable from the standard ones. We prove that extending $PA$ with this set yields an $omega$-complete specification, which is finite in a setting with finitely many actions.

Groote and Luttik (1998a) proved that the extension of the theory pCRL with the axioms for branching bisimulation of Van Glabbeek and Weijland (1996) yields a ground complete axiomatisation of branching bisimulation algebras with data, and conditionals and alternative quantification over these, provided that the data part has built-in equality and built-in Skolem functions. In this paper we shall use this result to obtain ground complete axiomatisations of $eta$-bisimulation algebras, delay bisimulation algebras and weak bisimulation algebras with data, conditionals and alternative quantification over data, under the same proviso as before. Groote and Luttik (1998a) proved that the extension of the theory pCRL with the axioms for branching bisimulation of Van Glabbeek and Weijland (1996) yields a ground complete axiomatisation of branching bisimulation algebras with data, and conditionals and alternative quantification over these, provided that the data part has built-in equality and built-in Skolem functions. In this paper we shall use this result to obtain ground complete axiomatisations of $eta$-bisimulation algebras, delay bisimulation algebras and weak bisimulation algebras with data, conditionals and alternative quantification over data, under the same proviso as before.

Theories that are designed to reason about processes and the information they exchange usually also include a construction to quantify over this information. We mention the input prefix mechanism of, e.g., the $pi$-calculus and the operation $gsum{$ for alternative quantification over data of mcrl. These constructions are implemented as binders, and hence imply a relatively complicated notion of substitution that takes the binding of these operations into account. As a consequence, the defining axioms of such constructions are not suitable for purely equational reasoning, or, to put it differently, proof systems for process theories that contain binders are not algebraic. In this paper, we shall define the variety of cylindric process algebras with conditionals, and we prove that, for data with built-in equality and built-in Skolem functions, it is an algebraic semantics of a subsystem of mcrl{. Thus we obtain a proof system for a class of process algebras with data and alternative quantification from which the complicated notion of substitution is eliminated.

We define a class of process algebras with silent step and a generalised operation $gsum{$ that allows explicit treatment of emph{alternative quantification over data, and we investigate the specific subclass formed by the algebras of finite processes modulo rooted branching bisimulation. We give a ground complete axiomatisation for those branching bisimulation algebras of which the data part has built-in equality and Skolem functions.

We define a class of process algebras with a generalised operation $sum$ that allows explicit treatment of emph{alternative quantification over data, and investigate the specific subclass formed by the algebras of finite processes modulo strong bisimulation. We prove that, in such algebras, equality between process terms is definable by means of a first-order data formula, and that, if the data is computable and has a built-in equality predicate, any $Pi^0_4$ data formula is definable as an equation between ground process terms. From these results we work to the conclusion that equality in strong bisimulation algebras with a computable data part is $Pi^0_4$-hard. We also investigate a restricted version of alternative quantification: the input prefix mechanism of Parrow and Sangiorgi (1995) and Hennessy and Lin (1996). We show that this restriction yields a less expressive formalism if the data is computable and has a built-in equality predicate: equality between input prefix processes coincides with the universal fragment of first-order logic for the data. That is, the input prefix mechanism gives rise to strong bisimulation algebras for which equality is complete in $Pi^0_1$. Finally, we give a ground complete axiomatisation for those strong bisimulation algebras of which the data part has built-in equality and Skolem functions.

We give a formal specification in $mu$CRL of the Link Layer as described in the IEEE document ``P1394 Standard for a High Performance Serial Bus''; this specification may serve as a starting point for further verification.