arXiv subjects

Anna Ingolfsdottir

Publications and source records attributed to Anna Ingolfsdottir.

18 recordsLinked to original sources

arXiv2025

Deciding characteristic formulae: A journey in the branching-time spectrum

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 (co)NP- or PSPACE-complete.

cs.LO↗

arXiv2024

The complexity of deciding characteristic formulae in van Glabbeek's branching-time spectrum

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 finite, loop-free 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 consistent and prime ones, it 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.

cs.LO↗

arXiv2023

Bidirectional Runtime Enforcement of First-Order Branching-Time Properties

Runtime enforcement is a dynamic analysis technique that instruments a monitor with a system in order to ensure its correctness as specified by some property. This paper explores bidirectional enforcement strategies for properties describing the input and output behaviour of a system. We develop an operational framework for bidirectional enforcement and use it to study the enforceability of the safety fragment of Hennessy-Milner logic with recursion (sHML). We provide an automated synthesis function that generates correct monitors from sHML formulas, and show that this logic is enforceable via a specific type of bidirectional enforcement monitors called action disabling monitors.

cs.LO↗

arXiv2022

Complexity through Translations for Modal Logic with Recursion

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.

cs.LO↗

arXiv2022

On the Axiomatisation of Branching Bisimulation Congruence over CCS

In this paper we investigate the equational theory of (the restriction, relabelling, and recursion free fragment of) CCS modulo rooted branching bisimilarity, which is a classic, bisimulation-based notion of equivalence that abstracts from internal computational steps in process behaviour. Firstly, we show that CCS is not finitely based modulo the considered congruence. As a key step of independent interest in the proof of that negative result, we prove that each CCS process has a unique parallel decomposition into indecomposable processes modulo branching bisimilarity. As a second main contribution, we show that, when the set of actions is finite, rooted branching bisimilarity has a finite equational basis over CCS enriched with the left merge and communication merge operators from ACP.

cs.LO↗

arXiv2022

Axiomatizing recursion-free, regular monitors

Monitors are a key tool in the field of runtime verification, where they are used to verify system properties by analyzing execution traces generated by processes. Work on runtime monitoring carried out in a series of papers by Aceto et al.$~$has specified monitors using a variation on the regular fragment of Milner's CCS and studied two trace-based notions of equivalence over monitors, namely verdict and $ω$-verdict equivalence. This article is devoted to the study of the equational logic of monitors modulo those two notions of equivalence. It presents complete equational axiomatizations of verdict and $ω$-verdict equivalence for closed and open terms over recursion-free monitors. It is also shown that verdict equivalence has no finite equational axiomatization over open monitors when the set of actions is finite and contains at least two actions.

cs.LO↗

arXiv2022

On the Axiomatisability of Parallel Composition

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 finite, ground-complete axiomatisations for various simulation and (decorated) trace semantics. We also show that no congruence over BCCSP that includes bisimilarity and is included in possible futures equivalence has a finite, ground-complete axiomatisation; this negative result applies to all the nested trace and nested simulation semantics.

cs.LO↗

arXiv2021

In search of lost time: Axiomatising parallel composition in process algebras

This survey reviews some of the most recent achievements in the saga of the axiomatisation of parallel composition, along with some classic results. We focus on the recursion, relabelling and restriction free fragment of CCS and we discuss the solutions to three problems that were open for many years. The first problem concerns the status of Bergstra and Klop's auxiliary operators left merge and communication merge in the finite axiomatisation of parallel composition modulo bisimiliarity: We argue that, under some natural assumptions, the addition of a single auxiliary binary operator to CCS does not yield a finite axiomatisation of bisimilarity. Then we delineate the boundary between finite and non-finite axiomatisability of the congruences in van Glabbeek's linear time-branching time spectrum over CCS. Finally, we present a novel result to the effect that rooted weak bisimilarity has no finite complete axiomatisation over CCS.

cs.LO↗

arXiv2018

Developing Theoretical Foundations for Runtime Enforcement

The ubiquitous reliance on software systems increases the need for ensuring that systems behave correctly and are well protected against security risks. Runtime enforcement is a dynamic analysis technique that utilizes software monitors to check the runtime behaviour of a software system with respect to a correctness specification. Whenever the runtime behaviour of the monitored system is about to deviate from the specification (either due to a programming bug or a security hijack attack), the monitors apply enforcement techniques to prevent this deviation. Current Runtime Enforcement techniques require that the correctness specification defines the behaviour of the enforcement monitor itself. This burdens the specifier with not only having to define property that needs to be enforced, but also with having to specify how this should be enforced at runtime; we thus relieve the specifier from this burden by resorting to a highly expressive logic. Using a logic we allow the specifier to define the correctness specification as a logic formula from which we can automatically synthesise the appropriate enforcement monitor. Highly expressive logics can, however, permit for defining a wide variety of formulae, some of which cannot actually be enforced correctly at runtime. We thus study the enforceability of Hennessy Milner Logic with Recursion for which we identify a subset that allows for defining enforceable formulae. This allows us to define a synthesis function that translates enforceable formulae into enforcement monitors. As our monitors are meant to ensure the correct behaviour of the monitored system, it is imperative that they work correctly themselves. We thus study formal definitions that allow us to ensure that our enforcement monitors behave correctly.

cs.LO↗

arXiv2018

On Runtime Enforcement via Suppressions

Runtime enforcement is a dynamic analysis technique that uses monitors to enforce the behaviour specified by some correctness property on an executing system. The enforceability of a logic captures the extent to which the properties expressible via the logic can be enforced at runtime. We study the enforceability of Hennessy-Milner Logic with Recursion (muHML) with respect to suppression enforcement. We develop an operational framework for enforcement which we then use to formalise when a monitor enforces a muHML property. We also show that the safety syntactic fragment of the logic, sHML, is enforceable by providing an automated synthesis function that generates correct suppression monitors from sHML formulas.

cs.LO↗

arXiv2016

Proceedings First Workshop on Pre- and Post-Deployment Verification Techniques

The PrePost (Pre- and Post-Deployment Verification Techniques) workshop aimed at bringing together researchers working in the field of computer-aided validation and verification to discuss the connections and interplay between pre- and post-deployment verification techniques. Examples of the topics covered by the workshop are the relationships between classic model checking and testing on the one hand and runtime verification and statistical model checking on the other, and between type systems that may be checked either statically or dynamically through techniques such as runtime monitoring.

cs.LO↗

arXiv2013

Meta SOS - A Maude Based SOS Meta-Theory Framework

Meta SOS is a software framework designed to integrate the results from the meta-theory of structural operational semantics (SOS). These results include deriving semantic properties of language constructs just by syntactically analyzing their rule-based definition, as well as automatically deriving sound and ground-complete axiomatizations for languages, when considering a notion of behavioural equivalence. This paper describes the Meta SOS framework by blending aspects from the meta-theory of SOS, details on their implementation in Maude, and running examples.

cs.LO↗

arXiv2011

Axiomatizing GSOS with Predicates

In this paper, we introduce an extension of the GSOS rule format with predicates such as termination, convergence and divergence. For this format we generalize the technique proposed by Aceto, Bloom and Vaandrager for the automatic generation of ground-complete axiomatizations of bisimilarity over GSOS systems. Our procedure is implemented in a tool that receives SOS specifications as input and derives the corresponding axiomatizations automatically. This paves the way to checking strong bisimilarity over process terms by means of theorem-proving techniques.

cs.LO↗

arXiv2011

Modelling and Simulation of Asynchronous Real-Time Systems using Timed Rebeca

In this paper we propose an extension of the Rebeca language that can be used to model distributed and asynchronous systems with timing constraints. We provide the formal semantics of the language using Structural Operational Semantics, and show its expressiveness by means of examples. We developed a tool for automated translation from timed Rebeca to the Erlang language, which provides a first implementation of timed Rebeca. We can use the tool to set the parameters of timed Rebeca models, which represent the environment and component variables, and use McErlang to run multiple simulations for different settings. Timed Rebeca restricts the modeller to a pure asynchronous actor-based paradigm, where the structure of the model represents the service oriented architecture, while the computational model matches the network infrastructure. Simulation is shown to be an effective analysis support, specially where model checking faces almost immediate state explosion in an asynchronous setting.

cs.SE↗

arXiv2010

A Bisimulation-based Method for Proving the Validity of Equations in GSOS Languages

This paper presents a bisimulation-based method for establishing the soundness of equations between terms constructed using operations whose semantics is specified by rules in the GSOS format of Bloom, Istrail and Meyer. The method is inspired by de Simone's FH-bisimilarity and uses transition rules as schematic transitions in a bisimulation-like relation between open terms. The soundness of the method is proven and examples showing its applicability are provided. The proposed bisimulation-based proof method is incomplete, but the article offers some completeness results for restricted classes of GSOS specifications.

cs.LO↗

arXiv2009

Characteristic Formulae for Fixed-Point Semantics: A General Framework

The literature on concurrency theory offers a wealth of examples of characteristic-formula constructions for various behavioural relations over finite labelled transition systems and Kripke structures that are defined in terms of fixed points of suitable functions. Such constructions and their proofs of correctness have been developed independently, but have a common underlying structure. This study provides a general view of characteristic formulae that are expressed in terms of logics with a facility for the recursive definition of formulae. It is shown how several examples of characteristic-formula constructions from the literature can be recovered as instances of the proposed general framework, and how the framework can be used to yield novel constructions.

cs.LO↗

arXiv2006

A Finite Equational Base for CCS with Left Merge and Communication Merge

Using the left merge and communication merge from ACP, we present an equational base (i.e., a ground-complete and $ω$-complete set of valid equations) for the fragment of CCS without recursion, restriction and relabelling. Our equational base is finite if the set of actions is finite.

cs.LO↗

arXiv2005

Split-2 Bisimilarity has a Finite Axiomatization over CCS with Hennessy's Merge

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.

cs.LO↗