Abstract A digital twin is a virtual replica of a physical system that has to interact with it in real-time in order to facilitate decision-making, to reduce failures and costs, and to ensure a coherent and safe system execution. We call effectiveness the ability of the digital twin to direct the physical counterpart. In this paper we provide the means to evaluate the effectiveness of a digital twin in the case that the physical system is operating under uncertainty, and it is therefore subject to perturbations . Specifically, we present the DT-Stark tool, that extends Stark , a tool for modelling and verification of systems operating under uncertainty, with feedback , a special mechanism that allow us to model the communications, and their effects, between the digital and the physical (perturbed) twin in a concise, clean fashion. We can then exploit the features of Stark to compare the behaviour of the twins, to verify properties over them, and to measure effectiveness. We provide some examples of the use of our tool by applying it to the evaluation of the effectiveness of digital twins in two robotic scenarios: an industrial plant and a smart hospital.

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.

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.

In probabilistic process algebras the classic qualitative description of process behaviour is enriched with quantitative information on it, usually modelled in terms of probabilistic weights and/or distributions over the qualitative behaviour. In this setting, we use behavioural equivalences to check whether two processes show exactly the same behaviour, and, if this is not the case, we can use behavioural metrics to measure the distance between them. Compositional reasoning requires that equivalence, or closeness, of behaviour of two processes are not destroyed when language operators are applied on top of them in order to build larger processes. Formally, the equivalence must be a congruence, and the metric must be uniformly continuous, with respect to language operators. Instead of verifying these compositional properties by hand, operator-by-operator, it is much more convenient to prove them for a class of operators once for all, and to check that the operators one is dealing with are in that class. This is achieved by means of SOS specification formats: they consist in a set of syntactical constraints characterising a class of operators on the patterns of SOS rules, that define the operational semantics of languages. With this survey, we aim to collect and describe the specification formats that have been proposed in the literature to guarantee the compositional properties of (variants of) bisimulation equivalences and bisimulation metrics in the probabilistic setting.

We present the Software Tool for the Analysis of Robustness in the unKnown environment (Stark), our Java tool for the specification, analysis and verification of robustness properties of Cyber-Physical Systems (CPSs). Stark includes: (i) a specification language for systems behaviour, perturbations, distances on systems behaviours, and requirements on systems behaviour expressed in the Robustness Temporal Logic (RobTL), a temporal logic for the specification and verification of properties on the evolution of distances between the behaviours of CPSs, and thus also of robustness properties; (ii) a module for the simulation of system behaviours and their perturbed versions; (iii) a module for the evaluation of distances between behaviours; (iv) a statistical model checker for RobTL formulae.

We propose two step-by-step approaches to the analysis of robustness in biochemical networks. Our aim is to measure the ability of the network to exhibit step-by-step limited variations on the concentration of a species of interest at varying of the initial concentration of other species. The first approach we propose is reaction-by-reaction, i.e. we compare the states reached by nominal and perturbed networks after they have performed the same number of reactions. We provide a statistical technique allowing for estimating robustness, we implement it in a tool called spebnr ( a Simple Python Environment for statistical estimation of Biochemical Network Robustness ) and showcase it on three case studies: the EnvZ/OmpR osmoregulatory signaling system of Escherichia Coli, the mechanism of bacterial chemotaxis of Escherichia Coli, and enzyme activity at saturation. Then, we consider a time-by-time approach, in which networks are compared on the basis of the states they reached at the same time point, regardless of how many reactions occurred. This approach is implemented in Stark , and we apply it to the study the robustness of the EnvZ/OmpR osmoregulatory signaling system and the Lotka-Volterra equations.

Due to the diffusion of IoT, modern software systems are often thought to control and coordinate smart devices in order to manage assets and resources, and to guarantee efficient behaviours. For this class of systems, which interact extensively with humans and with their environment, it is thus crucial to guarantee their correct behaviour in order to avoid unexpected and possibly dangerous situations. In this paper we will present a framework that allows us to measure the robustness of systems. This is the ability of a program to tolerate changes in the environmental conditions and preserving the original behaviour. In the proposed framework, the interaction of a program with its environment is represented as a sequence of random variables describing how both evolve in time. For this reason, the considered measures will be defined among probability distributions of observed data. The proposed framework will be then used to define the notions of adaptability and reliability. The former indicates the ability of a program to absorb perturbation on environmental conditions after a given amount of time. The latter expresses the ability of a program to maintain its intended behaviour (up-to some reasonable tolerance) despite the presence of perturbations in the environment. Moreover, an algorithm, based on statistical inference, is proposed to evaluate the proposed metric and the aforementioned properties. We use two case studies to the describe and evaluate the proposed approach.

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.

Bergstra and Klop have shown thatbisimilarityhas afiniteequational axiomatisation over ACP/CCS extended with the binaryleftandcommunication mergeoperators. Moller proved that auxiliary operators arenecessaryto obtain a finite axiomatisation of bisimilarity over CCS, and Aceto et al. showed that this remains true whenHennessy’s mergeis added to that language. These results raise the question of whether there isoneauxiliarybinaryoperator whose addition to CCS leads to a finite axiomatisation of bisimilarity. We contribute to answering this question in the simplified setting of the recursion-, relabelling-, and restriction-free fragment of CCS. We formulate three natural assumptions pertaining to the operational semantics of auxiliary operators and their relationship to parallel composition and prove that an auxiliary binary operator facilitating a finite axiomatisation of bisimilarity in the simplified setting cannot satisfy all three assumptions.

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.

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. On the other hand, we show that no congruence over that language 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.

We propose a method for the decomposition of modal formulae on processes with nondeterminism and probability with respect to Structural Operational Semantics. The purpose is to reduce the satisfaction problem of a formula for a process to verifying whether its subprocesses satisfy certain formulae obtained from the decomposition. To deal with the probabilistic behavior of processes, and thus with the decomposition of formulae characterizing it, we introduce a SOS-like machinery allowing for the specification of the behavior of open distribution terms. By our decomposition, we obtain (pre)congruence formats for probabilistic bisimilarity, ready similarity and similarity.

We propose a SOS-based method for decomposing modal formulae for nondeterministic probabilistic processes. The purpose is to reduce the satisfaction problem of a formula for a process to verifying whether its subprocesses satisfy certain formulae obtained from its decomposition. By our decomposition, we obtain (pre)congruence formats for probabilistic bisimilarity, ready similarity and similarity.

We study function elimination for Arithmetical Logics. We propose a method allowing substitution of functions occurring in a given formula with functions with less arity. We prove the correctness of the method and we use it to show the decidability of the satisfiability problem for two classes of f ormulas allowing linear and polynomial terms.

Rule formats are sets of syntactical constraints over SOS rules ensuring semantical properties of the derived LTS. Given a rule format, our proposal is to relax the constraints imposed on each single rule and to introduce some constraints on the form of the whole set of rules, thus obtaining a new format ensuring the same semantical property and being less demanding than the original one. We apply our idea to a well known rule format for rooted branching bisimulation equivalence.