Nordic Journal of Computing

Probabilistic Simulations for Probabilistic Processes ^{∗}

Roberto Segala and Nancy Lynch MIT Laboratory for Computer Science Cambridge, MA 02139

Abstract. Several probabilistic simulation relations for probabilistic systems are defined and evaluated according to two criteria: compositionality and preservation of “interesting” properties. Here, the interesting properties of a system are identified with those that are expressible in an untimed version of the Timed Probabilistic concurrent Computation Tree Logic (TPCTL) of Hansson. The definitions are made, and the evaluations carried out, in terms of a general labeled transition system model for concurrent probabilistic computation. The results cover weak simulations, which abstract from internal computation, as well as strong simulations, which do not.

1. Introduction

Randomization has been shown to be a useful tool for the solution of problems in distributed systems [2, 3, 15]. In order to support reasoning about probabilistic distributed systems, many researchers have recently focused on the study of models and methods for the analysis of such systems [4, 6, 8, 26, 29, 30]. The general approach that is taken is to extend to the probabilistic setting those models and methods that have already proved successful for non-probabilistic distributed systems.

In the non-probabilistic setting, labeled transition systems have become well accepted as a basis for formal specification and verification of concurrent and distributed systems. (See, e.g., [21, 22].) A transition system is an abstract machine that represents either an implementation (i.e., a physical device or software system), or a specification (i.e., a description of the required properties of an implementation). In order to extend labeled transition systems to the probabilistic setting, the main addition that is needed is some mechanism for representing probabilistic choices as well as nondeterministic choices [8, 26, 30].

In the non-probabilistic setting, there are two principal methods that are used for analyzing labeled transition systems: temporal logic (e.g. [25]),

∗ Supported by NSF grant CCR-89-15206, and CCR-92-25124, by ARPA contracts N00014-89-J-1988 and N00014-92-J-4033, and by ONR contract N00014-91-J-1046.

Received July 1997.

which is used to establish that a system satisfies certain properties, and equivalence or preorder relations (e.g., [9, 21, 22, 24]), which are used to establish that one system “implements” another, according to some notion of implementation. Each equivalence or preorder preserves some of the properties of a system, and thus the use of a relation as a notion of implementation means that we are interested only in the properties that such a relation preserves.

Among the equivalences and preorders that have proved most useful are the class of simulation relations, which establish step-by-step correspondences between two systems. Bisimulation relations are two-directional relations that have proved fundamental in the process algebraic setting. Unidirectional simulations, such as refinement mappings and forward simulations, have turned out to be quite successful in formal verification of nonprobabilistic distributed systems [12, 20, 21]. Thus, it is highly desirable to extend the use of simulations to the probabilistic setting.

In this paper, we define several extensions of the classical bisimulation and simulation relations (both in their strong and weak versions), to the probabilistic setting. There are many possible extensions that could be made; it is important to evaluate the various possibilities according to objective criteria. We use two criteria: compositionality and preservation of “interesting” properties. The first requirement, compositionality, is widely accepted since it forms the basis of many modular verification techniques.

To make sense of the second requirement, it is necessary to be specific about what is meant by an “interesting” property. Here, we identify the interesting properties of a system with those that are expressible in an untimed version (PCTL) of the Timed Probabilistic concurrent Computation Tree Logic (TPCTL) of Hansson [8]; as discussed in [8], this logic is sufficiently powerful to represent most of the properties of practical interest. Thus, our second evaluation criterion is based on the types of PCTL formulas that a relation preserves. For the weak relations, i.e., the ones that abstract from internal computation, we use a new version of PCTL, called WPCTL, which abstracts from internal computation as well.

We define and evaluate our simulation relations in terms of a new general labeled transition system model for concurrent probabilistic computation, which borrows ideas from [8, 30]. The model distinguishes between probabilistic and nondeterministic choices but, unlike the Concurrent Markov Chains of [8, 30], does not distinguish between probabilistic and nondeterministic states. A probabilistic automaton is a labeled transition system whose transition relation is a set of pairs (s, P), where P is a discrete probability distribution over (action, state) pairs and a special symbol δ, representing deadlock. If the distribution P is only over pairs with the same action, then a transition is called simple and can be denoted by s ⟶^{a} P′, where P′ is a discrete probability distribution over states. The separation between nondeterministic and probabilistic behavior is achieved by means of adversaries (or schedulers), that, similar to [8, 26, 30], choose a next transition to schedule based on the past history of the automaton. In our case, differently from [8, 26, 30], we allow an adversary to choose the next transition randomly. Indeed, an external environment that provides some input essentially behaves like a randomized adversary.

Our first major result is that randomized adversaries do not change the distinguishing power of PCTL and WPCTL. Intuitively, the main reason for this result is that PCTL and WPCTL are concerned with probability bounds rather than exact probabilities.

We then redefine the strong bisimulation relation of [16] in terms of our model, and also define a strong simulation relation that generalizes the simulation relation of [13], strengthening it a bit so that some liveness is preserved. We show that strong simulation preserves PCTL formulas without negation and existential quantification. Next, we generalize the strong relations by making them insensitive to probabilistic combination of transitions, i.e., by allowing probabilistic combination of several transitions in order to simulate a single transition. The motivation for this generalization is that the combination of transitions corresponds to the ability of an adversary to choose the next transition probabilistically. Our second main result is that the new relations, called strong probabilistic bisimulation and strong probabilistic simulation, are still compositional and preserve PCTL formulas and PCTL formulas without negation and existential quantification, respectively.

Similar to the strong case, we define new relations that abstract from internal computation and we show that they preserve WPCTL. However, the straightforward generalization of the strong probabilistic relations, although compositional, does not guarantee that WPCTL is preserved. For this reason we introduce two other relations, called branching probabilistic bisimulation and branching probabilistic simulation, which impose new restrictions similar to those of branching bisimulation [7]. Our third main result is that branching probabilistic bisimulation and branching probabilistic simulation are compositional and preserve WPCTL formulas and WPCTL formulas without negation and existential quantification, respectively, up to a condition about divergences.

The rest of the paper is organized as follows. Section 2 defines the standard automata of non-probabilistic systems; Section 3 introduces our probabilistic model; Section 4 introduces PCTL, defines its semantics in terms of our model, and shows that the distinguishing power of PCTL does not change by using randomized adversaries; Sections 5, 6 and 7 study the strong and weak relations on our probabilistic model, and show how they preserve PCTL formulas; Section 8 contains some concluding remarks and further work.

2. Automata

An automaton A consists of four components: a set states(A) of states, a nonempty set start(A) ⊆ states(A) of start states, an action signature sig(A) = (ext(A), int(A)) where ext(A) and int(A) are disjoint sets of external and internal actions, respectively, and a transition relation trans(A) ⊆ states(A)×acts(A)×states(A), where acts(A) denotes the set ext(A)∪int(A) of actions. Thus, an automaton is a state machine with labeled transitions. Its action signature describes the interface with the external environment by specifying which actions model events that are visible from the external environment and which ones model internal events.

An execution fragment α of an automaton A is a (finite or infinite) sequence of alternating states and actions starting with a state and, if the execution fragment is finite, ending in a state, α = s_{0}a_{1}s_{1}a_{2}s_{2} ⋯, where each (s_{i}, a_{i+1}, s_{i+1}) is a transition of A. Denote by fstate(α) the first state of α and, if α is finite, denote by lstate(α) the last state of α. Furthermore, denote by frag^{∗}(A) and frag(A) the sets of finite and all execution fragments of A, respectively. An execution is an execution fragment whose first state is a start state. Denote by exec^{∗}(A) and exec(A) the sets of finite and all executions of A, respectively. A state s of A is reachable if there exists a finite execution of A that ends in s. A finite execution fragment α_{1} = s_{0}a_{1}s_{1} ⋯ a_{n}s_{n} of A and an execution fragment α_{2} = s_{n}a_{n+1}s_{n+1} ⋯ of A can be concatenated. In this case the concatenation, written α_{1}⌢α_{2}, is the execution fragment s_{0}a_{1}s_{1} ⋯ a_{n}s_{n}a_{n+1}s_{n+1} · · ·. An execution fragment α_{1} of A is a prefix of an execution fragment α_{2} of A, written α_{1} ≤ α_{2}, if either α_{1} = α_{2} or α_{1} is finite and there exists an execution fragment α′_{1} of A such that α_{2} = α_{1}⌢α′_{1}.

3. The Basic Probabilistic Model

3.1 Probability Spaces

Most of our definitions rely on the notion of a probability space, which is used to denote which events can be observed and what are their probabilities.

A probability space is a triplet (Ω, F, P) where Ω is a set, F is a collection of subsets of Ω that is closed under complement and countable union and such that Ω ∈ F, and P is a function from F to [0, 1] such that P [Ω] = 1 and for any collection {C_{i}}_{i} of at most countably many pairwise disjoint elements of F, P [∪_{i}C_{i}] = ∑_{i} P [C_{i}].

The set Ω is called the sample space and contains the objects that we want to analyze. For example Ω = [0, 1]. The set F is called the σ-algebra and contains the subsets of Ω that we can measure, also called events. For example F can be the set of measurable sets of [0, 1] according to Lebesgue. Finally, P is called the probability measure and is a function that associates a measure with each element of F. For example, P can associate each element of F with its Lebesgue measure.

A probability space (Ω, F, P) is discrete if F = 2^{Ω} and for each C ⊆ Ω, P [C] = ∑_{x∈C} P [{x}]. It is immediate to verify that for every discrete probability space there are at most countably many points with a non-zero probability measure. Given a set X, we denote by Probs(X) the set of discrete probability spaces (Ω, F, P) whose sample space Ω is a subset of X.

The Dirac distribution over an element x, denoted by D(x), is the probability space with a unique element x.

Throughout the paper we denote a probability space (Ω, F, P) by P. As a notational convention, if P is decorated with indices and primes, then the same indices and primes carry to its elements. Thus, P′_{i} denotes (Ω′_{i}, F′_{i}, P′_{i}).

The product of two discrete probability spaces (Ω_{1}, F_{1}, P_{1}) and (Ω_{2}, F_{2}, P_{2}), denoted by (Ω_{1}, F_{1}, P_{1})⊗(Ω_{2}, F_{2}, P_{2}), is the discrete probability space (Ω_{1}× Ω_{2}, 2^{Ω_{1}×Ω_{2}}, P), where P [(x_{1}, x_{2})] = P_{1}[x_{1}]P_{2}[x_{2}] for each (x_{1}, x_{2}) ∈ Ω_{1} ×Ω_{2}. In other words, the product of two discrete probability spaces P_{1}, P_{2} is a new probability space that describes the operation of picking an element at random from P_{1} and P_{2} independently.

3.2 Probabilistic Automata

Definition 1. A probabilistic automaton M consists of four components: a set states(M) of states, a nonempty set start(M) ⊆ states(M) of start states, an action signature sig(M) = (ext(M), int(M)) where ext(M) and int(M) are disjoint sets of external and internal actions, respectively, and a transition relation

trans(M) ⊆ states(M) × Probs((acts(M) × states(M)) ∪ {δ}),

where acts(M) denotes the set ext(M) ∪ int(M) of actions.

A probabilistic automaton M is simple if for each transition (s, P) of trans(M) there is an action a of acts(M) such that Ω ⊆ {a}×states(M). In such a case a transition can be represented alternatively as (s, a, P′) where P′ ∈ Probs(states(M)), and it is called a simple transition with action a.

A probabilistic automaton is fully probabilistic if it has a unique start state and from each state there is at most one transition enabled. □

Thus a probabilistic automaton differs from an automaton in that the action and the next state of a given transition are chosen probabilistically. The symbol δ that can appear in the sample space of each transition represents those situations where a system deadlocks. Thus, for example, it is possible that from a state s a probabilistic automaton performs some action with probability p and deadlocks with probability 1 − p.

A simple probabilistic automaton does not allow any kind of probabilistic choice on actions. Once a transition is chosen, then the next action is determined and the next state is given by a random distribution.

A fully probabilistic automaton is a probabilistic automaton without nondeterminism; at each point only one transition can be chosen.

An ordinary automaton is a special case of a probabilistic automaton where each transition leads to a Dirac distribution; the generative model of probabilistic processes of [6] is a special case of a fully probabilistic automaton; simple probabilistic automata are partially captured by the reactive model of [6] in the sense that the reactive model assumes some form of nondeterminism between different actions. However, the reactive model does not allow nondeterministic choices between transitions involving the same action. By restricting simple probabilistic automata to have finitely many states, we obtain objects with a structure similar to that of the Concurrent Labeled Markov Chains of [8]; however, in our model we do not need to distinguish between nondeterministic and probabilistic states. In our model nondeterminism is obtained by means of the structure of the transition relation. This allows us to retain most of the traditional notation that is used for automata.

Definition 2. An execution fragment α of a probabilistic automaton M is a (finite or infinite) sequence of alternating states and actions starting with a state and, if the execution fragment is finite, ending in a state, α = s_{0}a_{1}s_{1}a_{2}s_{2} ⋯, where for each i there exists a probability space P such that (s_{i}, P) ∈ trans(M) and (a_{i+1}, s_{i+1}) ∈ Ω. Denote by frag^{∗}(M) and frag(M) the sets of finite and all executions fragments of M, respectively. An execution is an execution fragment whose first state is a start state. Denote by exec^{∗}(M) and exec(M) the sets of finite and all executions of M, respectively.

An extended execution (fragment) of M is either an execution fragment of M, or a sequence α = s_{0}a_{1}s_{1} ⋯ a_{n}s_{n}δ such that s_{0}a_{1}s_{1} ⋯ a_{n}s_{n} is an execution (fragment) of M. □

Even though we have defined executions for a probabilistic automaton, for the study of the probabilistic behavior of a probabilistic automaton, some more detailed structure is needed. Such a structure, which we call a probabilistic execution, is introduced in Section 3.3.

The next definition shows how it is possible to combine several transitions of a probabilistic automaton into a new one. Informally, a combined transition leaving from a state s is obtained by choosing a transition that leaves from s probabilistically, and then behaving according to the transition chosen. Combined transitions play a fundamental role for the definition of probabilistic adversaries and the definition of our probabilistic simulations.

Definition 3. Given a probabilistic automaton M, a finite or countable set {P_{i}}_{i} of probability distributions of Probs((acts(M)×states(M))∪{δ}), and a weight p_{i} > 0 for each i such that ∑_{i} p_{i} ≤ 1, the combination ∑_{i} p_{i}P_{i} of the distributions {P_{i}}_{i} is the probability space P such that

∘ Ω = \{ \begin{matrix}∪_{i}Ω_{i} & if ∑_{i} p_{i} = 1 \\ ∪_{i}Ω_{i} ∪ \{δ\} & if ∑_{i} p_{i} < 1 \end{matrix}

∘ F = 2^{Ω}

∘ for each (a, s) ∈ Ω, P [(a, s)] = ∑_{{i|(a,s)∈Ω_{i}}} p_{i}P_{i}[(a, s)]

∘ if δ ∈ Ω, then P [δ] = (1 − ∑_{i} p_{i}) + ∑_{{i|δ∈Ω_{i}}} p_{i}P_{i}[δ]. A pair (s, P) is a combined transition of M if there exists a finite or countable family of transitions {(s, P_{i})}_{i} and a set of positive weights {p_{i}}_{i} with ∑_{i} p_{i} ≤ 1, such that P = ∑_{i} p_{i}P_{i}. Denote by ctrans(M) the set of combined transitions of M. □

For notational convenience we write s ⟶^{a} P whenever there is a simple transition (s, a, P) in M, and we write s ⟶^{a}_{C} P whenever there is a simple combined transition (s, a, P) in M. We write s ⟶^{a} whenever there exists a probability space P such that s ⟶^{a} P.

We now turn to the parallel composition operator, which is defined in the CSP style [11], i.e., by synchronizing two automata on their common actions. As outlined in [8], it is not clear how to define a parallel composition operator for general probabilistic automata that extends the CSP operator of ordinary automata; thus, we only define it for simple probabilistic automata.

Definition 4. Two simple probabilistic automata M_{1} and M_{2} are compatible if

(1) int(M_{1}) ∩ acts(M_{2}) = ∅, and

(2) int(M_{2}) ∩ acts(M_{1}) = ∅.

The parallel composition M_{1}∥M_{2} of compatible simple probabilistic automata M_{1} and M_{2} is the simple probabilistic automaton M such that (1) states(M) = states(M_{1}) × states(M_{2})

(2) start(M) = start(M_{1}) × start(M_{2})

(3) ext(M) = ext(M_{1}) ∪ ext(M_{2})

(4) int(M) = int(M_{1}) ∪ int(M_{2})

(5) ((s_{1}, s_{2}), a, P) ∈ trans(M) iff P = P_{1} ⊗ P_{2}, such that

(a) if a ∈ acts(M_{1}) then (s_{1}, a, P_{1}) ∈ trans(M_{1}), else P_{1} = D(s_{1}), and

(b) if a ∈ acts(M_{2}) then (s_{2}, a, P_{2}) ∈ trans(M_{2}), else P_{2} = D(s_{2}). □

Our analysis in this paper will focus on simple probabilistic automata, and we use general probabilistic automata only for the analysis of probabilistic schedulers. Several systems can be described as simple probabilistic automata. A probabilistic Turing Machine where we assume that each cell of the random tape is instantiated when it is read for the first time is a simple probabilistic automaton with a unique action, say τ, whose states are the instantaneous descriptions of the given machine; an algorithm that at some point can flip a coin or roll a dice can be represented as a simple probabilistic automaton where the flipping and rolling operations are simple transitions. If the outcome of a coin flip or dice roll affects the external behavior of the automaton, then the flip and roll actions can be followed by simple transitions whose actions represent the outcome of the random choice. We emphasize that if we introduce an input/output distinction as in [20], then it is possible to compose general probabilistic automata under the conditions that their input actions appear only in simple transitions. A similar observation appears in [31].

3.3 Schedulers and Adversaries

Several papers in the literature use schedulers, sometimes viewed as adversarial entities, to resolve the nondeterminism in probabilistic systems [5, 8, 17, 30]. An adversary (or scheduler) is an object that schedules the next transition based on the past history of a probabilistic automaton. The next transition can be chosen probabilistically.

Definition 5. An adversary for a probabilistic automaton M is a function A taking a finite execution fragment α of M and returning a combined transition of M that leaves from lstate(α). Formally, A : frag^{∗}(M) → ctrans(M) such that if A(α) = (s, P), then s = lstate(α). An adversary is deterministic if on input α it returns either transitions of M or the pair (lstate(α), D(δ)), i.e., the next transition is chosen deterministically. Denote the set of adversaries for a probabilistic automaton M by Advs(M). □

Observe that δ can appear in the combined transitions chosen by an adversary. Such an option is useful when the actions enabled from some state are meant to model input from the external environment and the adversary plays the role of an environment that is not providing any input.

Definition 6. An adversary schema for a probabilistic automaton M, denoted by Advs, is a subset of Advs(M). If Advs is a proper subset of Advs(M) then Advs is a restricted adversary schema, otherwise Advs is a full adversary schema. □

Adversary schemas are used to reduce the power of a class of adversaries. Note, for example, that the set of deterministic adversaries is an example of a restricted adversary schema whenever M is not fully probabilistic. Other examples of restricted adversary schemas are sets of adversaries that base their choices only on partial knowledge of the past history. We refer the reader to [1, 19] for examples of analysis of distributed algorithms based on restricted adversary schemas.

In this paper, in order to guarantee some minimal liveness, we impose a different restriction on our adversaries. Specifically, we denote by Padvs(M) the adversary schema where each adversary can choose δ with a non-zero probability on input α iff there is no transition enabled in M from lstate(α), and we denote by Dadvs(M) the set of deterministic adversaries of Padvs(M). In other words, our adversaries must schedule something whenever something can be scheduled.

We next define what it means for a probabilistic automaton to run under the control of an adversary. Namely, suppose that M has already performed some finite execution fragment α and that an adversary A starts resolving the nondeterminism at that point. The result of the interaction between M and A is a fully probabilistic automaton, called a probabilistic execution, where at each point the only transition enabled is the transition due to the choice of A. A similar construction appears in [30]. Unfortunately, the definition of a probabilistic execution is not simple since each state contains the past history of M.

Definition 7. A probabilistic execution fragment H of a probabilistic automaton M is a fully probabilistic automaton such that

(1) states(H) ⊆ frag^{∗}(M).

(2) for each transition (α, P) of H there exists a combined transition (lstate(α), P′) of M, called the corresponding combined transition, such that

Ω′ = {(a, s)|(a, αas) ∈ Ω} ∪ ({δ} ∩ Ω), and

P′[(a, s)] = P [(a, αas)]

for each (a, s) ∈ Ω′. If q = lstate(α), then denote P by P_{q}^{H} and denote (α, P) by tr_{q}^{H}.

(3) each state of H is reachable and enables one transition. A probabilistic execution of M is a probabilistic execution fragment of M whose start state is a start state of M. □

Condition (1) says that the states of a probabilistic execution H contain the past history of M; Condition (2) ensures that the transitions of H are derived from transitions of M by including the history in the new states that are reached; Condition (3) is just technical to eliminate useless states and to handle δ uniformly. Observe that a state q may enable a transition (q, D(δ)).

Now we can define formally what it means for a probabilistic automaton M to run under the control of an adversary A.

Definition 8. Given a probabilistic automaton M, an adversary A for M, and a finite execution fragment α of M, the execution H(M, A, α) of M under adversary A with starting fragment α is the unique probabilistic execution fragment of M whose start state is α and such that for each state q, if (q, P) ∈ trans(H(M, A, α)), then the corresponding combined transition of (q, P) is A(q). □

3.4 Events

We define a probability space (Ω_{H}, F_{H}, P_{H}) for each probabilistic execution fragment H, so that it is possible to analyze the probabilistic behavior of a probabilistic automaton once the nondeterminism is removed. This construction is slightly different from the construction presented in [28].

First of all, we observe that there is a strong correspondence between the extended execution fragments of a probabilistic automaton and the extended executions of one of its probabilistic execution fragments. We express this correspondence by means of an operator α↑q_{0}^{H} that takes an extended execution fragment of M and gives back the corresponding extended execution of H, and α↓ that takes an extended execution of H and gives back the corresponding extended execution fragment of M.

Then, the sample space Ω_{H} can be defined as the set of extended executions of M that correspond to complete extended execution fragments of H, where an extended execution α of H is complete iff it is either infinite or α = α′δ and δ ∈ Ω_{lstate(α′)}^{H}. For each finite extended execution fragment α of M, let C_{α}, the cone with prefix α, be the set {α′ ∈ Ω_{H} | α ≤ α′}, and let C_{H} be the class of cones for H. The probability μ_{H}(C_{α}) of the cone C_{α} is the product of the probabilities associated with each edge that generates α in H. Formally, let q_{0} be the start state of H,

and let s_{0} be lstate(q_{0}). If α = q_{0}⌢s_{0}a_{1}s_{1} ⋯ s_{n−1}a_{n}s_{n}, then μ_{H}(C_{α}) =^{△}

P_{q_{0}}^{H}[(a_{1}, q_{1})] ⋯ P_{q_{n−1}}^{H}[(a_{n}, q_{n})], where each q_{i} is q_{0}⌢s_{0}a_{1}s_{1} ⋯ a_{i}s_{i}, and if α =

q_{0}⌢s_{0}a_{1}q_{1} ⋯ q_{n−1}a_{n}q_{n}δ, then μ_{H}(C_{α}) =^{△} P_{q_{0}}^{H}[(a_{1}, q_{1})] ⋯ P_{q_{n−1}}^{H}[(a_{n}, q_{n})]P_{q_{n}}^{H}[δ],

where each q_{i} is defined as before. In [27] it is shown that there is a unique measure μ̄_{H} that extends μ_{H} to the σ-field σ(C_{H}) generated by C_{H}, i.e., the smallest σ-field that contains C_{H}. F_{H} is then obtained from σ(C_{H}) by extending each event with any set of extended executions taken from 0probability cones, and P_{H} is obtained by extending μ̄_{H} to F_{H} in the obvious way. With this definition it is possible to show that any union of cones (even uncountable) is measurable. In fact, at most countably many cones have a non-zero measure.

Examples of events are the occurrence of a specific finite execution α, which is C_{α}, and the occurrence of a specific action a, which can be represented as the union of cones C_{α} such that action a occurs in α.

In our analysis of probabilistic automata we are not interested in events for specific probabilistic executions. Whenever we want to express a property, we want to express it relative to any probabilistic execution. This is the purpose of event schemas.

Definition 9. An event schema e for a probabilistic automaton M is a function that associates an event of F_{H} with each probabilistic execution fragment H of M. □

An example of an event schema is the function that associates with each probabilistic execution fragment H the event of performing a specific action a.

4. Probabilistic Computation Tree Logic

In this section we present the logic that is used for our analysis, and we give it a semantics based on our model. It is a simplification of the Timed Probabilistic concurrent Computation Tree Logic (TPCTL) of [8], where, unlike in [8], we do not consider time issues. Then, we show that randomized adversaries do not change the distinguishing power of the logic.

Consider a set of actions ranged over by a. The syntax of PCTL formulas is defined as follows:

f ::= a | ¬f | f_{1} ∧ f_{2} | J Af
f_{1} EU_{≥p} f_{2} | f_{1} AU_{≥p} f_{2} | f_{1} EU_{>p} f_{2} | f_{1} AU_{>p} f_{2}

Informally, the atomic formula a means that action a is the only one that can occur during the first transition of a probabilistic automaton and that action a must indeed occur; the formula J Af means that f is valid for a probabilistic automaton M after making the first transition invisible; the formula f_{1} EU_{≥p} f_{2} means that there exists an adversary such that the probability of f_{2} eventually holding and f_{1} holding till f_{2} holds is at least p; the formula f_{1} AU_{≥p} f_{2} means that the same property as above is valid for each adversary. For example, the property that under any scheduling policy action a occurs eventually with probability at least 1/2 is expressed by the formula true AU_{≥1/2} a, where true can be expressed by the formula ¬(a∧¬a). For the formal semantics of PCTL we need two auxiliary operators on probabilistic automata.

Let M be a probabilistic automaton, a an action of M, and s a state of M. Then M[(a, s)] is a probabilistic automaton obtained from M by adding a new state s′, adding a new transition (s′, a, D(s)), and making s′ into the unique start state. In other words M[(a, s)] forces M to start with action a and then reach state s.

Let M be a probabilistic automaton. Then M^{→} is obtained from M by adding a duplicate of each start state, by making the duplicate states into the new start states, and, for each transition s ⟶^{a} P of M where s is a start state, by adding a transition s′ ⟶^{τ} P from the duplicate s′ of s, where τ is an internal action that cannot occur in any PCTL formula. In other words M^{→} makes sure that the first transition of M is invisible.

Let M be a probabilistic automaton, and let α be an extended execution of M. Let ⊒ denote either ≥ or >. Let an execution α of M be complete iff either it is infinite or it is finite and no transition is enabled in M from lstate(α). Then we define the satisfaction relations M ⊧ f and α ⊧_{M} g as follows

M ⊧ a  iff each complete execution of M

starts with action a,

M ⊧ ¬f  iff not M ⊧ f,
M ⊧ f_{1} ∧ f_{2}  iff M ⊧ f_{1} and M ⊧ f_{2},
α ⊧_{M} f_{1} U f_{2}  iff there is n > 0 such that α = s_{0}a_{1}s_{1} ⋯ a_{n}s_{n}⌢α′,

for each i, 1 ≤ i < n, M[(a_{i}, s_{i})] ⊧ f_{1},

and M[(a_{n}, s_{n})] ⊧ f_{2},

M ⊧ J Af  iff M^{→}⊧ f,
M ⊧ f_{1} EU_{⊒p} f_{2} iff there exists an adversary A and a start state s_{0}

such that P_{H}[e_{f_{1}Uf_{2}}(H)] ⊒ p,

where H = H(M, A, s_{0}), and e_{f_{1}Uf_{2}}(H) is the set of elements α′ of Ω_{H} such that α′ ⊧_{M} f_{1} U f_{2},

M ⊧ f_{1} AU_{⊒p} f_{2} iff for each adversary A and each start state s_{0},

P_{H}[e_{f_{1}Uf_{2}}(H)] ⊒ p,

where H = H(M, A, s_{0}), and e_{f_{1}Uf_{2}}(H) is the set of elements α′ of Ω_{H} such that α′ ⊧_{M} f_{1} U f_{2}.

Note that for each probabilistic execution H the set e_{f_{1}Uf_{2}}(H) can be expressed as a union of cones, and thus it is an element of F_{H}. This guarantees that the semantics of PCTL is well defined.

In the definition above we did not mention explicitly what kind of adversaries to consider for the validity of a formula. In [8] the adversaries are assumed to be deterministic. However, the semantics does not change by adding randomization to the adversaries. The intuitive justification of this claim is that if we are just interested in upper and lower bounds to the probability of some event, then any probabilistic combination of events stays within the bounds. Moreover, deterministic adversaries are sufficient to observe the bounds.

Theorem 1. For each probabilistic automaton M and each PCTL formula f, M ⊧ f relative to Dadvs(M) iff M ⊧ f relative to Padvs(M).

Proof sketch. The proof is by induction on the structure of the formula f, and most of it is simple routine checking. Two critical points are the following: if M ⊧ f_{1} EU_{⊒p} f_{2} relative to randomized adversaries, then we need to make sure that there exists at least a deterministic adversary that can be used to satisfy f_{1} EU_{⊒p} f_{2}; if M ⊧ f_{1} AU_{⊒p} f_{2} relative to deterministic adversaries, then we need to make sure that no probabilistic adversary would lead to a violation of f_{1} AU_{⊒p} f_{2}. In both cases the idea is to convert a probabilistic adversary A for a probabilistic automaton M into a deterministic one such that the probability of e_{f_{1}Uf_{2}} is increased (first case) or decreased (second case). The conversion is shown in [27]. □

We now show how to change the syntax and semantics of PCTL to abstract from internal computation. The new logic is denoted by WPCTL.

The syntax of WPCTL is the same as that of PCTL with the additional requirement that no internal action can occur in a formula. For the semantics of WPCTL, there are three main changes.

M ⊧ a  iff each complete extended execution of M has at least

one external action, and its first external action is a,

α ⊧_{M} f_{1} U f_{2} iff there exists n > 0 such that α = s_{0}a_{1}s_{1} ⋯ a_{n}s_{n}⌢α′,

a_{n} is external, M[(a_{n}, s_{n})] ⊧ f_{2}, and for

each i, 1 ≤ i < n, if a_{i} is external, then M[(a_{i}, s_{i})] ⊧ f_{1},

M ⊧ J Af  iff M^{⇒}⊧ f,

where M^{⇒} hides the first external transitions of M, i.e., it is obtained from M by duplicating all its states (and then removing the non-reachable ones at the end), by making the duplicates of the old start states into the new start states, by reproducing all the internal transitions in the duplicated states, and, for each external transition (s, a, P) of M, by adding an internal transition (s′, τ, P) from the duplicate s′ of s, where τ is a new internal action. Note that the satisfaction relation for an execution is defined solely in terms of its external transitions.

Theorem 2. For each probabilistic automaton M and each WPCTL formula f, M ⊧ f relative to Dadvs(M) iff M ⊧ f relative to Padvs(M).

5. Strong Relations

In this section we analyze relations that are sensitive to internal computation. We formalize in our model the bisimulations of [16] (strong bisimulation) following the lines of [8], and the simulations of [13, 16] (strong simulation); then, we show that strong bisimulation preserves PCTL and that strong simulation preserves PCTL formulas that do not contain negation and EU_{⊒p}. We then introduce two other coarser relations that allow probabilistic combination of transitions and continue to preserve PCTL formulas and PCTL formulas without negation and EU_{⊒p}, respectively. For convenience, throughout the rest of this paper we assume that no pair of probabilistic automata has any state in common.

Definition 10. Let R be an equivalence relation over a set X. Two probability spaces (Ω_{1}, F_{1}, P_{1}) and (Ω_{2}, F_{2}, P_{2}) of Probs(X) are R-equivalent, written (Ω_{1}, F_{1}, P_{1}) ≡_{R} (Ω_{2}, F_{2}, P_{2}), iff for every class C of X/ R,

∑_{x∈Ω_{1}∩C} P_{1}[x] = ∑_{x∈Ω_{2}∩C} P_{2}[x].

In other words (Ω_{1}, F_{1}, P_{1}) and (Ω_{2}, F_{2}, P_{2}) are R-equivalent if they assign the same probability measure to each equivalence class of R. □

Definition 11. A strong bisimulation between two simple probabilistic automata M_{1} and M_{2} is an equivalence relation R over states(M_{1})∪states(M_{2}) such that

(1) each start state of M_{1} is related to at least one start state of M_{2}, and vice versa;

(2) for each s_{1} R s_{2} and each transition s_{1} ⟶^{a} P_{1} of either M_{1}, M_{2}, there exists a transition s_{2} ⟶^{a} P_{2} of either M_{1}, M_{2} such that P_{1} ≡_{R} P_{2}.

We write M_{1} ≃ M_{2} whenever acts(M_{1}) = acts(M_{2}) and there is a strong bisimulation between M_{1} and M_{2}. □

Condition 2 of Definition 11 is stated in [16] in a different but equivalent way, i.e., for each equivalence class [x] of R, the probabilities of reaching [x] from s_{1} and s_{2} are the same. Strong bisimulation coincides with the strong bisimulation of [22, 24] whenever the involved probabilistic automata represent ordinary automata.

The next definition is used to introduce strong simulations. A similar definition appears in [13]. Informally, (Ω_{1}, F_{1}, P_{1}) ⊑_{R} (Ω_{2}, F_{2}, P_{2}) means that there is a way to split the probabilities of the states of Ω_{1} between the states of Ω_{2} and vice versa, expressed by a function w, so that the relation R is preserved. In other words the left probability space can be embedded into the right one up to R.

Definition 12. Let R⊆ X × Y be a relation between two set X, Y, and let (Ω_{1}, F_{1}, P_{1}) and (Ω_{2}, F_{2}, P_{2}) be two probability spaces of Probs(X) and Probs(Y), respectively. Then (Ω_{1}, F_{1}, P_{1}) and (Ω_{2}, F_{2}, P_{2}) are in relation ⊑_{R}, written (Ω_{1}, F_{1}, P_{1}) ⊑_{R} (Ω_{2}, F_{2}, P_{2}), iff there exists a function w : X × Y → [0, 1] such that

(1) for each x ∈ X, ∑_{y∈Y} w(x, y) = P_{1}[x],

(2) for each y ∈ Y, ∑_{x∈X} w(x, y) = P_{2}[y],

(3) for each (x, y) ∈ X × Y, if w(x, y) > 0 then x R y. The function w is called a weight function. □

Definition 13. A strong simulation between two simple probabilistic automata M_{1} and M_{2} is a relation R⊆ states(M_{1}) × states(M_{2}) such that (1) each start state of M_{1} is related to at least one start state of M_{2};

(2) for each s_{1} R s_{2} and each transition s_{1} ⟶^{a} P_{1} of M_{1}, there exists a transition s_{2} ⟶^{a} P_{2} of M_{2} such that P_{1} ⊑_{R} P_{2}.

(3) for each s_{1} R s_{2}, if s_{2} ⟶^{a}, then s_{1} ⟶^{a}.

We write M_{1} ⊑_{SS} M_{2} whenever acts(M_{1}) = acts(M_{2}) and there is a strong simulation between M_{1} and M_{2}. The kernel of strong simulation is denoted by ≡_{SS}. □

If we do not include Condition 3 in the definition of a strong simulation, then we obtain a relation that extends the strong simulation relation of ordinary automata. Here we add Condition 3 to guarantee some minimum liveness requirements, thus extending the 2/3-bisimulation relation of [16]. Condition 3 is fundamental for the preservation of PCTL formulas; however it can be relaxed by requiring s_{1} to enable some transition whenever s_{2} enables some transition.

Proposition 1. ≃ and ⊑_{SS} are compositional. That is, for each M_{1} and M_{2} such that acts(M_{1}) = acts(M_{2}), and for each M_{3} compatible with both M_{1} and M_{2}, if M_{1} ≃ M_{2}, then M_{1}∥M_{3} ≃ M_{2}∥M_{3}, and if M_{1} ⊑_{SS} M_{2}, then M_{1}∥M_{3} ⊑_{SS} M_{2}∥M_{3}. □

Lemma 1. Let X, Y be two disjoint sets, R be an equivalence relation on X ∪ Y, and let P_{1} and P_{2} be probability spaces of Probs(X) and Probs(Y), respectively, such that P_{1} ≡_{R} P_{2}. Then P_{1} ⊑_{R′} P_{2}, where R′=R ∩X × Y.

Lemma 1 can be used to prove directly that bisimulation is finer than simulation. The same observation applies to all the other pairs of relations that we define in this paper.

Theorem 3. Let M_{1} and M_{2} be two simple probabilistic automata, and let f be a PCTL formula.

(1) If M_{1} ≃ M_{2}, then M_{1} ⊧ f iff M_{2} ⊧ f.

(2) If M_{1} ⊑_{SS} M_{2} and f does not contain any occurrence of ¬ and EU_{⊒p}, then M_{2} ⊧ f implies M_{1} ⊧ f.

Proof sketch. The proofs are by induction on the structure of f, where the nontrivial step is the analysis of f_{1} AU_{⊒p} f_{2} and f_{1} EU_{⊒p} f_{2}. In the first case it is enough to show that for each probabilistic execution H_{1} of M_{1} obtainable from some adversary there exists a probabilistic execution H_{2} of M_{2}, obtainable from some adversary, such that P_{H_{2}}[e_{f_{1}Uf_{2}}(H_{2})] ≤ P_{H_{1}}[e_{f_{1}Uf_{2}}(H_{1})]. In the second case we need to make sure that P_{H_{2}}[e_{f_{1}Uf_{2}}(H_{2})] = P_{H_{1}}[e_{f_{1}Uf_{2}}(H_{1})].

The probabilistic execution H_{2} is built by reproducing the structure of H_{1} via R. We also need to ensure that H_{2} is obtainable from some adversary, and for this part we need Condition 3 of Definition 13. Indeed, if δ occurs in a transition enabled from a state q of H_{2}, then there is some state q′ of H_{1} that corresponds to q via R and that contains δ in the transition that it enables. Then, lstate(q′) does not enable any transition in M_{2}, which, using

Fig. 1: Strong simulations do not preserve EU_{⊒p}.

Fig. 2: Probabilistic combination of transitions is useful.

Condition 3, means that lstate(q) does not enable any transition in M_{2}. We do not need to show that H_{2} can be generated by a deterministic adversary (indeed this is false in general) because of Theorem 1. The correspondence between H_{1} and H_{2} is called an execution correspondence structure and it is shown to exist in [27]. Once an execution correspondence structure is built, it is easy to show that P_{H_{2}}[e_{f_{1}Uf_{2}}(H_{2})] ≤ P_{H_{1}}[e_{f_{1}Uf_{2}}(H_{1})] if R is a strong simulation, and that P_{H_{2}}[e_{f_{1}Uf_{2}}(H_{2})] = P_{H_{1}}[e_{f_{1}Uf_{2}}(H_{1})] if R is a strong bisimulation. □

Example 1. PCTL formulas with occurrences of EU_{⊒p} are not preserved in general by ≡_{SS}. Consider the two simple probabilistic automata of Figure 1. The two probabilistic automata are strong simulation equivalent by matching each s_{i} with s′_{i} and by matching s_{2}, s_{6}, s_{7}, s_{10} to s′_{1}, s′_{3}, s′_{4}, s′_{8}, respectively. However, the right probabilistic automaton satisfies true AU_{≥1} (a ∧ (true EU_{≥1/2} c)), whereas the left probabilistic automaton does not. □

Example 2. Consider the two probabilistic automata of Figure 2, where s_{0}, s′_{0} are the start states, s_{1}, s′_{1} enable some transition with action b, and s_{2}, s′_{2} enable some transition with action c. The difference between the left and right probabilistic automata is that the right probabilistic automaton enables an additional transition which is obtained by combining the two transitions of the left probabilistic automaton. Thus, the two probabilistic automata satisfy the same PCTL formulas; however, there is no simulation from the right probabilistic automaton to the left one since the middle transition cannot be reproduced. □

Example 2 suggests two coarser relations where it is possible to combine several transitions into a unique one. Note that the only difference between the new preorders and the old ones is the use of ⟶^{a}_{C} (combined transitions) instead of ⟶^{a} (regular transitions) in Condition 2.

Definition 14. A strong probabilistic bisimulation between two simple probabilistic automata M_{1} and M_{2} is an equivalence relation R over states(M_{1})∪ states(M_{2}) such that

(1) each start state of M_{1} is related to at least one start state of M_{2}, and vice versa;

(2) for each s_{1} R s_{2} and each transition s_{1} ⟶^{a} P_{1} of either M_{1}, M_{2}, there exists a combined transition s_{2} ⟶^{a}_{C} P_{2} of either M_{1}, M_{2} such that P_{1} ≡_{R} P_{2}.

We write M_{1} ≃_{P} M_{2} whenever acts(M_{1}) = acts(M_{2}) and there is a strong probabilistic bisimulation between M_{1} and M_{2}. □

Definition 15. A strong probabilistic simulation between two simple probabilistic automata M_{1} and M_{2} is a relation R⊆ states(M_{1})×states(M_{2}) such that

(1) each start state of M_{1} is related to at least one start state of M_{2};

(2) for each s_{1} R s_{2} and each transition s_{1} ⟶^{a} (Ω_{1}, F_{1}, P_{1}) of M_{1}, there exists a combined transition s_{2} ⟶^{a}_{C} (Ω_{2}, F_{2}, P_{2}) of M_{2} such that (Ω_{1}, F_{1}, P_{1}) ⊑_{R} (Ω_{2}, F_{2}, P_{2}).

(3) for each s_{1} R s_{2}, if s_{2} ⟶^{a}, then s_{1} ⟶^{a}. We write M_{1} ⊑_{SPS} M_{2} whenever acts(M_{1}) = acts(M_{2}) and there is a strong probabilistic simulation between M_{1} and M_{2}. The kernel of strong probabilistic simulation is denoted by ≡_{SPS}. □

Proposition 2. ≃_{P} and ⊑_{SPS} are compositional. □

Theorem 4. Let M_{1} and M_{2} be two simple probabilistic automata, and let f be a PCTL formula.

(1) If M_{1} ≃_{P} M_{2}, then M_{1} ⊧ f iff M_{2} ⊧ f.

(2) If M_{1} ⊑_{SPS} M_{2} and f does not contain any occurrence of ¬ and EU_{⊒p}, then M_{2} ⊧ f implies M_{1} ⊧ f. □

Even strong probabilistic bisimulations and strong probabilistic simulations are a generalization of the strong bisimulation and simulation relations of ordinary automata. In fact, if a transition of M_{1} leading to a Dirac distribution can be simulated by a combined transition of M_{2}, then the same transition of M_{1} can be simulated by a non-combined transition of M_{2}, which leads to a Dirac distribution if we are dealing with ordinary automata.

Remark 1. Strong probabilistic simulations provide us with a simple way to represent the closed interval specification systems of [13]. A probabilistic specification system of [13] is a state machine where each state is associated with a set of probability distributions over the next state. The set of probability distributions for a state s is specified by associating each state s′ with a set of probabilities that can be used from s. In our framework a specification structure can be represented as a probabilistic automaton that, from each state, enables one transition for each one of the probability distributions over the next states that are allowed. A probabilistic process system is a “fully probabilistic” (in our terms) probabilistic specification system. A probabilistic process system P is said to satisfy a probabilistic specification system S if there exists a strong simulation from P to S.

A closed interval specification system is a specification system whose set of probability distributions is described by means of a lower bound and an upper bound, for each pair (s, s′), on the probability of reaching s′ from s. Thus, the set of probability distributions that are allowed from any state form a polytope. By using our strong probabilistic simulation as satisfaction relation, it is possible to represent each polytope by means of its corners only. Any point within the polytope is given by a combination of the corners. □

6. Weak Transitions

The relations of Section 5 do not abstract from internal computation, while in practice a notion of implementation should ignore the internal transitions of a system as much as possible. In order to do so, we extend our arrow notation in a way similar to the non-probabilistic case [22]. We define the weak arrows ⟹^{a} and ⟹^{a}_{C} to state that a probability distribution over states P is reached through a sequence of transitions of M, some of which are internal. The main difference from the non-probabilistic case is that in our framework the transitions involved form a tree rather than a linear chain. Formally, s ⟹^{a} P, where a is either an external action or the empty sequence and P is a probability distribution over states, iff there is a probabilistic execution fragment H such that

(1) the start state of H is s;

Fig. 3: A representation of a weak transition with action a.

(2) P_{H}[{αδ | αδ ∈ Ω_{H}}] = 1, i.e., the probability of termination in H is 1;

(3) for each αδ ∈ Ω_{H}, trace(α) = a;

(4) Ω = {lstate(α) | αδ ∈ Ω_{H}}, and for each element s′ of Ω, P [s′] = ∑_{αδ∈Ω_{H}|lstate(α)=s′} P_{H}[C_{αδ}];

(5) for each state q of H, either tr_{q}^{H} is the pair (lstate(q), D(δ)), or the transition that corresponds to tr_{q}^{H} is a transition of M.

A weak combined transition, s ⟹^{a}_{C} P, is defined as a weak transition by dropping Condition 5.

Example 3. The diagram of Figure 3 represents graphically a weak transition with action a that leads to state s_{1} with probability 5/12 and to state s_{2} with probability 7/12. We do not represent the states as finite execution fragments since their position in the diagram gives enough information. Similarly, we do not represent δ explicitly. The action τ represents any internal action. From the formal definition of a weak transition, a tree that represents a weak transition may have an infinite branching structure, i.e., it may have transitions that lead to countably many states, and may have some infinite paths; however, each tree representing a weak transition has the property that infinite paths occur with probability 0. This definition of a weak transition is more general than the definition given in [28], where it is required that no infinite path appear in a weak transition. Figure 4 represents a weak transition of a probabilistic automaton with cycles in its transition relation. Specifically, H represents the weak transition s_{0} ⟹ P, where P [s_{0}] = 1/8 and P [s_{1}] = 7/8. If we extend H indefinitely on its right, then we obtain a new probabilistic execution fragment that represents the weak transition s_{0} ⟹ D(s_{1}). Observe that the new probabilistic execution fragment has an infinite path that occurs with probability 0. Furthermore, observe that there is no other way to reach state s_{1} with probability 1. □

Fig. 4: A weak transition of a probabilistic automaton with cycles.

7. Weak Relations

In this section we study the weak versions of the relations of Section 5, and we show how they relate to WPCTL. We introduce only the probabilistic version of each relation, since the others can be derived subsequently in a straightforward way. We start by presenting the natural extension of the probabilistic relations of Section 5; then, in order to preserve WPCTL, we introduce a branching version of the new relations using the basic idea of branching bisimulation [7].

Weak probabilistic bisimulations and weak probabilistic simulations can be defined in a straightforward manner by changing Condition 2 of Definitions 14 and 15 so that each transition s_{1} ⟶^{a} P_{1} of a probabilistic au-

tomaton can be simulated by a weak combined transition s_{2} ⟹_{C}^{a⌈ext(M_{2})} P_{2} of the other probabilistic automaton, and by using weak transitions in Condition 3. Even in this case, with the opportune arguments about Condition 3, the weak probabilistic relations are an extension of the corresponding relations for ordinary automata. However, although the two weak relations are compositional, WPCTL formulas are not preserved by weak bisimulations and weak simulations. The key problem is that weakly bisimilar executions do not satisfy the same formulas. Consider the diagram below.

[figure: s_{0}; R; τ; s_{1}; a; f_{1}; s_{2}; τ; s_{3}; τ; s_{4}; R; s′_{0}; a; ?; s′_{1}]

Since s′_{1} and s_{2} are not necessarily related, it is not possible to deduce M[(a, s′_{1})] ⊧ f_{1} from M[(a, s_{2})] ⊧ f_{1}. To solve the problem we need to make sure that s′_{1} and s_{2} are related, and thus we introduce the branching versions of our weak relations.

Definition 16. A branching probabilistic bisimulation between two simple probabilistic automata M_{1} and M_{2} is an equivalence relation R over states(M_{1}) ∪ states(M_{2}) such that (1) each start state of M_{1} is related to at least one start state of M_{2}, and

vice versa;

(2) for each s_{1} R s_{2} and each transition s_{1} ⟶^{a} P_{1} of either M_{1}, M_{2}, there

exists a weak combined transition s_{2} ⟹_{C}^{a⌈ext(M_{2})} P_{2} of either M_{1}, M_{2}

such that P_{1} ≡_{R} P_{2} and s_{2} ⟹_{C}^{a⌈ext(M_{2})} P_{2} satisfies the branching condition, i.e., there is a probabilistic execution fragment H that represents

s_{2} ⟹_{C}^{a⌈ext(M_{2})} P_{2} such that for each extended execution αδ of Ω_{H} and each occurrence of a state s in α, either

(a) s_{1} R s, a ∈ ext(M_{2}) implies that a has not occurred yet, and each state s′ preceding s in α satisfies s_{1} R s′, or

(b) a ∈ ext(M_{2}) implies that a has occurred, and for each s′_{1} ∈ Ω_{1} such that s′_{1} R lstate(α), s′_{1} R s.

We write M_{1} ≃_{P} M_{2} whenever ext(M_{1}) = ext(M_{2}) and there is a branching probabilistic bisimulation between M_{1} and M_{2}. □

Another way to state the branching condition is the following: there is

a probabilistic execution fragment H that represents s_{2} ⟹_{C}^{a⌈ext(M_{2})} P_{2} such that, viewing H as a tree, all the the states of the tree that occur before action a are related to s_{1}, and whenever a state s′_{2} of Ω_{2} is related to some state s′_{1} of Ω_{1}, then all the states in the path from s_{2} to s′_{2} that occur after action a are related to s′_{1} as well. In other words, each complete path in the tree satisfies the branching condition of [7].

Definition 17. A branching probabilistic simulation between two simple probabilistic automata M_{1} and M_{2} is a relation R⊆ states(M_{1})×states(M_{2}) such that

(1) each start state of M_{1} is related to at least one start state of M_{2};

(2) for each s_{1} R s_{2} and each transition s_{1} ⟶^{a} (Ω_{1}, F_{1}, P_{1}) of M_{1}, there

exists a weak combined transition s_{2} ⟹_{C}^{a⌈ext(M_{2})} (Ω_{2}, F_{2}, P_{2}) of M_{2} such

that (Ω_{1}, F_{1}, P_{1}) ⊑_{R} (Ω_{2}, F_{2}, P_{2}), and s_{2} ⟹_{C}^{a⌈ext(M_{2})} (Ω_{2}, F_{2}, P_{2}) satisfies

the branching condition.

(3) for each s_{1} R s_{2}, if s_{2} ⟹^{a}, then s_{1} ⟹^{a}. We write M_{1} ⊑_{BPS} M_{2} whenever ext(M_{1}) = ext(M_{2}) and there is a branching probabilistic simulation between M_{1} and M_{2}. The kernel of branching probabilistic simulation is denoted by ≡_{BPS}. □

Proposition 3. ≃_{P} and ⊑_{BPS} are compositional. □

To show that WPCTL formulas are preserved by the different simulation relations, we need to guarantee that a probabilistic automaton is free from divergences with probability 1. The definition below allows for a probabilistic automaton to exhibit infinite internal computation, but it requires that such a behavior can happen only with probability 0.

Definition 18. A probabilistic automaton M is probabilistically convergent if for each probabilistic execution H of M and each state q of H, the probability of diverging (performing infinitely many internal actions and no external actions) from q is 0, i.e., P_{H}[Θ_{q}] = 0, where Θ_{q} is the set of infinite executions of H that pass through state q and that do not contain any external action after passing through state q. Note that Θ_{q} is measurable since it is the complement of a union of cones. □

Theorem 5. Let M_{1} and M_{2} be two probabilistically convergent, simple probabilistic automata, and f be a WPCTL formula.

(1) If M_{1} ≃_{P} M_{2}, then M_{1} ⊧ f iff M_{2} ⊧ f.

(2) If M_{1} ⊑_{BPS} M_{2} and f does not contain any occurrence of ¬ and EU_{⊒p}, then M_{2} ⊧ f implies M_{1} ⊧ f.

Proof sketch. Similar to the proof of Proposition 3. Here the construction of H_{2} is much more complicated than in the proof of Proposition 3 due to the fact that we need to combine several weak transitions. Moreover, we need to show that the branching requirement guarantees the preservation of properties between bisimilar executions. □

8. Concluding Remarks

We have extended some of the classical simulation relations to a new probabilistic model that distinguishes naturally between probabilistic and nondeterministic choice and that allows us to represent naturally randomized and/or restricted forms of scheduling policies. Our method of analysis is based on compositionality issues and preservation of PCTL and WPCTL formulas. Throughout the presentation we have shown how our relations are a conservative extension of the corresponding relations defined on ordinary automata. We have observed that the distinguishing power of PCTL does not change if we allow randomization in the schedulers. Based on that, we have introduced a new collection of relations whose main idea is that a probabilistic automaton may combine some of its transitions probabilistically in order to simulate another probabilistic automaton.

In [27] this work is pursued further by extending the trace semantics of ordinary automata to the probabilistic framework. The key issue is compositionality, which is not trivial to achieve. We show that all the simulation relations of this paper are sound for the trace semantics, and we introduce other coarser simulation relations that capture the trace semantics better.

A problem that is still open is to derive adequacy results for PCTL and WPCTL. We do not know whether PCTL and WPCTL are adequate for our probabilistic simulation relations. In the non-probabilistic framework adequate logics for strong bisimulation are studied in [10], and adequate logics for branching bisimulation are studied in [23]. An adequate logic for strong bisimulation in the probabilistic framework is studied in [16]; however, no nondeterminism is present in the formalism of [16].

If PCTL and WPCTL are not adequate, then further research should focus either on finding adequate logics (what other operators do we need?) or finding more appropriate simulation relations. An important question is to determine whether WPCTL is sufficiently powerful to express all the properties of practical interest.

Acknowledgments. Thanks to the anonymous referees for their valuable suggestions on a draft version of this paper. In particular, one of the referees pointed out an error in Theorems 19, 23 and 28 of [28], which we have corrected here.

References

[1] Aggarwal, S. 1994. Time Optimal Self-Stabilizing Spanning Tree Algorithms. Tech. Report MIT/LCS/TR-632, MIT Laboratory for Computer Science.

[2] Aspnes, J. and Herlihy, M.P. 1990. Fast randomized consensus using shared memory. Journal of Algorithms 15, 1 (September), 441–460.

[3] Ben-Or, M. 1983. Another advantage of free choice: completely asynchronous agreement protocols. In Proceedings of the 2^{nd} Annual ACM Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada.

[4] Christoff, I. 1990. Testing Equivalences for Probabilistic Processes. PhD thesis, Department of Computer Science, Uppsala University.

[5] Fischer, M. and Zuck, L. 1988. Reasoning about Uncertainty in Fault Tolerant Distributed Systems. In Proceedings of the Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Volume 331 of Lecture Notes in Computer Science. Springer-Verlag, 142–158.

[6] Glabbeek, R.J. van, Smolka, S.A., Steffen, B., and Tofts, C.M.N. 1990. Reactive, generative, and stratified models of probabilistic processes. In Proceedings 5^{th} Annual Symposium on Logic in Computer Science, Philadelphia, USA. IEEE Computer Society Press, 130–141.

[7] Glabbeek, R.J. van and Weijland, W.P. 1989. Branching Time and Abstraction in Bisimulation Semantics (extended abstract). In Information Processing 89. North-Holland, 613–618.

[8] Hansson, H. 1994. Time and Probability in Formal Design of Distributed Systems. Volume 1 of Real-Time Safety Critical Systems. Elsevier.

[9] Hennessy, M. 1988. Algebraic Theory of Processes. MIT Press, Cambridge, Massachusetts.

[10] Hennessy, M. and Milner, R. 1985. Algebraic Laws for Nondeterminism and Concurrency. Journal of the ACM 32, 1, 137–161.

[11] Hoare, C.A.R. 1985. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs.

[12] Jonsson, B. 1991. Simulations between Specifications of Distributed Systems. In Proceedings of CONCUR 91, Amsterdam, Volume 527 of Lecture Notes in

Computer Science. Springer-Verlag, 346–360.

[13] Jonsson, B. and Larsen, K.G. 1991. Specification and Refinement of Probabilistic Processes. In Proceedings of the 6th IEEE Symposium on Logic in Computer Science. Amsterdam, 266–277.

[14] Jonsson, B. and Parrow, J., Editors. 1994. Proceedings of CONCUR 94, Uppsala, Sweden, Volume 836 of Lecture Notes in Computer Science. Springer-Verlag.

[15] Kushilevitz, E. and Rabin, M. 1992. Randomized Mutual Exclusion Algorithms Revisited. In Proceedings of the 11^{th} Annual ACM Symposium on Principles of Distributed Computing, Quebec, Canada, 275–284.

[16] Larsen, K.G. and Skou, A. 1991. Bisimulation through Probabilistic Testing. Information and Computation 94, 1 (Sept.), 1–28.

[17] Lehmann, D. and Rabin, M. 1981. On the advantage of free choice: a symmetric and fully distributed solution to the dining philosophers problem. In Proceedings of the 8^{th} Annual ACM Symposium on Principles of Programming Languages, 133–138.

[18] 1990. Proceedings 5^{th} Annual Symposium on Logic in Computer Science, Philadelphia, USA. IEEE Computer Society Press.

[19] Lynch, N.A., Saias, I., and Segala, R. 1994. Proving Time Bounds for Randomized Distributed Algorithms. In Proceedings of the 13^{th} Annual ACM Symposium on Principles of Distributed Computing, Los Angeles, CA, 314–323.

[20] Lynch, N.A. and Tuttle., M.R. 1987. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6^{th} Annual ACM Symposium on Principles of Distributed Computing. Vancouver, Canada, 137–151.

[21] Lynch, N.A. and Vaandrager, F.W. 1991. Forward and Backward Simulations for Timing-Based Systems. In Proceedings of the REX Workshop “Real-Time: Theory in Practice”, Volume 600 of Lecture Notes in Computer Science. Springer-Verlag, 397–446.

[22] Milner, R. 1989. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs.

[23] Nicola, R. De and Vaandrager, F. W. 1990. Three Logics for Branching Bisimulation (extended abstract). In Proceedings 5^{th} Annual Symposium on Logic in Computer Science, Philadelphia, USA. IEEE Computer Society Press, 118–129.

[24] Park, D.M.R. 1981. Concurrency and automata on infinite sequences. In 5^{th} GI Conference, Volume 104 of Lecture Notes in Computer Science. Springer-Verlag, 167–183.

[25] Pnueli, A. 1982. The temporal semantics of concurrent programs. Theoretical Computer Science 13, 45–60.

[26] Pnueli, A. and Zuck, L. 1986. Verification of multiprocess probabilistic protocols. Distributed Computing 1, 1, 53–72.

[27] Segala, R. 1995. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, MIT, Dept. of Electrical Engineering and Computer Science.

[28] Segala, R. and Lynch, N.A. 1994. Probabilistic Simulations for Probabilistic Processes. In Proceedings of CONCUR 94, Uppsala, Sweden, Volume 836 of Lecture Notes in Computer Science. Springer-Verlag, 481–496.

[29] Seidel, K. 1992. Probabilistic Communicating Processes. Tech. Report PRG-102, Ph.D. Thesis, Programming Research Group, Oxford University Computing Laboratory.

[30] Vardi, M.Y. 1985. Automatic Verification of Probabilistic Concurrent Finite-State Programs. In Proceedings of 26th IEEE Symposium on Foundations of Computer Science. Portland, OR, 327–338.

[31] Wu, S.H., Smolka, S., and Stark, E.W. 1994. Composition and behaviors of probabilistic I/O automata. In Proceedings of CONCUR 94, Uppsala, Sweden, Volume 836 of Lecture Notes in Computer Science. Springer-Verlag.