1,721,051 research outputs found
Proceedings Combined 25th International Workshop on Expressiveness in Concurrency and 15th Workshop on Structural Operational Semantics Beijing, China, September 3, 2018 Preface
No full textA weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spaces
No full textBisimulation metrics are a successful instrument used to estimate the behavioural distance between probabilistic concurrent systems. They have been defined in both discrete and continuous state space models. However, the weak semantics approach, where non-observable actions are abstracted away, has been adopted only in the discrete case. In this paper we fill this gap and provide a weak bisimulation metric for models with continuous state spaces. A technical difficulty is to provide a suitable notion of weak transition, which requires to lift transitions leaving from states to transitions leaving from a continuous distribution over states. We prove that our weak bisimulation metric is non-expansive, thus allowing for compositional reasoning. We prove that systems at distance zero are equated by a suitable notion of probabilistic weak bisimulation. We apply our theory in a case study where continuous distributions derive from the evolution of the physical environment
Probabilistic divide & congruence: Branching bisimilarity
No full textSince the seminal paper by Bloom, Fokkink and van Glabbeek, the Divide and Congruence technique allows for the derivation of compositional properties of nondeterministic processes from the SOS-based decomposition of their modal properties. In an earlier paper, we extended their technique to deal also with quantitative aspects of process behavior: we proved the (pre)congruence property for strong (bi)simulations on processes with nondeterminism and probability. In this paper we further extend our decomposition method to favor compositional reasoning with respect to probabilistic weak semantics. In detail, we consider probabilistic branching and rooted probabilistic branching bisimilarity, and we propose logical characterizations for them. These are strongly based on the modal operator (epsilon) which combines quantitative information and weak semantics by introducing a sort of probabilistic lookahead on process behavior. Our enhanced method will exploit distribution specifications, an SOS-like framework defining the probabilistic behavior of processes, to decompose this particular form of lookahead. We will show how we can apply the proposed decomposition method to derive congruence formats for the considered equivalences from their logical characterizations. (C) 2019 Elsevier B.V. All rights reserved
Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics Berlin, Germany, 4th September 2017 Preface
No full textRaiders of the lost equivalence: Probabilistic branching bisimilarity
No full textProbabilistic branching bisimilarity allows us to compare process behaviour with respect to their branching structure and probabilistic features, while abstracting away from those computation steps that can be marked as irrelevant to the analysis at hand. To the best of our knowledge, in the context of nondeterministic probabilistic processes, no proof of probabilistic branching bisimilarity being an equivalence has been provided so far. Since, as happened in the fully nondeterministic case, some researchers are using such a result by taking it for granted, we decided to dedicate this note to a formal proof of it. More precisely, we extend and adapt the proof strategy used by Basten in the fully nondeterministic case. Thus, we introduce the probabilistic analogue to the notion of semi-branching bisimilarity and to van Glabbeek and Weijland's Stuttering Lemma to prove that probabilistic branching bisimilarity is indeed an equivalence relation
The metric linear-time branching-time spectrum on nondeterministic probabilistic processes
No full textBehavioral equivalences were introduced as a simple and elegant proof methodology for establishing whether the behavior of two processes cannot be distinguished by an external observer. The knowledge of observers usually depends on the observations that they can make on process behavior. Furthermore, the combination of nondeterminism and probability in concurrent systems leads to several interpretations of process behavior. Clearly, different kinds of observations as well as different interpretations lead to different kinds of behavioral relations, such as (bi)simulations, traces and testing. If we restrict our attention to linear properties only, we can identify three main approaches to trace and testing semantics: the trace distributions, the trace-by-trace and the extremal probabilities approaches. In this paper, we propose novel notions of behavioral metrics that are based on the three classic approaches above, and that can be used to measure the disparities in the linear behavior of processes with respect to trace and testing semantics. We study the properties of these metrics, like compositionality (expressed in terms of the non-expansiveness property), and we compare their expressive powers. More precisely, we compare them also to (bi)simulation metrics, thus obtaining the first metric linear time – branching time spectrum
Stark: A Software Tool for the Analysis of Robustness in the unKnown Environment
No full textCyber-Physical Systems (CPSs) are characterised by the interaction of various agents operating under highly changing and, sometimes, unpredictable environmental conditions. It is therefore fundamental to verify whether these systems are robust against perturbations, i.e., whether systems are able to function correctly even in perturbed circumstances. In this paper we present the Software Tool for the Analysis of Robustness in the unKnown environment (Stark), our Java tool for the specification, analysis and testing of robustness properties of CPSs. Stark includes: (i) a specification language for systems behaviour, perturbations, distances on systems behaviours, and properties of those distances; (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 formulae 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
- …
