Anna Ingólfsdóttir

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.

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.

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.

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.

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

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.

I&C Journal 2003 Journal Article

A semantic theory for value-passing processes based on the late approach

• Anna Ingólfsdóttir

A general class of languages for value-passing calculi based on the late semantic approach is defined and a concrete instantiation of the general syntax is given. This is a modification of the standard CCS according to the late approach. Three kinds of semantics are given for this language. First a Plotkin style operational semantics by means of an applicative labelled transition system is introduced. This is a modification of the standard labelled transition system that caters for value-passing according to the late approach. As an abstraction, late bisimulation preorder is given. Then a general class of denotational models for the late semantics is defined. A denotational model for the concrete language is given as an instantiation of the general class. Two equationally based proof systems are defined. The first one, which is value-finitary, i. e. only reasons about a finite number of values at each time, is shown to be sound and complete with respect to this model. The second proof system, a value-infinitary one, is shown to be sound with respect to the model, whereas the completeness is proven later. The operational and the denotational semantics are compared and it is shown that the bisimulation preorder is finer than the preorder induced by the denotational model. We also show that in general the ω-bisimulation preorder is strictly included in the model induced preorder. Finally a value-finitary version of the bisimulation preorder is defined and the full abstractness of the denotational model with respect to it is shown. It is also shown that for CCS L the ω-bisimulation preorder coincides with the preorder induced by the model. From this we can conclude that if we allow for parameterized recursion in our language, we may express processes which coincide in any algebraic domain but are distinguished by the ω-bisimulation. This shows that if we extend CCS L in this way we obtain a strictly more expressive language.

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.

I&C Journal 2001 Journal Article

A Domain Equation for Bisimulation

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

TCS Journal 2001 Journal Article

A fully abstract denotational model for observational precongruence

• Anna Ingólfsdóttir
• Andrea Schalk

A domain theoretic denotational model is given for a simple sublanguage of CCS extended with divergence operator. The model is derived as an abstraction on a suitable notion of normal forms for labelled transition systems. It is shown to be fully abstract with respect to observational precongruence.

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).

CSL Conference 1997 Conference Paper

Weak Semantics Based on Lighted Button Pressing Experiments

• Anna Ingólfsdóttir

Abstract Imposing certain restrictions on the transition system that defines the behaviour of a process allows us to characterize the readiness semantics of [OH86] by means of black-box testing experiments, or more precisely by lighted button testing experiments [BM92]. As divergence is considered we give the semantics as a preorder, the readiness preorder, which kernel coincides with the readiness equivalence of [OH86]. This leads to a bisimulation like characterization and a modal characterization of the semantics. A concrete language, recursive free CCS without τ, is introduced, a proof system defined and it is shown to be sound and complete with respect to the readiness preorder. In the completeness proof the modal characterization plays an important role as it allows us to prove algebraicity of the preorder purely operationally. Foundation.

CSL Conference 1996 Conference Paper

A Fully Abstract Denotational Model for Observational Precongruence

• Anna Ingólfsdóttir
• Andrea Schalk

Abstract A domain theoretic denotational model is given for a simple sublanguage of CCS extended with divergence operator. The model is derived as an abstraction on a suitable notion of normal forms for labelled transition systems. It is shown to be fully abstract with respect to observational precongruence.

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

Late and early semantics coincide for testing

• Anna Ingólfsdóttir

Late and early operational semantics are given for CCS. Late and early testing are defined and it is shown that the derived preorders coincide, contrary to what happens for bisimulation-like equivalences.