Author name cluster

Bas Luttik

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

15 papers

2 author rows

TCS Journal 2025 Journal Article

Axiomatising weak bisimulation congruences over CCS with left merge and communication merge

Luca Aceto
Valentina Castiglioni
Anna Ingólfsdóttir
Bas Luttik

Classic weak bisimulation-based congruences are not finitely axiomatisable over (the recursion, relabelling, and restriction free fragment of) CCS. Motivated by these negative results, this paper studies the role of auxiliary operators in the finite equational characterisation of CCS parallel composition modulo those congruences. Firstly, we consider CCS with interleaving and left merge. We provide finite equational bases for this language modulo branching, η, delay, and weak bisimulation congruence. In particular, the completeness proofs for η, delay, and weak bisimulation congruence are obtained by reduction to the completeness result for branching bisimulation congruence. Then we extend the language with full merge and communication merge. In this case we provide an equational basis modulo branching bisimulation congruence under the assumption that the set of action names is infinite.

Details DOI

TCS Journal 2025 Journal Article

Non finite axiomatisability of weak bisimulation-based congruences

Luca Aceto
Valentina Castiglioni
Anna Ingólfsdóttir
Bas Luttik

We study the axiomatisability of CCS parallel composition operator modulo weak bisimulation-based congruences. Specifically, we prove that all congruences that are coarser than rooted branching bisimilarity, and finer than rooted weak bisimilarity, do not admit a finite equational axiomatisation over the recursion, restriction, and relabelling free fragment of CCS.

Details DOI

CSL Conference 2021 Conference Paper

Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?

Luca Aceto
Valentina Castiglioni
Wan J. Fokkink
Anna Ingólfsdóttir
Bas Luttik

Bergstra and Klop have shown that bisimilarity has a finite equational axiomatisation over ACP/CCS extended with the binary left and communication merge operators. Moller proved that auxiliary operators are necessary to obtain a finite axiomatisation of bisimilarity over CCS, and Aceto et al. showed that this remains true when Hennessy’s merge is added to that language. These results raise the question of whether there is one auxiliary binary operator whose addition to CCS leads to a finite axiomatisation of bisimilarity. This study provides a negative answer to that question based on three reasonable assumptions.

Details

TCS Journal 2020 Journal Article

On the axiomatisability of priority III: Priority strikes again

Luca Aceto
Elli Anastasiadi
Valentina Castiglioni
Anna Ingólfsdóttir
Bas Luttik
Mathias Ruggaard Pedersen

Aceto et al. , proved that, over the process algebra BCCSP with the priority operator of Baeten, Bergstra and Klop, the equational theory of order-insensitive bisimilarity is not finitely based. However, it was noticed that by substituting the action prefixing operator of BCCSP with BPA's sequential composition, the infinite family of equations used to show that non-finite axiomatisability result could be proved by a finite collection of sound equations. That observation left as an open question the existence of a finite axiomatisation for order-insensitive bisimilarity over BPA with the priority operator. In this paper we provide a negative answer to this question. We prove that, in the presence of at least two actions, order-insensitive bisimilarity is not finitely based over BPA with priority.

Details DOI

I&C Journal 2019 Journal Article

Divide and congruence III: From decomposition of modal formulas to preservation of stability and divergence

Wan Fokkink
Rob van Glabbeek
Bas Luttik

In two earlier papers we derived congruence formats with regard to transition system specifications for weak semantics on the basis of a decomposition method for modal formulas. The idea is that a congruence format for a semantics must ensure that the formulas in the modal characterisation of this semantics are always decomposed into formulas that are again in this modal characterisation. The stability and divergence requirements that are imposed on many of the known weak semantics have so far been outside the realm of this method. Stability refers to the absence of a τ-transition. We show, using the decomposition method, how congruence formats can be relaxed for weak semantics that are stability-respecting. This relaxation for instance brings the priority operator within the range of the stability-respecting branching bisimulation format. Divergence, which refers to the presence of an infinite sequence of τ-transitions, escapes the inductive decomposition method. We circumvent this problem by proving that a congruence format for a stability-respecting weak semantics is also a congruence format for its divergence-preserving counterpart.

Details DOI

TCS Journal 2016 Journal Article

Unique parallel decomposition in branching and weak bisimulation semantics

Bas Luttik

We consider the property of unique parallel decomposition modulo branching and weak bisimilarity. First, we show that normed behaviours always have parallel decompositions, but that these are not necessarily unique. Then, we establish that finite behaviours have unique parallel decompositions. We derive the latter result from a general theorem about unique decompositions in partial commutative monoids.

Details DOI

CSL Conference 2015 Conference Paper

Evidence for Fixpoint Logic

Sjoerd Cranen
Bas Luttik
Tim A. C. Willemse

For many modal logics, dedicated model checkers offer diagnostics (e. g. , counterexamples) that help the user understand the result provided by the solver. Fixpoint logic offers a unifying framework in which such problems can be expressed and solved, but a drawback of this framework is that it lacks comprehensive diagnostics generation. We extend the framework with a notion of evidence, which can be specialized to obtain diagnostics for various model checking problems, behavioural equivalence and refinement checking problems. We demonstrate this by showing how our notion of evidence can be used to obtain diagnostics for the problem of deciding stuttering bisimilarity. Moreover, we show that our notion generalizes the existing notions of counterexample and witness for LTL and ACTL* model checking.

Details

I&C Journal 2013 Journal Article

Reactive Turing machines

Jos C.M. Baeten
Bas Luttik
Paul van Tilburg

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.

Details DOI

TCS Journal 2011 Journal Article

On the axiomatizability of priority II

Luca Aceto
Taolue Chen
Anna Ingolfsdottir
Bas Luttik
Jaco van de Pol

This paper contributes to the study of the equational theory of the priority operator of Baeten, Bergstra and Klop in the setting of the process algebra BCCSP. It is shown that, in the presence of at least two actions, the collection of process equations over BCCSP with the priority operator that are valid modulo bisimilarity, irrespective of the chosen priority order over actions, is not finitely based. This holds true even if one restricts oneself to the collection of valid process equations that do not contain occurrences of process variables.

Details DOI

TCS Journal 2011 Journal Article

Unguardedness mostly means many solutions

Jos C.M. Baeten
Bas Luttik

A widely accepted method to specify (possibly infinite) behaviour is to define it as the solution, in some process algebra, of a recursive specification, i. e. , a system of recursive equations over the fundamental operations of the process algebra. The method only works if the recursive specification has a unique solution in the process algebra; it is well-known that guardedness is a sufficient requirement on a recursive specification to guarantee a unique solution in any of the standard process algebras. In this paper we investigate to what extent guardedness is also a necessary requirement to ensure unique solutions. We prove a theorem to the effect that all unguarded recursive specifications over BPA have infinitely many solutions in the standard models for BPA. In contrast, we observe that there exist recursive specifications over PA, necessarily involving parallel composition, that have a unique solution, or finitely many solutions in the standard models for PA.

Details DOI

I&C Journal 2008 Journal Article

On finite alphabets and infinite bases

Taolue Chen
Wan Fokkink
Bas Luttik
Sumit Nain

Van Glabbeek presented the linear time–branching time spectrum of behavioral semantics. He studied these semantics in the setting of the basic process algebra BCCSP, and gave finite, sound and ground-complete, axiomatizations for most of these semantics. Groote proved for some of van Glabbeek’s axiomatizations that they are ω -complete, meaning that an equation can be derived if (and only if) all of its closed instantiations can be derived. In this paper, we settle the remaining open questions for all the semantics in the linear time–branching time spectrum, either positively by giving a finite sound and ground-complete axiomatization that is ω -complete, or negatively by proving that such a finite basis for the equational theory does not exist. We prove that in case of a finite alphabet with at least two actions, failure semantics affords a finite basis, while for ready simulation, completed simulation, simulation, possible worlds, ready trace, failure trace and ready semantics, such a finite basis does not exist. Completed simulation semantics also lacks a finite basis in case of an infinite alphabet of actions.

Details DOI

TCS Journal 2005 Journal Article

CCS with Hennessy's merge has no finite-equational axiomatization

Luca Aceto
Wan Fokkink
Anna Ingólfsdóttir
Bas Luttik

This paper confirms a conjecture of Bergstra and Klop's from 1984 by establishing that the process algebra obtained by adding an auxiliary operator proposed by Hennessy in 1981 to the recursion free fragment of Milner's Calculus of Communicating Systems is not finitely based modulo bisimulation equivalence. Thus, Hennessy's merge cannot replace the left merge and communication merge operators proposed by Bergstra and Klop, at least if a finite axiomatization of parallel composition modulo bisimulation equivalence is desired.

Details DOI

TCS Journal 2005 Journal Article

Decomposition orders—another generalisation of the fundamental theorem of arithmetic

Bas Luttik
Vincent van Oostrom

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 ACP ɛ 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.

Details DOI

I&C Journal 2004 Journal Article

Remarks on Thatte’s transformation of term rewriting systems

Bas Luttik
Piet Rodenburg
Rakesh Verma

We carry out a detailed analysis of Thatte’s transformation of term rewriting systems. We refute an earlier claim that this transformation preserves confluence for weakly persistent systems. We prove the preservation of weak normalization, and of confluence in weakly normalizing systems and in nonoverlapping systems with linear subtemplates. We conclude by proving that weak persistence is an undecidable property of term rewriting systems.

Details DOI

MFCS Conference 2003 Conference Paper

A Unique Decomposition Theorem for Ordered Monoids with Applications in Process Theory

Bas Luttik

Abstract We prove a unique decomposition theorem for a class of ordered commutative monoids. Then, we use our theorem to establish that every weakly normed process definable in \({\mathsf{ACP}{}^{{\mathalpha{\varepsilon}}}}\) with bounded communication can be expressed as the parallel composition of a multiset of weakly normed parallel prime processes in exactly one way.

Details