Luca Aceto

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.

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.

CSL Conference 2025 Conference Paper

The Complexity of Deciding Characteristic Formulae in Van Glabbeek's Branching-Time Spectrum

• Luca Aceto
• Antonis Achilleos
• Aggeliki Chalki
• Anna Ingólfsdóttir

Characteristic formulae give a complete logical description of the behaviour of processes modulo some chosen notion of behavioural semantics. They allow one to reduce equivalence or preorder checking to model checking, and are exactly the formulae in the modal logics characterizing classic behavioural equivalences and preorders for which model checking can be reduced to equivalence or preorder checking. This paper studies the complexity of determining whether a formula is characteristic for some process in each of the logics providing modal characterizations of the simulation-based semantics in van Glabbeek’s branching-time spectrum. Since characteristic formulae in each of those logics are exactly the satisfiable and prime ones, this article presents complexity results for the satisfiability and primality problems, and investigates the boundary between modal logics for which those problems can be solved in polynomial time and those for which they become computationally hard. Amongst other contributions, this article also studies the complexity of constructing characteristic formulae in the modal logics characterizing simulation-based semantics, both when such formulae are presented in explicit form and via systems of equations.

GandALF Workshop 2025 Workshop Paper

The Complexity of Deciding Characteristic Formulae Modulo Nested Simulation (extended abstract)

• Luca Aceto
• Antonis Achilleos
• Aggeliki Chalki
• Anna Ingólfsdóttir

This paper studies the complexity of determining whether a formula in the modal logics characterizing the nested-simulation semantics is characteristic for some process, which is equivalent to determining whether the formula is satisfiable and prime. The main results are that the problem of determining whether a formula is prime in the modal logic characterizing the 2-nested-simulation preorder is coNP-complete and is PSPACE-complete in the case of the n-nested-simulation preorder, when n>=3. This establishes that deciding characteristic formulae for the n-nested simulation semantics is PSPACE-complete, when n>=3. In the case of the 2-nested simulation semantics, that problem lies in the complexity class DP, which consists of languages that can be expressed as the intersection of one language in NP and of one in coNP.

GandALF Workshop 2022 Workshop Paper

Complexity through Translations for Modal Logic with Recursion

• Luca Aceto
• Antonis Achilleos
• Elli Anastasiadi
• Adrian Francalanza
• Anna Ingolfsdottir

This paper studies the complexity of classical modal logics and of their extension with fixed-point operators, using translations to transfer results across logics. In particular, we show several complexity results for multi-agent logics via translations to and from the mu-calculus and modal logic, which allow us to transfer known upper and lower bounds. We also use these translations to introduce a terminating tableau system for the logics we study, based on Kozen's tableau for the mu-calculus, and the one of Fitting and Massacci for modal logic.

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.

CSL Conference 2021 Conference Paper

The Best a Monitor Can Do

• Luca Aceto
• Antonis Achilleos
• Adrian Francalanza
• Anna Ingólfsdóttir
• Karoliina Lehtinen

Existing notions of monitorability for branching-time properties are fairly restrictive. This, in turn, impacts the ability to incorporate prior knowledge about the system under scrutiny - which corresponds to a branching-time property - into the runtime analysis. We propose a definition of optimal monitors that verify the best monitorable under- or over-approximation of a specification, regardless of its monitorability status. Optimal monitors can be obtained for arbitrary branching-time properties by synthesising a sound and complete monitor for their strongest monitorable consequence. We show that the strongest monitorable consequence of specifications expressed in Hennessy-Milner logic with recursion is itself expressible in this logic, and present a procedure to find it. Our procedure enables prior knowledge to be optimally incorporated into runtime monitors.

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.

TCS Journal 2019 Journal Article

When are prime formulae characteristic?

• Luca Aceto
• Dario Della Monica
• Ignacio Fábregas
• Anna Ingólfsdóttir

In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed that the formulae for which model checking can be reduced to preorder checking, that is, the characteristic formulae, are exactly the consistent and prime ones. This paper presents general, sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones. It is shown that the given conditions apply to various behavioural relations in the literature. In particular, characteristic formulae are exactly the prime and consistent ones for all the semantics in van Glabbeek's linear time-branching time spectrum.

TCS Journal 2014 Journal Article

Axiomatizing weak simulation semantics over BCCSP

• Luca Aceto
• David de Frutos Escrig
• Carlos Gregorio-Rodríguez
• Anna Ingolfsdottir

This paper is devoted to the study of the (in)equational theory of the largest (pre)congruences over the language BCCSP induced by variations on the classic simulation preorder and equivalence that abstract from internal steps in process behaviours. In particular, the article focuses on the (pre)congruences associated with the weak simulation, the weak complete simulation and the weak ready simulation preorders. We present results on the (non)existence of finite (ground-)complete (in)equational axiomatizations for each of these behavioural semantics. The axiomatization of those semantics using conditional equations is also discussed in some detail.

JELIA Conference 2014 Conference Paper

On the Expressiveness of the Interval Logic of Allen's Relations Over Finite and Discrete Linear Orders

• Luca Aceto
• Dario Della Monica
• Anna Ingólfsdóttir
• Angelo Montanari
• Guido Sciavicco

Abstract Interval temporal logics take time intervals, instead of time instants, as their primitive temporal entities. One of the most studied interval temporal logics is Halpern and Shoham’s modal logic of time intervals HS, which associates a modal operator with each binary relation between intervals over a linear order (the so-called Allen’s interval relations). A complete classification of all HS fragments with respect to their relative expressive power has been recently given for the classes of all linear orders and of all dense linear orders. The cases of discrete and finite linear orders turn out to be much more involved. In this paper, we make a significant step towards solving the classification problem over those classes of linear orders. First, we illustrate various non-trivial temporal properties that can be expressed by HS fragments when interpreted over finite and discrete linear orders; then, we provide a complete set of definabilities for the HS modalities corresponding to the Allen’s relations meets, later, begins, finishes, and during, as well as the ones corresponding to their inverse relations. The only missing cases are those of the relations overlaps and overlapped by.

I&C Journal 2013 Journal Article

38th International Colloquium on Automata, Languages and Programming

• Luca Aceto
• Monika Henzinger
• Jiří Sgall

TIME Conference 2013 Conference Paper

A Complete Classification of the Expressiveness of Interval Logics of Allen's Relations over Dense Linear Orders

• Luca Aceto
• Dario Della Monica
• Anna Ingólfsdóttir
• Angelo Montanari
• Guido Sciavicco

Interval temporal logics are temporal logics that take time intervals, instead of time instants, as their primitive temporal entities. One of the most studied interval temporal logics is Halpern and Shoham's modal logic of time intervals (HS), which has a distinct modality for each binary relation between intervals over a linear order. As HS turns out to be undecidable over most classes of linear orders, the study of HS fragments, featuring a proper subset of HS modalities, is a major item in the research agenda for interval temporal logics. A characterization of HS fragments in terms of their relative expressive power has been given for the class of all linear orders. Unfortunately, there is no easy way to directly transfer such a result to other meaningful classes of linear orders. In this paper, we provide a complete classification of the expressiveness of HS fragments over the class of (all) dense linear orders.

LPAR Conference 2013 Conference Paper

An Algorithm for Enumerating Maximal Models of Horn Theories with an Application to Modal Logics

• Luca Aceto
• Dario Della Monica
• Anna Ingólfsdóttir
• Angelo Montanari
• Guido Sciavicco

Abstract The fragment of propositional logic known as Horn theories plays a central role in automated reasoning. The problem of enumerating the maximal models of a Horn theory ( MaxMod ) has been proved to be computationally hard, unless P = NP. To the best of our knowledge, the only algorithm available for it is the one based on a brute-force approach. In this paper, we provide an algorithm for the problem of enumerating the maximal subsets of facts that do not entail a distinguished atomic proposition in a definite Horn theory ( MaxNoEntail ). We show that MaxMod is polynomially reducible to MaxNoEntail (and vice versa), making it possible to solve also the former problem using the proposed algorithm. Addressing MaxMod via MaxNoEntail opens, inter alia, the possibility of benefiting from the monotonicity of the notion of entailment. (The notion of model does not enjoy such a property.) We also discuss an application of MaxNoEntail to expressiveness issues for modal logics, which reveals the effectiveness of the proposed algorithm.

TCS Journal 2012 Journal Article

Rule formats for distributivity

• Luca Aceto
• Matteo Cimini
• Anna Ingolfsdottir
• MohammadReza Mousavi
• Michel A. Reniers

This paper proposes rule formats for Structural Operational Semantics guaranteeing that certain binary operators are left distributive with respect to a set of binary operators. Examples of left-distributivity laws from the literature are shown to be instances of the provided formats. Some conditions ensuring the invalidity of the left-distributivity law are also offered.

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.

TARK Conference 2011 Conference Paper

Sigma algebras in probabilistic epistemic dynamics

• Luca Aceto
• Wiebe van der Hoek
• Anna Ingólfsdóttir
• Joshua Sack

This paper extends probabilistic dynamic epistemic logic from a finite setting to an infinite setting, by introducing σ-algebras to the probability spaces in the models. This may extend the applicability of the logic to a real world setting with infinitely many possible measurements. It is shown that the dynamics preserves desirable properties of measurability and that completeness of the proof system holds with the extended semantics.

TCS Journal 2011 Journal Article

SOS rule formats for zero and unit elements

• Luca Aceto
• Matteo Cimini
• Anna Ingolfsdottir
• MohammadReza Mousavi
• Michel A. Reniers

This paper proposes rule formats for Structural Operational Semantics guaranteeing that certain constants act as left or right unit/zero elements for a set of binary operators. Examples of left and right zero, as well as unit, elements from the literature are shown to fit the rule formats offered in this study.

TCS Journal 2006 Journal Article

Bisimilarity is not finitely based over BPA with interrupt

• Luca Aceto
• Wan Fokkink
• Anna Ingolfsdottir
• Sumit Nain

This paper shows that bisimulation equivalence does not afford a finite equational axiomatization over the language obtained by enriching Bergstra and Klop's basic process algebra (BPA) with the interrupt operator. Moreover, it is shown that the collection of closed equations over this language is also not finitely based. In sharp contrast to these results, the collection of closed equations over the language BPA enriched with the disrupt operator is proven to be finitely based.

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.

TCS Journal 2005 Journal Article

Guest editors’ foreword

• Luca Aceto
• Wan Fokkink
• Anna Ingolfsdottir
• Zoltán Ésik

I&C Journal 2004 Journal Article

Nested semantics over finite trees are equationally hard

• Luca Aceto
• Wan Fokkink
• Rob van Glabbeek
• Anna Ingólfsdóttir

This paper studies nested simulation and nested trace semantics over the language BCCSP, a basic formalism to express finite process behaviour. It is shown that none of these semantics affords finite (in)equational axiomatizations over BCCSP. In particular, for each of the nested semantics studied in this paper, the collection of sound, closed (in)equations over a singleton action set is not finitely based.

TCS Journal 2003 Journal Article

Equational theories of tropical semirings

• Luca Aceto
• Zoltán Ésik
• Anna Ingólfsdóttir

This paper studies the equational theories of various exotic semirings presented in the literature. Exotic semirings are semirings whose underlying carrier set is some subset of the set of real numbers equipped with binary operations of minimum or maximum as sum, and addition as product. Two prime examples of such structures are the (max, +) semiring and the tropical semiring. It is shown that none of the exotic semirings commonly considered in the literature has a finite basis for its equations, and that similar results hold for the commutative idempotent weak semirings that underlie them. For each of these commutative idempotent weak semirings, the paper offers characterizations of the equations that hold in them, decidability results for their equational theories, explicit descriptions of the free algebras in the varieties they generate, and relative axiomatization results.

TCS Journal 2003 Journal Article

The max-plus algebra of the natural numbers has no finite equational basis

• Luca Aceto
• Zoltán Ésik
• Anna Ingólfsdóttir

This paper shows that the collection of identities which hold in the algebra N of the natural numbers with constant zero, and binary operations of sum and maximum is not finitely based. Moreover, it is proven that, for every n, the equations in at most n variables that hold in N do not form an equational basis. As a stepping stone in the proof of these facts, several results of independent interest are obtained. In particular, explicit descriptions of the free algebras in the variety generated by N are offered. Such descriptions are based upon a geometric characterization of the equations that hold in N, which also yields that the equational theory of N is decidable in exponential time.

TCS Journal 2003 Journal Article

The power of reachability testing for timed automata

• Luca Aceto
• Patricia Bouyer
• Augusto Burgueño
• Kim G Larsen

The computational engine of the verification tool UPPAAL consists of a collection of efficient algorithms for the analysis of reachability properties of systems. Model-checking of properties other than plain reachability ones may currently be carried out in such a tool as follows. Given a property φ to model-check, the user must provide a test automaton T φ for it. This test automaton must be such that the original system S has the property expressed by φ precisely when none of the distinguished reject states of T φ can be reached in the synchronized parallel composition of S with T φ. This raises the question of which properties may be analysed by Uppaal in such a way. This paper gives an answer to this question by providing a complete characterization of the class of properties for which model-checking can be reduced to reachability testing in the sense outlined above. This result is obtained as a corollary of a stronger statement pertaining to the compositionality of the property language considered in this study. In particular, it is shown that our language is the least expressive compositional language that can express a simple safety property stating that no reject state can ever be reached. Finally, the property language characterizing the power of reachability testing is used to provide a definition of characteristic properties with respect to a timed version of the ready simulation preorder, for nodes of τ-free, deterministic timed automata.

I&C Journal 2001 Journal Article

A Domain Equation for Bisimulation

• Samson Abramsky
• Luca Aceto
• Anna Ingólfsdóttir

TCS Journal 1999 Journal Article

A complete equational axiomatization for MPA with string iteration

• Luca Aceto
• Jan Friso Groote

We study equational axiomatizations of bisimulation equivalence for the language obtained by extending Milner's basic CCS with string iteration. String iteration is a variation on the original binary version of the Kleene star operation p∗q obtained by restricting the first argument to be a non-empty sequence of atomic actions. We show that, for every positive integer k, bisimulation equivalence over the set of processes in this language with loops of length at most k is finitely axiomatizable, provided that the set of actions is finite. We also offer an infinite equational theory that completely axiomatizes bisimulation equivalence over the whole language. We prove that this result cannot be improved upon by showing that no finite equational axiomatization of bisimulation equivalence over basic CCS with string iteration can exist, unless the set of actions is empty.

MFCS Conference 1999 Conference Paper

Is Your Model Checker on Time? On the Complexity of Model Checking for Timed Modal Logics

• Luca Aceto
• François Laroussinie

Abstract This paper studies the structural complexity of model checking for (variations on) the specification formalisms used in the tools CMC and Uppaal, and fragments of a timed alternation-free μ -calculus. For each of the logics we study, we characterize the computational complexity of model checking, as well as its specification and program complexity, using timed automata as our system model.

TCS Journal 1998 Journal Article

On a question of A. Salomaa the equational theory of regular expressions over a singleton alphabet is not finitely based

• Luca Aceto
• Wan Fokkink
• Anna Ingólfsdóttir

Salomaa (1969, p. 143) asked whether the equational theory of regular expressions over a singleton alphabet has a finite equational base. In this paper, we provide a negative answer to this long-standing question. The proof of our main result rests upon a model-theoretic argument. For every finite collection of equations, that are sound in the algebra of regular expressions over a singleton alphabet, we build a model in which some valid regular equation fails. The construction of the model mimics the one used by Conway (1971, p. 105) in his proof of a result, originally due to Redko, to the effect that infinitely many equations are needed to axiomatize equality of regular expressions. Our analysis of the model, however, needs to be more refined than the one provided by Conway (1971).

I&C Journal 1997 Journal Article

An Equational Axiomatization for Multi-exit Iteration

• Luca Aceto
• Wan Fokkink

This paper presents an equational axiomatization of bisimulation equivalence over the language of Basic Process Algebra (BPA) with multi-exit iteration. Multi-exit iteration is a generalization of the standard binary Kleene star operation that allows for the specification of agents that, up to bisimulation equivalence, are solutions of systems of recursion equations of the formX1 = def P1X2+Q1 ⋮Xn = def PnX1+Qn, wherenis a positive integer and thePi and theQi are process terms. The addition of multi-exit iteration to BPA yields a more expressive language than that obtained by augmenting BPA with the standard binary Kleene star (BPA*). As a consequence, the proof of completeness of the proposed equational axiomatization for this language, although standard in its general structure, is much more involved than that for BPA*. An expressiveness hierarchy for the family ofk-exit iteration operators proposed by Bergstra, Bethke, and Ponse is also offered.

I&C Journal 1996 Journal Article

Axiomatizing Prefix Iteration with Silent Steps

• Luca Aceto
• Rob van Glabbeek
• Wan Fokkink
• Anna Ingólfsdóttir

Prefix iteration is a variation on the original binary version of the Kleene star operationP*Q, obtained by restricting the first argument to be an atomic action. The interaction of prefix iteration with silent steps is studied in the setting of Milner's basic CCS. Complete equational axiomatizations are given for four notions of behavioural congruence over basic CCS with prefix iteration, viz. , branching congruence, η-congruence, delay congruence, and weak congruence. The completeness proofs forη-, delay, and weak congruence are obtained by reduction to the completeness theorem for branching congruence. It is also argued that the use of the completeness result for branching congruence in obtaining the completeness result for weak congruence leads to a considerable simplification with respect to the only direct proof presented in the literature. The preliminaries and the completeness proofs focus on open terms, i. e. , terms that may contain process variables. As a by-product, theω-completeness of the axiomatizations is obtained, as well as their completeness for closed terms.

I&C Journal 1996 Journal Article

CPO Models for Compact GSOS Languages

• Luca Aceto
• Anna Ingólfsdóttir

In this paper, we present a general way of giving denotational semantics to a class of languages equipped with an operational semantics that fits the GSOS format of Bloom, Istrail, and Meyer. The canonical model used for this purpose will be Abramsky's domain of synchronization trees, and the denotational semantics automatically generated by our methods will be guaranteed to be fully abstract with respect to the finitely observable part of the bisimulation preorder. In the process of establishing the full abstraction result, we also obtain several general results on the bisimulation preorder (including a complete axiomatization for it), and give a novel operational interpretation of GSOS languages.

TCS Journal 1995 Journal Article

A complete axiomatization of timed bisimulation for a class of timed regular behaviours

• Luca Aceto
• Alan Jeffrey

One of the most satisfactory results in process theory is Milner's axiomatization of strong bisimulation for regular CCS. This result holds for open terms with finite-state recursion. Wang has shown that timed bisimulation can also be axiomatized, but only for closed terms without recursion. In this paper, we provide an axiomatization for timed bisimulation of open terms with finite-state recursion.

TCS Journal 1994 Journal Article

GSOS and finite labelled transition systems

• Luca Aceto

Recently there has been considerable interest in studying formats of Plotkin style inference rules which ensure that the induced labelled transition system semantics have certain properties. In this note, I shall give a contribution to this line of research by giving a restricted version of Bloom, Istrail and Meyer's GSOS format Bloom et al. (1988), Bloom (1989) which induces finite labelled transition systems.