-
Runtime Instrumentation for Reactive Components (Extended Version)
Authors:
Luca Aceto,
Duncan Paul Attard,
Adrian Francalanza,
Anna Ingólfsdóttir
Abstract:
Reactive software calls for instrumentation methods that uphold the reactive attributes of systems. Runtime verification imposes another demand on the instrumentation, namely that the trace event sequences it reports to monitors are sound -- that is, they reflect actual executions of the system under scrutiny. This paper presents RIARC, a novel decentralised instrumentation algorithm for outline m…
▽ More
Reactive software calls for instrumentation methods that uphold the reactive attributes of systems. Runtime verification imposes another demand on the instrumentation, namely that the trace event sequences it reports to monitors are sound -- that is, they reflect actual executions of the system under scrutiny. This paper presents RIARC, a novel decentralised instrumentation algorithm for outline monitors meeting these two demands. The asynchronous setting of reactive software complicates the instrumentation due to potential trace event loss or reordering. RIARC overcomes these challenges using a next-hop IP routing approach to rearrange and report events soundly to monitors.
RIARC is validated in two ways. We subject its corresponding implementation to rigorous systematic testing to confirm its correctness. In addition, we assess this implementation via extensive empirical experiments, subjecting it to large realistic workloads to ascertain its reactiveness. Our results show that RIARC optimises its memory and scheduler usage to maintain latency feasible for soft real-time applications. We also compare RIARC to inline and centralised monitoring, revealing that it induces comparable latency to inline monitoring in moderate concurrency settings, where software performs long-running, computationally-intensive tasks, such as in Big Data stream processing.
△ Less
Submitted 28 June, 2024;
originally announced June 2024.
-
The complexity of deciding characteristic formulae in van Glabbeek's branching-time spectrum
Authors:
Luca Aceto,
Antonis Achilleos,
Aggeliki Chalki,
Anna Ingolfsdottir
Abstract:
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 che…
▽ More
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.
△ Less
Submitted 22 May, 2024;
originally announced May 2024.
-
A unified rule format for bounded nondeterminism in SOS with terms as labels
Authors:
Luca Aceto,
Ignacio Fábregas,
Álvaro García-Pérez,
Anna Ingólfsdóttir
Abstract:
We present a unified rule format for structural operational semantics with terms as labels that guarantees that the associated labelled transition system has some bounded-nondeterminism property. The properties we consider include finite branching, initials finiteness and image finiteness.
We present a unified rule format for structural operational semantics with terms as labels that guarantees that the associated labelled transition system has some bounded-nondeterminism property. The properties we consider include finite branching, initials finiteness and image finiteness.
△ Less
Submitted 5 February, 2024;
originally announced February 2024.
-
Rule Formats for Nominal Process Calculi
Authors:
Luca Aceto,
Ignacio Fábregas,
Álvaro García-Pérez,
Anna Ingólfsdóttir,
Yolanda Ortega-Mallén
Abstract:
The nominal transition systems (NTSs) of Parrow et al. describe the operational semantics of nominal process calculi. We study NTSs in terms of the nominal residual transition systems (NRTSs) that we introduce. We provide rule formats for the specifications of NRTSs that ensure that the associated NRTS is an NTS and apply them to the operational specification of the early pi-calculus. Our study st…
▽ More
The nominal transition systems (NTSs) of Parrow et al. describe the operational semantics of nominal process calculi. We study NTSs in terms of the nominal residual transition systems (NRTSs) that we introduce. We provide rule formats for the specifications of NRTSs that ensure that the associated NRTS is an NTS and apply them to the operational specification of the early pi-calculus. Our study stems from the recent Nominal SOS of Cimini et al. and from earlier works in nominal sets and nominal logic by Gabbay, Pitts and their collaborators.
△ Less
Submitted 1 February, 2024;
originally announced February 2024.
-
Logical characterisations, rule formats and compositionality for input-output conformance simulation
Authors:
Luca Aceto,
Ignacio Fábregas,
Carlos Gregorio-Rodríguez,
Anna Ingólfsdóttir
Abstract:
Input-output conformance simulation (iocos) has been proposed by Gregorio-Rodríguez, Llana and Martínez-Torres as a simulation-based behavioural preorder underlying model-based testing. This relation is inspired by Tretmans' classic ioco relation, but has better worst-case complexity than ioco and supports stepwise refinement. The goal of this paper is to develop the theory of iocos by studying lo…
▽ More
Input-output conformance simulation (iocos) has been proposed by Gregorio-Rodríguez, Llana and Martínez-Torres as a simulation-based behavioural preorder underlying model-based testing. This relation is inspired by Tretmans' classic ioco relation, but has better worst-case complexity than ioco and supports stepwise refinement. The goal of this paper is to develop the theory of iocos by studying logical characterisations of this relation, rule formats for it and its compositionality. More specifically, this article presents characterisations of iocos in terms of modal logics and compares them with an existing logical characterisation for ioco proposed by Beohar and Mousavi. It also offers a characteristic-formula construction for iocos over finite processes in an extension of the proposed modal logics with greatest fixed points. A precongruence rule format for iocos and a rule format ensuring that operations take quiescence properly into account are also given. Both rule formats are based on the GSOS format by Bloom, Istrail and Meyer. The general modal decomposition methodology of Fokkink and van Glabbeek is used to show how to check the satisfaction of properties expressed in the logic for iocos in a compositional way for operations specified by rules in the precongruence rule format for iocos .
△ Less
Submitted 6 February, 2024; v1 submitted 1 February, 2024;
originally announced February 2024.
-
When Are Prime Formulae Characteristic?
Authors:
Luca Aceto,
Dario Della Monica,
Ignacio Fábregas,
Anna Ingólfsdóttir
Abstract:
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 cons…
▽ More
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.
△ Less
Submitted 6 February, 2024; v1 submitted 1 February, 2024;
originally announced February 2024.
-
On the specification of modal systems: A comparison of three frameworks
Authors:
Luca Aceto,
Ignacio Fábregas,
David de Frutos Escrig,
Anna Ingólfsdóttir,
Miguel Palomino
Abstract:
This paper studies the relationships between three notions of behavioural preorder that have been proposed in the literature: refinement over modal transition systems, and the covariant-contravariant simulation and the partial bisimulation preorders over labelled transition systems. It is shown that there are mutual translations between modal transition systems and labelled transition systems that…
▽ More
This paper studies the relationships between three notions of behavioural preorder that have been proposed in the literature: refinement over modal transition systems, and the covariant-contravariant simulation and the partial bisimulation preorders over labelled transition systems. It is shown that there are mutual translations between modal transition systems and labelled transition systems that preserve, and reflect, refinement and the covariant-contravariant simulation preorder. The translations are also shown to preserve the modal properties that can be expressed in the logics that characterize those preorders. A translation from labelled transition systems modulo the partial bisimulation preorder into the same model modulo the covariant-contravariant simulation preorder is also offered, together with some evidence that the former model is less expressive than the latter. In order to gain more insight into the relationships between modal transition systems modulo refinement and labelled transition systems modulo the covariant-contravariant simulation preorder, their connections are also phrased and studied in the context of institutions.
△ Less
Submitted 6 February, 2024; v1 submitted 1 February, 2024;
originally announced February 2024.
-
The Way We Were: Structural Operational Semantics Research in Perspective
Authors:
Luca Aceto,
Pierluigi Crescenzi,
Anna Ingólfsdóttir,
Mohammad Reza Mousavi
Abstract:
This position paper on the (meta-)theory of Structural Operational Semantic (SOS) is motivated by the following two questions: (1) Is the (meta-)theory of SOS dying out as a research field? (2) If so, is it possible to rejuvenate this field with a redefined purpose?
In this article, we will consider possible answers to those questions by first analysing the history of the EXPRESS/SOS workshops…
▽ More
This position paper on the (meta-)theory of Structural Operational Semantic (SOS) is motivated by the following two questions: (1) Is the (meta-)theory of SOS dying out as a research field? (2) If so, is it possible to rejuvenate this field with a redefined purpose?
In this article, we will consider possible answers to those questions by first analysing the history of the EXPRESS/SOS workshops and the data concerning the authors and the presentations featured in the editions of those workshops as well as their subject matters.
The results of our quantitative and qualitative analyses all indicate a diminishing interest in the theory of SOS as a field of research. Even though `all good things must come to an end', we strive to finish this position paper on an upbeat note by addressing our second motivating question with some optimism. To this end, we use our personal reflections and an analysis of recent trends in two of the flagship conferences in the field of Programming Languages (namely POPL and PDLI) to draw some conclusions on possible future directions that may rejuvenate research on the (meta-)theory of SOS. We hope that our musings will entice members of the research community to breathe new life into a field of research that has been kind to three of the authors of this article.
△ Less
Submitted 13 September, 2023;
originally announced September 2023.
-
Complexity results for modal logic with recursion via translations and tableaux
Authors:
Luca Aceto,
Antonis Achilleos,
Elli Anastasiadi,
Adrian Francalanza,
Anna Ingólfsdóttir
Abstract:
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 $μ$-calculus and modal logic, which allow us to transfer known upper and lower bounds. We also use these translations to introduc…
▽ More
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 $μ$-calculus and modal logic, which allow us to transfer known upper and lower bounds. We also use these translations to introduce terminating and non-terminating tableau systems for the logics we study, based on Kozen's tableau for the $μ$-calculus and the one of Fitting and Massacci for modal logic. Finally, we describe these tableaux with $μ$-calculus formulas, thus reducing the satisfiability of each of these logics to the satisfiability of the $μ$-calculus, resulting in a general 2EXP upper bound for satisfiability testing.
△ Less
Submitted 1 July, 2024; v1 submitted 29 June, 2023;
originally announced June 2023.
-
MM Algorithms to Estimate Parameters in Continuous-time Markov Chains
Authors:
Giovanni Bacci,
Anna Ingólfsdóttir,
Kim G. Larsen,
Raphaël Reynouard
Abstract:
Continuous-time Markov chains (CTMCs) are popular modeling formalism that constitutes the underlying semantics for real-time probabilistic systems such as queuing networks, stochastic process algebras, and calculi for systems biology. Prism and Storm are popular model checking tools that provide a number of powerful analysis techniques for CTMCs. These tools accept models expressed as the parallel…
▽ More
Continuous-time Markov chains (CTMCs) are popular modeling formalism that constitutes the underlying semantics for real-time probabilistic systems such as queuing networks, stochastic process algebras, and calculi for systems biology. Prism and Storm are popular model checking tools that provide a number of powerful analysis techniques for CTMCs. These tools accept models expressed as the parallel composition of a number of modules interacting with each other. The outcome of the analysis is strongly dependent on the parameter values used in the model which govern the timing and probability of events of the resulting CTMC. However, for some applications, parameter values have to be empirically estimated from partially-observable executions. In this work, we address the problem of estimating parameter values of CTMCs expressed as Prism models from a number of partially-observable executions. We introduce the class parametric CTMCs -- CTMCs where transition rates are polynomial functions over a set of parameters -- as an abstraction of CTMCs covering a large class of Prism models. Then, building on a theory of algorithms known by the initials MM, for minorization-maximization, we present iterative maximum likelihood estimation algorithms for parametric CTMCs covering two learning scenarios: when both state-labels and dwell times are observable, or just state-labels are. We conclude by illustrating the use of our technique in a simple but non-trivial case study: the analysis of the spread of COVID-19 in presence of lockdown countermeasures.
△ Less
Submitted 16 February, 2023;
originally announced February 2023.
-
Complexity through Translations for Modal Logic with Recursion
Authors:
Luca Aceto,
Antonis Achilleos,
Elli Anastasiadi,
Adrian Francalanza,
Anna Ingolfsdottir
Abstract:
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 introduc…
▽ More
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.
△ Less
Submitted 21 September, 2022;
originally announced September 2022.
-
On the Axiomatisation of Branching Bisimulation Congruence over CCS
Authors:
Luca Aceto,
Valentina Castiglioni,
Anna Ingolfsdottir,
Bas Luttik
Abstract:
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 independen…
▽ More
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.
△ Less
Submitted 28 June, 2022;
originally announced June 2022.
-
Bidirectional Runtime Enforcement of First-Order Branching-Time Properties
Authors:
Luca Aceto,
Ian Cassar,
Adrian Francalanza,
Anna Ingolfsdottir
Abstract:
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 sa…
▽ More
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.
△ Less
Submitted 27 February, 2023; v1 submitted 9 January, 2022;
originally announced January 2022.
-
Active Learning of Markov Decision Processes using Baum-Welch algorithm (Extended)
Authors:
Giovanni Bacci,
Anna Ingólfsdóttir,
Kim Larsen,
Raphaël Reynouard
Abstract:
Cyber-physical systems (CPSs) are naturally modelled as reactive systems with nondeterministic and probabilistic dynamics. Model-based verification techniques have proved effective in the deployment of safety-critical CPSs. Central for a successful application of such techniques is the construction of an accurate formal model for the system. Manual construction can be a resource-demanding and erro…
▽ More
Cyber-physical systems (CPSs) are naturally modelled as reactive systems with nondeterministic and probabilistic dynamics. Model-based verification techniques have proved effective in the deployment of safety-critical CPSs. Central for a successful application of such techniques is the construction of an accurate formal model for the system. Manual construction can be a resource-demanding and error-prone process, thus motivating the design of automata learning algorithms to synthesise a system model from observed system behaviours.
This paper revisits and adapts the classic Baum-Welch algorithm for learning Markov decision processes and Markov chains. For the case of MDPs, which typically demand more observations, we present a model-based active learning sampling strategy that choses examples which are most informative w.r.t.\ the current model hypothesis. We empirically compare our approach with state-of-the-art tools and demonstrate that the proposed active learning procedure can significantly reduce the number of observations required to obtain accurate models.
△ Less
Submitted 6 October, 2021;
originally announced October 2021.
-
In search of lost time: Axiomatising parallel composition in process algebras
Authors:
Luca Aceto,
Elli Anastasiadi,
Valentina Castiglioni,
Anna Ingolfsdottir,
Bas Luttik
Abstract:
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 c…
▽ More
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.
△ Less
Submitted 3 May, 2021;
originally announced May 2021.
-
A Choreographed Outline Instrumentation Algorithm for Asynchronous Components
Authors:
Luca Aceto,
Duncan Paul Attard,
Adrian Francalanza,
Anna Ingólfsdóttir
Abstract:
The runtime analysis of decentralised software requires instrumentation methods that are scalable, but also minimally invasive. This paper presents a new algorithm that instruments choreographed outline monitors. Our instrumentation algorithm scales and reorganises monitors dynamically as the system executes. We demonstrate the implementability of choreographed outline instrumentation and compare…
▽ More
The runtime analysis of decentralised software requires instrumentation methods that are scalable, but also minimally invasive. This paper presents a new algorithm that instruments choreographed outline monitors. Our instrumentation algorithm scales and reorganises monitors dynamically as the system executes. We demonstrate the implementability of choreographed outline instrumentation and compare it to inline instrumentation, subject to rigorous and comprehensive benchmarking. Our results debunk the general notion that outline monitoring is necessarily infeasible, and show that our implementation induces runtime overhead comparable to that of its inline counterpart for many practical cases.
△ Less
Submitted 19 April, 2021;
originally announced April 2021.
-
On the Axiomatisability of Parallel Composition
Authors:
Luca Aceto,
Valentina Castiglioni,
Anna Ingolfsdottir,
Bas Luttik,
Mathias R. Pedersen
Abstract:
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…
▽ More
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.
△ Less
Submitted 17 January, 2022; v1 submitted 22 February, 2021;
originally announced February 2021.
-
Axiomatizing recursion-free, regular monitors
Authors:
Luca Aceto,
Antonis Achilleos,
Elli Anastasiadi,
Anna Ingolfsdottir
Abstract:
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 ver…
▽ More
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.
△ Less
Submitted 10 May, 2022; v1 submitted 9 June, 2020;
originally announced June 2020.
-
An Operational Guide to Monitorability
Authors:
Luca Aceto,
Antonis Achilleos,
Adrian Francalanza,
Anna Ingólfsdóttir,
Karoliina Lehtinen
Abstract:
Monitorability delineates what properties can be verified at runtime. Although many monitorability definitions exist, few are defined explicitly in terms of the guarantees provided by monitors, i.e., the computational entities carrying out the verification. We view monitorability as a spectrum: the fewer monitor guarantees that are required, the more properties become monitorable. We present a mon…
▽ More
Monitorability delineates what properties can be verified at runtime. Although many monitorability definitions exist, few are defined explicitly in terms of the guarantees provided by monitors, i.e., the computational entities carrying out the verification. We view monitorability as a spectrum: the fewer monitor guarantees that are required, the more properties become monitorable. We present a monitorability hierarchy and provide operational and syntactic characterisations for its levels. Existing monitorability definitions are mapped into our hierarchy, providing a unified framework that makes the operational assumptions and guarantees of each definition explicit. This provides a rigorous foundation that can inform design choices and correctness claims for runtime verification tools.
△ Less
Submitted 3 June, 2019;
originally announced June 2019.
-
The Cost of Monitoring Alone
Authors:
Luca Aceto,
Antonis Achilleos,
Adrian Francalanza,
Anna Ingólfsdóttir,
Karoliina Lehtinen
Abstract:
We compare the succinctness of two monitoring systems for properties of infinite traces, namely parallel and regular monitors. Although a parallel monitor can be turned into an equivalent regular monitor, the cost of this transformation is a double-exponential blowup in the syntactic size of the monitors, and a triple-exponential blowup when the goal is a deterministic monitor. We show that these…
▽ More
We compare the succinctness of two monitoring systems for properties of infinite traces, namely parallel and regular monitors. Although a parallel monitor can be turned into an equivalent regular monitor, the cost of this transformation is a double-exponential blowup in the syntactic size of the monitors, and a triple-exponential blowup when the goal is a deterministic monitor. We show that these bounds are tight and that they also hold for translations between corresponding fragments of Hennessy-Milner logic with recursion over infinite traces.
△ Less
Submitted 13 February, 2019;
originally announced February 2019.
-
Adventures in Monitorability: From Branching to Linear Time and Back Again
Authors:
Luca Aceto,
Antonis Achilleos,
Adrian Francalanza,
Anna Ingólfsdóttir,
Karoliina Lehtinen
Abstract:
This paper establishes a comprehensive theory of runtime monitorability for Hennessy-Milner logic with recursion, a very expressive variant of the modal $μ$-calculus. It investigates the monitorability of that logic with a linear-time semantics and then compares the obtained results with ones that were previously presented in the literature for a branching-time setting. Our work establishes an exp…
▽ More
This paper establishes a comprehensive theory of runtime monitorability for Hennessy-Milner logic with recursion, a very expressive variant of the modal $μ$-calculus. It investigates the monitorability of that logic with a linear-time semantics and then compares the obtained results with ones that were previously presented in the literature for a branching-time setting. Our work establishes an expressiveness hierarchy of monitorable fragments of Hennessy-Milner logic with recursion in a linear-time setting and exactly identifies what kinds of guarantees can be given using runtime monitors for each fragment in the hierarchy. Each fragment is shown to be complete, in the sense that it can express all properties that can be monitored under the corresponding guarantees. The study is carried out using a principled approach to monitoring that connects the semantics of the logic and the operational semantics of monitors. The proposed framework supports the automatic, compositional synthesis of correct monitors from monitorable properties.
△ Less
Submitted 1 February, 2019;
originally announced February 2019.
-
Rule Formats for Nominal Process Calculi
Authors:
Luca Aceto,
Ignacio Fábregas,
Álvaro García-Pérez,
Anna Ingólfsdóttir,
Yolanda Ortega-Mallén
Abstract:
The nominal transition systems (NTSs) of Parrow et al. describe the operational semantics of nominal process calculi. We study NTSs in terms of the nominal residual transition systems (NRTSs) that we introduce. We provide rule formats for the specifications of NRTSs that ensure that the associated NRTS is an NTS and apply them to the operational specifications of the early and late pi-calculus. We…
▽ More
The nominal transition systems (NTSs) of Parrow et al. describe the operational semantics of nominal process calculi. We study NTSs in terms of the nominal residual transition systems (NRTSs) that we introduce. We provide rule formats for the specifications of NRTSs that ensure that the associated NRTS is an NTS and apply them to the operational specifications of the early and late pi-calculus. We also explore alternative specifications of the NTSs in which we allow residuals of abstraction sort, and introduce translations between the systems with and without residuals of abstraction sort. Our study stems from the Nominal SOS of Cimini et al. and from earlier works in nominal sets and nominal logic by Gabbay, Pitts and their collaborators.
△ Less
Submitted 11 October, 2019; v1 submitted 5 July, 2018;
originally announced July 2018.
-
On Runtime Enforcement via Suppressions
Authors:
Luca Aceto,
Ian Cassar,
Adrian Francalanza,
Anna Ingolfsdottir
Abstract:
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 enforceme…
▽ More
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.
△ Less
Submitted 3 July, 2018;
originally announced July 2018.
-
Develo** Theoretical Foundations for Runtime Enforcement
Authors:
Ian Cassar,
Adrian Francalanza,
Luca Aceto,
Anna Ingolfsdottir
Abstract:
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…
▽ More
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.
△ Less
Submitted 12 November, 2018; v1 submitted 24 April, 2018;
originally announced April 2018.
-
A Survey of Runtime Monitoring Instrumentation Techniques
Authors:
Ian Cassar,
Adrian Francalanza,
Luca Aceto,
Anna Ingólfsdóttir
Abstract:
Runtime Monitoring is a lightweight and dynamic verification technique that involves observing the internal operations of a software system and/or its interactions with other external entities, with the aim of determining whether the system satisfies or violates a correctness specification. Compilation techniques employed in Runtime Monitoring tools allow monitors to be automatically derived from…
▽ More
Runtime Monitoring is a lightweight and dynamic verification technique that involves observing the internal operations of a software system and/or its interactions with other external entities, with the aim of determining whether the system satisfies or violates a correctness specification. Compilation techniques employed in Runtime Monitoring tools allow monitors to be automatically derived from high-level correctness specifications (aka. properties). This allows the same property to be converted into different types of monitors, which may apply different instrumentation techniques for checking whether the property was satisfied or not. In this paper we compare and contrast the various types of monitoring methodologies found in the current literature, and classify them into a spectrum of monitoring instrumentation techniques, ranging from completely asynchronous monitoring on the one end and completely synchronous monitoring on the other.
△ Less
Submitted 23 August, 2017;
originally announced August 2017.
-
Determinizing Monitors for HML with Recursion
Authors:
Luca Aceto,
Antonis Achilleos,
Adrian Francalanza,
Anna Ingólfsdóttir,
Sævar Örn Kjartansson
Abstract:
We examine the determinization of monitors for HML with recursion. We demonstrate that every monitor is equivalent to a deterministic one, which is at most doubly exponential in size with respect to the original monitor. When monitors are described as CCS-like processes, this doubly exponential bound is optimal. When (deterministic) monitors are described as finite automata (as their LTS), then th…
▽ More
We examine the determinization of monitors for HML with recursion. We demonstrate that every monitor is equivalent to a deterministic one, which is at most doubly exponential in size with respect to the original monitor. When monitors are described as CCS-like processes, this doubly exponential bound is optimal. When (deterministic) monitors are described as finite automata (as their LTS), then they can be exponentially more succinct than their CCS process form.
△ Less
Submitted 30 November, 2016;
originally announced November 2016.
-
Algebraic Synchronization Trees and Processes
Authors:
Luca Aceto,
Arnaud Carayol,
Zoltán Ésik,
Anna Ingólfsdóttir
Abstract:
We study algebraic synchronization trees, i.e., initial solutions of algebraic recursion schemes over the continuous categorical algebra of synchronization trees. In particular, we investigate the relative expressive power of algebraic recursion schemes over two signatures, which are based on those for Basic CCS and Basic Process Algebra, as a means for defining synchronization trees up to isomorp…
▽ More
We study algebraic synchronization trees, i.e., initial solutions of algebraic recursion schemes over the continuous categorical algebra of synchronization trees. In particular, we investigate the relative expressive power of algebraic recursion schemes over two signatures, which are based on those for Basic CCS and Basic Process Algebra, as a means for defining synchronization trees up to isomorphism as well as modulo bisimilarity and language equivalence. The expressiveness of algebraic recursion schemes is also compared to that of the low levels in Caucal's pushdown hierarchy.
△ Less
Submitted 3 October, 2016;
originally announced October 2016.
-
Proceedings First Workshop on Pre- and Post-Deployment Verification Techniques
Authors:
Luca Aceto,
Adrian Francalanza,
Anna Ingolfsdottir
Abstract:
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…
▽ More
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.
△ Less
Submitted 25 May, 2016;
originally announced May 2016.
-
Meta SOS - A Maude Based SOS Meta-Theory Framework
Authors:
Luca Aceto,
Eugen-Ioan Goriac,
Anna Ingolfsdottir
Abstract:
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 eq…
▽ More
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.
△ Less
Submitted 28 July, 2013;
originally announced July 2013.
-
Characteristic Formulae for Relations with Nested Fixed Points
Authors:
Luca Aceto,
Anna Ingólfsdóttir
Abstract:
A general framework for the connection between characteristic formulae and behavioral semantics is described in [2]. This approach does not suitably cover semantics defined by nested fixed points, such as the n-nested simulation semantics for n greater than 2. In this study we address this deficiency and give a description of nested fixed points that extends the approach for single fixed points in…
▽ More
A general framework for the connection between characteristic formulae and behavioral semantics is described in [2]. This approach does not suitably cover semantics defined by nested fixed points, such as the n-nested simulation semantics for n greater than 2. In this study we address this deficiency and give a description of nested fixed points that extends the approach for single fixed points in an intuitive and comprehensive way.
△ Less
Submitted 15 February, 2012;
originally announced February 2012.
-
Graphical representation of covariant-contravariant modal formulae
Authors:
Luca Aceto,
Ignacio Fábregas,
David de Frutos-Escrig,
Anna Ingólfsdóttir,
Miguel Palomino
Abstract:
Covariant-contravariant simulation is a combination of standard (covariant) simulation, its contravariant counterpart and bisimulation. We have previously studied its logical characterization by means of the covariant-contravariant modal logic. Moreover, we have investigated the relationships between this model and that of modal transition systems, where two kinds of transitions (the so-called may…
▽ More
Covariant-contravariant simulation is a combination of standard (covariant) simulation, its contravariant counterpart and bisimulation. We have previously studied its logical characterization by means of the covariant-contravariant modal logic. Moreover, we have investigated the relationships between this model and that of modal transition systems, where two kinds of transitions (the so-called may and must transitions) were combined in order to obtain a simple framework to express a notion of refinement over state-transition models. In a classic paper, Boudol and Larsen established a precise connection between the graphical approach, by means of modal transition systems, and the logical approach, based on Hennessy-Milner logic without negation, to system specification. They obtained a (graphical) representation theorem proving that a formula can be represented by a term if, and only if, it is consistent and prime. We show in this paper that the formulae from the covariant-contravariant modal logic that admit a "graphical" representation by means of processes, modulo the covariant-contravariant simulation preorder, are also the consistent and prime ones. In order to obtain the desired graphical representation result, we first restrict ourselves to the case of covariant-contravariant systems without bivariant actions. Bivariant actions can be incorporated later by means of an encoding that splits each bivariant action into its covariant and its contravariant parts.
△ Less
Submitted 22 August, 2011;
originally announced August 2011.
-
Axiomatizing GSOS with Predicates
Authors:
Luca Aceto,
Georgiana Caltais,
Eugen-Ioan Goriac,
Anna Ingolfsdottir
Abstract:
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 de…
▽ More
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.
△ Less
Submitted 15 August, 2011;
originally announced August 2011.
-
Modelling and Simulation of Asynchronous Real-Time Systems using Timed Rebeca
Authors:
Luca Aceto,
Matteo Cimini,
Anna Ingolfsdottir,
Arni Hermann Reynisson,
Steinar Hugi Sigurdarson,
Marjan Sirjani
Abstract:
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 im…
▽ More
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.
△ Less
Submitted 31 July, 2011;
originally announced August 2011.
-
A Bisimulation-based Method for Proving the Validity of Equations in GSOS Languages
Authors:
Luca Aceto,
Matteo Cimini,
Anna Ingolfsdottir
Abstract:
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…
▽ More
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.
△ Less
Submitted 15 February, 2010;
originally announced February 2010.
-
Characteristic Formulae for Fixed-Point Semantics: A General Framework
Authors:
Luca Aceto,
Anna Ingolfsdottir,
Joshua Sack
Abstract:
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 s…
▽ More
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.
△ Less
Submitted 10 November, 2009;
originally announced November 2009.
-
A Finite Equational Base for CCS with Left Merge and Communication Merge
Authors:
Luca Aceto,
Wan Fokkink,
Anna Ingolfsdottir,
Bas Luttik
Abstract:
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.
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.
△ Less
Submitted 2 August, 2006; v1 submitted 1 August, 2006;
originally announced August 2006.
-
Split-2 Bisimilarity has a Finite Axiomatization over CCS with<br> Hennessy's Merge
Authors:
Luca Aceto,
Wan Fokkink,
Anna Ingolfsdottir,
Bas Luttik
Abstract:
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…
▽ More
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.
△ Less
Submitted 21 June, 2005; v1 submitted 19 January, 2005;
originally announced January 2005.
