A survey of modal logics characterising behavioural equivalences for non-deterministic and stochastic systems
---
paper_title: Testing equivalences for processes

paper_content:

Given a set of processes and a set of tests on these processes we show how to define in a natural way three different equivalences on processes. These equivalences are applied to a particular language CCS. We give associated complete proof systems and fully abstract models. These models have a simple representation in terms of trees.
---
paper_title: Algebraic laws for nondeterminism and concurrency

paper_content:

Since a nondeterministic and concurrent program may, in general, communicate repeatedly with its environment, its meaning cannot be presented naturally as an input/output function (as is often done in the denotational approach to semantics). In this paper, an alternative is put forth. First, a definition is given of what it is for two programs or program parts to be equivalent for all observers; then two program parts are said to be observation congruent if they are, in all program contexts, equivalent. The behavior of a program part, that is, its meaning, is defined to be its observation congruence class. The paper demonstrates, for a sequence of simple languages expressing finite (terminating) behaviors, that in each case observation congruence can be axiomatized algebraically. Moreover, with the addition of recursion and another simple extension, the algebraic language described here becomes a calculus for writing and specifying concurrent programs and for proving their properties.
---
paper_title: Communicating sequential processes

paper_content:

This paper suggests that input and output are basic primitives of programming and that parallel composition of communicating sequential processes is a fundamental program structuring method. When combined with a development of Dijkstra's guarded command, these concepts are surprisingly versatile. Their use is illustrated by sample solutions of a variety of familiar programming exercises.
---
paper_title: A Theory of Testing for Markovian Processes

paper_content:

We present a testing theory for Markovian processes in order to formalize a notion of efficiency which may be useful for the analysis of soft real time systems. Our Markovian testing theory is shown to enjoy close connections with the classical testing theory of De Nicola-Hennessy and the probabilistic testing theory of Cleaveland-Smolka et al. The Markovian testing equivalence is also shown to be coarser than the Markovian bisimulation equivalence. A fully abstract characterization is developed to ease the task of establishing testing related relationships between Markovian processes. It is then demonstrated that our Markovian testing equivalence, which is based on the (easier to work with) probability of executing a successful computation whose average duration is not greater than a given amount of time, coincides with the Markovian testing equivalence based on the (more intuitive) probability of reaching success within a given amount of time. Finally, it is shown that it is not possible to define a Markovian preorder which is consistent with reward based performance measures, thus justifying why a generic notion of efficiency has been considered.
---
paper_title: Testing Equivalences and Fully Abstract Models for Probabilistic Processes

paper_content:

We present a framework in which the observable behavior of probabilistic processes is distinguished through testing. Probabilistic transition systems are used to model the operational behavior of processes. The observable behavior of processes is studied in terms of probabilities for successful interaction with tests. Based on these probabilities three equivalences are defined. We define three denotational models, and show that each model contains exactly the necessary information for verification of one of the equivalences.
---
paper_title: Interactive Markov Chains

paper_content:

This chapter introduces the central formalism of this book, Interactive Markov Chains1 (IMC). It arises as an integration of interactive processes and continuous-time Markov chains. There are different ways to combine both formalisms, and some of them have appeared in the literature. We therefore begin with a detailed discussion of the different integration possibilities and argue why we take which decision. As a result IMC combine the different ingredients as orthogonal to each other as possible. We proceed by defining composition operators for IMC. Wethen focus our attention on the discussion of strong and weak bisimilarity, incorporating the notion of maximal progress into the definitions. In order to efficiently compute these relations we develop algorithms that are more involved than the ones presented in earlier chapters. Anyhow, we prove that their computational complexity is not increased. A small example of using IMC to compositionally specify and aggregate the leaky bucket principle concludes this chapter.
---
paper_title: Performance Measure Sensitive Congruences for Markovian Process Algebras

paper_content:

The modeling and analysis experience with process algebras has shown the necessity of extending them with priority, probabilistic internal/external choice, and time while preserving compositionality. The purpose of this paper is to make a further step by introducing a way to express performance measures, in order to allow the modeler to capture the QoS metrics of interest. We show that the standard technique of expressing stationary and transient performance measures as weighted sums of state probabilities and transition frequencies can be imported in the process algebra framework. Technically speaking, if we denote by n ∈ N the number of performance measures of interest, in this paper we define a family of extended Markovian process algebras with generative master-reactive slaves synchronization mechanism called EMPAgrn including probabilities, priorities, exponentially distributed durations, and sequences of rewards of length n. Then we show that the Markovian bisimulation equivalence ∼MBn is a congruence for EMPAgrn which preserves the specified performance measures and we give a sound and complete axiomatization for finite EMPAgrn terms. Finally, we present a case study conducted with the software tool Two Towers in which we contrast the average performance of a selection of distributed algorithms for mutual exclusion modeled with EMPAgrn.
---
paper_title: Testing Preorders for Probabilistic Processes

paper_content:

We present a testing preorder for probabilistic processes based on a quantification of the probability with which processes pass tests. The theory enjoys close connections with the classical testing theory of De Nicola and Hennessy in that whenever a process passes a test with probability 1 (respectively some nonzero probability) in our setting, then the process must (respectively may) pass the test in the classical theory. We also develop an alternative characterization of the probabilistic testing preorders that takes the form of a mapping from probabilistic traces to the interval 0, 1], where a probabilistic trace is an alternating sequence of actions and probability distributions over actions. Finally, we give proof techniques, derived from the alternative characterizations, for establishing preorder relationships between probabilistic processes. The utility of these techniques is demonstrated by means of some simple examples.
---
paper_title: Trace Machines for Observing Continuous-Time Markov Chains

paper_content:

In this paper, we study several linear-time equivalences (Markovian trace equivalence, failure and ready trace equivalence) for continuous-time Markov chains that refer to the probabilities for timed execution paths. Our focus is on testing scenarios by means of push-button experiments with appropriate trace machines and a discussion of the connections between the equivalences. For Markovian trace equivalence, we provide alternative characterizations, including one that abstracts away from the time instances where actions are observed, but just reports on the average sojourn times in the states. This result is used for a reduction of the question whether two finite-state continuous-time Markov chains are Markovian trace equivalent to the probabilistic trace equivalence problem for discrete-time Markov chains (and the latter is known to be solvable in polynomial time).
---
paper_title: The Linear Time - Branching Time Spectrum II

paper_content:

This paper studies semantic equivalences and preorders for sequential systems with silent moves, restricting attention to the ones that abstract from successful termination, stochastic and real-time aspects of the investigated systems, and the structure of the visible actions systems can perform. It provides a parameterized definition of such a preorder, such that most such preorders and equivalences found in the literature are obtained by a suitable instantiation of the parameters. Other instantiations yield preorders that combine properties from various semantics. Moreover, the approach shows several ways in which preorders that were originally only considered for systems without silent moves, most notably the ready simulation, can be generalized to an abstract setting, and how preorders that were originally only considered for for systems without divergence, such as the coupled simulation, can be extended to divergent systems. All preorders come with—or rather as—a modal characterization, and when possible also a relational characterization. The paper concludes with some pros and cons of the preorders.
---
paper_title: A Compositional Approach to Performance Modelling

paper_content:

1. Introduction 2. Background 3. Performance evaluation process algebra 4. Modelling study: multi-server multi-queue systems 5. Notions of equivalence 6. Isomorphism and weak isomorphism 7. Strong bisimilarity 8. Strong equivalence 9. Conclusions Bibliography Index.
---
paper_title: Equivalences, Congruences, and Complete Axiomatizations for Probabilistic Processes

paper_content:

We study several notions of process equivalence—viz. trace, failure, ready, and bisimulation equivalence—in the context of probabilistic labeled transition systems. We show that, unlike nondeterministic transition systems, “maximality” of traces and failures does not increase the distinguishing power of trace and failure equivalence, respectively. Thus, in the probabilistic case, trace and maximal trace equivalence coincide, and failure and ready equivalence coincide.
---
paper_title: Modal Logic Characterization of Markovian Testing and Trace Equivalences

paper_content:

Markovian testing and trace equivalences have been recently proposed as reasonable alternatives to Markovian bisimilarity, as both of them induce at the Markov chain level an aggregation strictly coarser than ordinary lumping that is still exact. In this paper we provide a modal logic characterization for each of the two non-bisimulation-based Markovian behavioral equivalences, which relies on a quantitative interpretation of a variant of the Hennessy-Milner logic. We also show that, unlike the Markovian bisimilarity case, such modal logic characterizations exist only when probabilistic and temporal aspects are treated in a global way.
---
paper_title: Reactive, generative, and stratified models of probabilistic processes

paper_content:

Reactive, generative, and stratified models are considered within the framework of PCCS, a specification language for probabilistic processes. A structural operational semantics of PCCS, given as a set of inference rules for each of the models, a notion of bisimulation semantics, and some conference proofs are presented. >
---
paper_title: Bisimulation through probabilistic testing

paper_content:

Abstract We propose a language for testing concurrent processes and examine its strength in terms of the processes that are distinguished by a test. By using probabilistic transition systems as the underlying semantic model, we show how a testing algorithm can distinguish, with a probability arbitrarily close to one, between processes that are not bisimulation equivalent. We also show a similar result (in a slightly stronger form) for a new process relation called 2 3 - bisimulation —which lies strictly between that of simulation and bisimulation. Finally, the ultimately strength of the testing language is shown to identify a new process relation called probabilistic bisimulation—which is strictly stronger than bisimulation.
---
paper_title: A Compositional Approach to Performance Modelling

paper_content:

1. Introduction 2. Background 3. Performance evaluation process algebra 4. Modelling study: multi-server multi-queue systems 5. Notions of equivalence 6. Isomorphism and weak isomorphism 7. Strong bisimilarity 8. Strong equivalence 9. Conclusions Bibliography Index.
---
paper_title: Bisimulation through probabilistic testing

paper_content:

Abstract We propose a language for testing concurrent processes and examine its strength in terms of the processes that are distinguished by a test. By using probabilistic transition systems as the underlying semantic model, we show how a testing algorithm can distinguish, with a probability arbitrarily close to one, between processes that are not bisimulation equivalent. We also show a similar result (in a slightly stronger form) for a new process relation called 2 3 - bisimulation —which lies strictly between that of simulation and bisimulation. Finally, the ultimately strength of the testing language is shown to identify a new process relation called probabilistic bisimulation—which is strictly stronger than bisimulation.
---
paper_title: Testing equivalences for processes

paper_content:

Given a set of processes and a set of tests on these processes we show how to define in a natural way three different equivalences on processes. These equivalences are applied to a particular language CCS. We give associated complete proof systems and fully abstract models. These models have a simple representation in terms of trees.
---
paper_title: A Theory of Testing for Markovian Processes

paper_content:

We present a testing theory for Markovian processes in order to formalize a notion of efficiency which may be useful for the analysis of soft real time systems. Our Markovian testing theory is shown to enjoy close connections with the classical testing theory of De Nicola-Hennessy and the probabilistic testing theory of Cleaveland-Smolka et al. The Markovian testing equivalence is also shown to be coarser than the Markovian bisimulation equivalence. A fully abstract characterization is developed to ease the task of establishing testing related relationships between Markovian processes. It is then demonstrated that our Markovian testing equivalence, which is based on the (easier to work with) probability of executing a successful computation whose average duration is not greater than a given amount of time, coincides with the Markovian testing equivalence based on the (more intuitive) probability of reaching success within a given amount of time. Finally, it is shown that it is not possible to define a Markovian preorder which is consistent with reward based performance measures, thus justifying why a generic notion of efficiency has been considered.
---
paper_title: Testing Equivalences and Fully Abstract Models for Probabilistic Processes

paper_content:

We present a framework in which the observable behavior of probabilistic processes is distinguished through testing. Probabilistic transition systems are used to model the operational behavior of processes. The observable behavior of processes is studied in terms of probabilities for successful interaction with tests. Based on these probabilities three equivalences are defined. We define three denotational models, and show that each model contains exactly the necessary information for verification of one of the equivalences.
---
paper_title: Performance Measure Sensitive Congruences for Markovian Process Algebras

paper_content:

The modeling and analysis experience with process algebras has shown the necessity of extending them with priority, probabilistic internal/external choice, and time while preserving compositionality. The purpose of this paper is to make a further step by introducing a way to express performance measures, in order to allow the modeler to capture the QoS metrics of interest. We show that the standard technique of expressing stationary and transient performance measures as weighted sums of state probabilities and transition frequencies can be imported in the process algebra framework. Technically speaking, if we denote by n ∈ N the number of performance measures of interest, in this paper we define a family of extended Markovian process algebras with generative master-reactive slaves synchronization mechanism called EMPAgrn including probabilities, priorities, exponentially distributed durations, and sequences of rewards of length n. Then we show that the Markovian bisimulation equivalence ∼MBn is a congruence for EMPAgrn which preserves the specified performance measures and we give a sound and complete axiomatization for finite EMPAgrn terms. Finally, we present a case study conducted with the software tool Two Towers in which we contrast the average performance of a selection of distributed algorithms for mutual exclusion modeled with EMPAgrn.
---
paper_title: Discrete Time Generative-Reactive Probabilistic Processes with Different Advancing Speeds

paper_content:

We present a process algebra expressing probabilistic external/internal choices, multi-way synchronizations, and processes with different advancing speeds in the context of discrete time, i.e. where time is not continuous but is represented by a sequence of discrete steps as in discrete time Markov chains (DTMCs). To this end, we introduce a variant of CSP that employs a probabilistic asynchronous parallel operator whose synchronization mechanism is based on a mixture of the classical generative and reactive models of probability. In particular, differently from existing discrete time process algebras, where parallel processes are executed in synchronous locksteps, the parallel operator that we adopt allows processes with different probabilistic advancing speeds (mean number of actions executed per time unit) to be modeled. Moreover, our generative-reactive synchronization mechanism makes it possible to always derive DTMCs in the case of fully specified systems. We then present a sound and complete axiomatization of probabilistic bisimulation over finite processes of our calculus, that is a smooth extension of the axiom system for a standard process algebra, thus solving the open problem of cleanly axiomatizing action restriction in the generative model. As a further result, we show that, when evaluating steady state based performance measures which are expressible by attaching rewards to actions, our approach provides an exact solution even if the advancing speeds are considered not to be probabilistic, without incurring the state space explosion problem that arises with standard synchronous approaches. We finally present a case study on multi-path routing showing the expressiveness of our calculus and that it makes it particularly easy to produce scalable specifications.
---
paper_title: Communicating sequential processes

paper_content:

This paper suggests that input and output are basic primitives of programming and that parallel composition of communicating sequential processes is a fundamental program structuring method. When combined with a development of Dijkstra's guarded command, these concepts are surprisingly versatile. Their use is illustrated by sample solutions of a variety of familiar programming exercises.
---
paper_title: Trace Machines for Observing Continuous-Time Markov Chains

paper_content:

In this paper, we study several linear-time equivalences (Markovian trace equivalence, failure and ready trace equivalence) for continuous-time Markov chains that refer to the probabilities for timed execution paths. Our focus is on testing scenarios by means of push-button experiments with appropriate trace machines and a discussion of the connections between the equivalences. For Markovian trace equivalence, we provide alternative characterizations, including one that abstracts away from the time instances where actions are observed, but just reports on the average sojourn times in the states. This result is used for a reduction of the question whether two finite-state continuous-time Markov chains are Markovian trace equivalent to the probabilistic trace equivalence problem for discrete-time Markov chains (and the latter is known to be solvable in polynomial time).
---
paper_title: Equivalences, Congruences, and Complete Axiomatizations for Probabilistic Processes

paper_content:

We study several notions of process equivalence—viz. trace, failure, ready, and bisimulation equivalence—in the context of probabilistic labeled transition systems. We show that, unlike nondeterministic transition systems, “maximality” of traces and failures does not increase the distinguishing power of trace and failure equivalence, respectively. Thus, in the probabilistic case, trace and maximal trace equivalence coincide, and failure and ready equivalence coincide.
---
paper_title: Algebraic laws for nondeterminism and concurrency

paper_content:

Since a nondeterministic and concurrent program may, in general, communicate repeatedly with its environment, its meaning cannot be presented naturally as an input/output function (as is often done in the denotational approach to semantics). In this paper, an alternative is put forth. First, a definition is given of what it is for two programs or program parts to be equivalent for all observers; then two program parts are said to be observation congruent if they are, in all program contexts, equivalent. The behavior of a program part, that is, its meaning, is defined to be its observation congruence class. The paper demonstrates, for a sequence of simple languages expressing finite (terminating) behaviors, that in each case observation congruence can be axiomatized algebraically. Moreover, with the addition of recursion and another simple extension, the algebraic language described here becomes a calculus for writing and specifying concurrent programs and for proving their properties.
---
paper_title: Specifying Performance Measures for PEPA

paper_content:

Stochastic process algebras such as PEPA provide ample support for the component-based construction of models. Tools compute the numerical solution of these models; however, the stochastic process algebra methodology lacks support for the specification and calculation of complex performance measures. This paper addresses that problem by presenting a performance specification language which supports high level reasoning about PEPA models, allowing the description of equilibrium (steady-state) measures. The meaning of the specification language can be made formal by examining its foundations in a stochastic modal logic. A case-study is presented to illustrate the approach.
---
paper_title: Bisimulation through probabilistic testing

paper_content:

Abstract We propose a language for testing concurrent processes and examine its strength in terms of the processes that are distinguished by a test. By using probabilistic transition systems as the underlying semantic model, we show how a testing algorithm can distinguish, with a probability arbitrarily close to one, between processes that are not bisimulation equivalent. We also show a similar result (in a slightly stronger form) for a new process relation called 2 3 - bisimulation —which lies strictly between that of simulation and bisimulation. Finally, the ultimately strength of the testing language is shown to identify a new process relation called probabilistic bisimulation—which is strictly stronger than bisimulation.
---
paper_title: Algebraic laws for nondeterminism and concurrency

paper_content:

Since a nondeterministic and concurrent program may, in general, communicate repeatedly with its environment, its meaning cannot be presented naturally as an input/output function (as is often done in the denotational approach to semantics). In this paper, an alternative is put forth. First, a definition is given of what it is for two programs or program parts to be equivalent for all observers; then two program parts are said to be observation congruent if they are, in all program contexts, equivalent. The behavior of a program part, that is, its meaning, is defined to be its observation congruence class. The paper demonstrates, for a sequence of simple languages expressing finite (terminating) behaviors, that in each case observation congruence can be axiomatized algebraically. Moreover, with the addition of recursion and another simple extension, the algebraic language described here becomes a calculus for writing and specifying concurrent programs and for proving their properties.
---
paper_title: Acceptance trees

paper_content:

A simple model, AT, for nondeterministic machines is presented which is based on certain types of trees. A set of operations, S, is defined over AT and it is shown to be completely characterized by a set of inequations over S. AT is used to define the denotational semantics of a language for defining nondeterministic machines. The significance of the model is demonstrated by showing that this semantics reflects an intuitive operational semantics of machines based on the idea that machines should only be differentiated if there is some experiment that differentiates between them.
---
paper_title: Testing Equivalences and Fully Abstract Models for Probabilistic Processes

paper_content:

We present a framework in which the observable behavior of probabilistic processes is distinguished through testing. Probabilistic transition systems are used to model the operational behavior of processes. The observable behavior of processes is studied in terms of probabilities for successful interaction with tests. Based on these probabilities three equivalences are defined. We define three denotational models, and show that each model contains exactly the necessary information for verification of one of the equivalences.
---
paper_title: Testing Preorders for Probabilistic Processes

paper_content:

We present a testing preorder for probabilistic processes based on a quantification of the probability with which processes pass tests. The theory enjoys close connections with the classical testing theory of De Nicola and Hennessy in that whenever a process passes a test with probability 1 (respectively some nonzero probability) in our setting, then the process must (respectively may) pass the test in the classical theory. We also develop an alternative characterization of the probabilistic testing preorders that takes the form of a mapping from probabilistic traces to the interval 0, 1], where a probabilistic trace is an alternating sequence of actions and probability distributions over actions. Finally, we give proof techniques, derived from the alternative characterizations, for establishing preorder relationships between probabilistic processes. The utility of these techniques is demonstrated by means of some simple examples.
---
paper_title: A Theory of Testing for Markovian Processes

paper_content:

We present a testing theory for Markovian processes in order to formalize a notion of efficiency which may be useful for the analysis of soft real time systems. Our Markovian testing theory is shown to enjoy close connections with the classical testing theory of De Nicola-Hennessy and the probabilistic testing theory of Cleaveland-Smolka et al. The Markovian testing equivalence is also shown to be coarser than the Markovian bisimulation equivalence. A fully abstract characterization is developed to ease the task of establishing testing related relationships between Markovian processes. It is then demonstrated that our Markovian testing equivalence, which is based on the (easier to work with) probability of executing a successful computation whose average duration is not greater than a given amount of time, coincides with the Markovian testing equivalence based on the (more intuitive) probability of reaching success within a given amount of time. Finally, it is shown that it is not possible to define a Markovian preorder which is consistent with reward based performance measures, thus justifying why a generic notion of efficiency has been considered.
---
paper_title: Specifying Performance Measures for PEPA

paper_content:

Stochastic process algebras such as PEPA provide ample support for the component-based construction of models. Tools compute the numerical solution of these models; however, the stochastic process algebra methodology lacks support for the specification and calculation of complex performance measures. This paper addresses that problem by presenting a performance specification language which supports high level reasoning about PEPA models, allowing the description of equilibrium (steady-state) measures. The meaning of the specification language can be made formal by examining its foundations in a stochastic modal logic. A case-study is presented to illustrate the approach.
---
paper_title: Bisimulation through probabilistic testing

paper_content:

Abstract We propose a language for testing concurrent processes and examine its strength in terms of the processes that are distinguished by a test. By using probabilistic transition systems as the underlying semantic model, we show how a testing algorithm can distinguish, with a probability arbitrarily close to one, between processes that are not bisimulation equivalent. We also show a similar result (in a slightly stronger form) for a new process relation called 2 3 - bisimulation —which lies strictly between that of simulation and bisimulation. Finally, the ultimately strength of the testing language is shown to identify a new process relation called probabilistic bisimulation—which is strictly stronger than bisimulation.
---
paper_title: Testing equivalences for processes

paper_content:

Given a set of processes and a set of tests on these processes we show how to define in a natural way three different equivalences on processes. These equivalences are applied to a particular language CCS. We give associated complete proof systems and fully abstract models. These models have a simple representation in terms of trees.
---
paper_title: Bisimulation through probabilistic testing

paper_content:

Abstract We propose a language for testing concurrent processes and examine its strength in terms of the processes that are distinguished by a test. By using probabilistic transition systems as the underlying semantic model, we show how a testing algorithm can distinguish, with a probability arbitrarily close to one, between processes that are not bisimulation equivalent. We also show a similar result (in a slightly stronger form) for a new process relation called 2 3 - bisimulation —which lies strictly between that of simulation and bisimulation. Finally, the ultimately strength of the testing language is shown to identify a new process relation called probabilistic bisimulation—which is strictly stronger than bisimulation.
---

Title: A survey of modal logics characterising behavioural equivalences for non-deterministic and stochastic systems

Section 1: Introduction
Description 1: Introduce the topic of behavioral equivalences and the different approaches such as bisimulation, testing, and trace equivalences. Also, provide a brief overview of the paper's structure and objectives.

Section 2: Process Calculi
Description 2: Present the nondeterministic, probabilistic, and Markovian process calculi, including their syntax and structural operational semantics.

Section 3: Behavioral Equivalences
Description 3: Recall the three major approaches to defining behavioral equivalences—bisimulation, testing, and trace—along with their nondeterministic, probabilistic, and Markovian versions.

Section 4: Modal Characterizations of Bisimulation Equivalence
Description 4: Present the modal logic characterizations of the nondeterministic, probabilistic, and Markovian versions of bisimulation equivalence.

Section 5: Modal Characterizations of Testing Equivalence
Description 5: Recall the modal logic characterization of nondeterministic testing equivalence, and provide new modal logic characterizations for the probabilistic and Markovian versions of testing equivalence.

Section 6: Modal Characterizations of Trace Equivalence
Description 6: Recall the modal logic characterization of nondeterministic trace equivalence, and provide new modal logic characterizations for the probabilistic and Markovian versions of trace equivalence.

Section 7: Comparing the Modal Logic Characterizations
Description 7: Compare the nine modal logic characterizations across the three approaches to defining behavioral equivalences and regularities within each approach.

Section 8: Future Work
Description 8: Discuss potential future research directions, including the regularity of logical operators for the different versions of testing equivalence, and conjectures regarding tests with copying.