Search

• < Previous
• 1
• Next >

---

Computation Tree Logic with Deadlock Detection

Rob van Glabbeek ; Bas Luttik ; Nikola Trcka.

We study the equivalence relation on states of labelled transition systems of satisfying the same formulas in Computation Tree Logic without the next state modality (CTL-X). This relation is obtained by De Nicola & Vaandrager by translating labelled transition systems to Kripke structures, while&nbsp;[&hellip;]

---

Split-2 Bisimilarity has a Finite Axiomatization over CCS with Hennessy&#39;s Merge

Luca Aceto ; Wan Fokkink ; Anna Ingolfsdottir ; Bas Luttik.

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&nbsp;[&hellip;]

---

Rooted Divergence-Preserving Branching Bisimilarity is a Congruence

Rob van Glabbeek ; Bas Luttik ; Linda Spaninks.

We prove that rooted divergence-preserving branching bisimilarity is a congruence for the process specification language consisting of nil, action prefix, choice, and the recursion construct.

---

The $\pi$-Calculus is Behaviourally Complete and Orbit-Finitely Executable

Bas Luttik ; Fei Yang.

Reactive Turing machines extend classical Turing machines with a facility to model observable interactive behaviour. We call a behaviour (finitely) executable if, and only if, it is equivalent to the behaviour of a (finite) reactive Turing machine. In this paper, we study the relationship between&nbsp;[&hellip;]

---

On the Axiomatisability of Parallel Composition

Luca Aceto ; Valentina Castiglioni ; Anna Ingolfsdottir ; Bas Luttik ; Mathias R. Pedersen.

This paper studies the existence of finite equational axiomatisations of the interleaving parallel composition operator modulo the behavioural equivalences in van Glabbeek's linear time-branching time spectrum. In the setting of the process algebra BCCSP over a finite set of actions, we provide&nbsp;[&hellip;]

---

Equivalence checking for weak bi-Kleene algebra

Tobias Kappé ; Paul Brunet ; Bas Luttik ; Alexandra Silva ; Fabio Zanasi.

Pomset automata are an operational model of weak bi-Kleene algebra, which describes programs that can fork an execution into parallel threads, upon completion of which execution can join to resume as a single thread. We characterize a fragment of pomset automata that admits a decision procedure for&nbsp;[&hellip;]

---

Pushdown Automata and Context-Free Grammars in Bisimulation Semantics

Jos C. M. Baeten ; Cesare Carissimo ; Bas Luttik.

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&nbsp;[&hellip;]

---