We present a spectrum of trace-based, testing, and bisimulation equivalences for nondeterministic and probabilistic processes whose activities are all observable. For every equivalence under study, we examine the discriminating power of three variants stemming from three approaches that differ for the way probabilities of events are compared when nondeterministic choices are resolved via deterministic schedulers. We show that the first approach - which compares two resolutions relatively to the probability distributions of all considered events - results in a fragment of the spectrum compatible with the spectrum of behavioral equivalences for fully probabilistic processes. In contrast, the second approach - which compares the probabilities of the events of a resolution with the probabilities of the same events in possibly different resolutions - gives rise to another fragment composed of coarser equivalences that exhibits several analogies with the spectrum of behavioral equivalences for fully nondeterministic processes. Finally, the third approach - which only compares the extremal probabilities of each event stemming from the different resolutions - yields even coarser equivalences that, however, give rise to a hierarchy similar to that stemming from the second approach.
Two of the most studied extensions of trace and testing equivalences to nondeterministic and probabilistic processes induce distinctions that have been questioned and lack properties that are desirable. Probabilistic trace-distribution equivalence differentiates systems that can perform the same set of traces with the same probabilities, and is not a congruence for parallel composition. Probabilistic testing equivalence, which relies only on extremal success probabilities, is backward compatible with testing equivalences for restricted classes of processes, such as fully nondeterministic proce…
In the paper "Relating Strong Behavioral Equivalences for Processes with Nondeterminism and Probabilities" to appear in TCS, we present a comparison of behavioral equivalences for nondeterministic and probabilistic processes. In particular, we consider strong trace, failure, testing, and bisimulation equivalences. For each of these groups of equivalences, we examine the discriminating power of three variants stemming from three approaches that differ for the way probabilities of events are compared when nondeterministic choices are resolved via deterministic schedulers. The established relatio…
The combination of nondeterminism and probability in concurrent systems lead to the development of several interpretations of process behavior. If we restrict our attention to linear properties only, we can identify three main approaches to trace and testing semantics: the trace distributions, the trace-by-trace and the extremal probabilities approaches. In this paper, we propose novel notions of behavioral metrics that are based on the three classic approaches above, and that can be used to measure the disparities in the linear behavior of processes wrt trace and testing semantics. We study t…
In the study of quantum process algebras, researchers have introduced different notions of equivalence between quantum processes like bisimulation or barbed congruence. However, there are intuitively equivalent quantum processes that these notions do not regard as equivalent. In this paper, we introduce a notion of equivalence named observational equivalence into qCCS. Since quantum processes have both probabilistic and nondeterministic transitions, we introduce schedulers that solve nondeterministic choices and obtain probability distribution of quantum processes. By definition, the restricti…
The $π$-calculus is a process algebra where agents interact by sending communication links to each other via noiseless communication channels. Taking into account the reality of noisy channels, an extension of the $π$-calculus, called the $π_N$-calculus, has been introduced recently. In this paper, we present an early transitional semantics of the $π_N$-calculus, which is not a directly translated version of the late semantics of $π_N$, and then extend six kinds of behavioral equivalences consisting of reduction bisimilarity, barbed bisimilarity, barbed equivalence, barbed congruence, bisimila…
We explore language semantics for automata combining probabilistic and nondeterministic behavior. We first show that there are precisely two natural semantics for probabilistic automata with nondeterminism. For both choices, we show that these automata are strictly more expressive than deterministic probabilistic automata, and we prove that the problem of checking language equivalence is undecidable by reduction from the threshold problem. However, we provide a discounted metric that can be computed to arbitrarily high precision.
We propose behavioral specification theories for most equivalences in the linear-time--branching-time spectrum. Almost all previous work on specification theories focuses on bisimilarity, but there is a clear interest in specification theories for other preorders and equivalences. We show that specification theories for preorders cannot exist and develop a general scheme which allows us to define behavioral specification theories, based on disjunctive modal transition systems, for most equivalences in the linear-time--branching-time spectrum.
Probabilistic automata (PAs) have been successfully applied in formal verification of concurrent and stochastic systems. Efficient model checking algorithms have been studied, where the most often used logics for expressing properties are based on probabilistic computation tree logic (PCTL) and its extension PCTL^*. Various behavioral equivalences are proposed, as a powerful tool for abstraction and compositional minimization for PAs. Unfortunately, the equivalences are well-known to be sound, but not complete with respect to the logical equivalences induced by PCTL or PCTL*. The desire of a b…
We study monads resulting from the combination of nondeterministic and probabilistic behaviour with the possibility of termination, which is essential in program semantics. Our main contributions are presentation results for the monads, providing equational reasoning tools for establishing equivalences and distances of programs.
Stuttering bisimulation is a well-known behavioral equivalence that preserves CTL-X, namely CTL without the next-time operator X. Correspondingly, the stuttering simulation preorder induces a coarser behavioral equivalence that preserves the existential fragment ECTL-{X,G}, namely ECTL without the next-time X and globally G operators. While stuttering bisimulation equivalence can be computed by the well-known Groote and Vaandrager's [1990] algorithm, to the best of our knowledge, no algorithm for computing the stuttering simulation preorder and equivalence is available. This paper presents suc…
In this paper we continue our research line on logical characterizations of behavioral metrics obtained from the definition of a metric over the set of logical properties of interest. This time we provide a characterization of both strong and weak trace metric on nondeterministic probabilistic processes, based on a minimal boolean logic L which we prove to be powerful enough to characterize strong and weak probabilistic trace equivalence. Moreover, we also prove that our characterization approach can be restated in terms of a more classic probabilistic L-model checking problem.
We investigate logics and equivalence relations that capture the qualitative behavior of Markov Decision Processes (MDPs). We present Qualitative Randomized CTL (QRCTL): formulas of this logic can express the fact that certain temporal properties hold over all paths, or with probability 0 or 1, but they do not distinguish among intermediate probability values. We present a symbolic, polynomial time model-checking algorithm for QRCTL on MDPs. The logic QRCTL induces an equivalence relation over states of an MDP that we call qualitative equivalence: informally, two states are qualitatively equiv…
The problem if a given configuration of a pushdown automaton (PDA) is bisimilar with some (unspecified) finite-state process is shown to be decidable. The decidability is proven in the framework of first-order grammars, which are given by finite sets of labelled rules that rewrite roots of first-order terms. The framework is equivalent to PDA where also deterministic (i.e. alternative-free) epsilon-steps are allowed, i.e. to the model for which Sénizergues showed an involved procedure deciding bisimilarity (1998, 2005). Such a procedure is here used as a black-box part of the algorithm. The re…
The weakest pre-expectation calculus has been proved to be a mature theory to analyze quantitative properties of probabilistic and nondeterministic programs. We present an automatic method for proving quantitative linear properties on any denumerable state space using iterative backwards fixed point calculation in the general framework of abstract interpretation. In order to accomplish this task we present the technique of random variable abstraction (RVA) and we also postulate a sufficient condition to achieve exact fixed point computation in the abstract domain. The feasibility of our approa…
Probabilistic transition system specifications (PTSSs) in the $nt μfθ/ ntμxθ$ format provide structural operational semantics for Segala-type systems that exhibit both probabilistic and nondeterministic behavior and guarantee that bisimilarity is a congruence for all operator defined in such format. Starting from the $nt μfθ/ ntμxθ$ format, we obtain restricted formats that guarantee that three coarser bisimulation equivalences are congruences. We focus on (i) Segala's variant of bisimulation that considers combined transitions, which we call here "convex bisimulation"; (ii) the bisimulation e…
In the theory of testing for Markovian processes developed so far, exponentially timed internal actions are not admitted within processes. When present, these actions cannot be abstracted away, because their execution takes a nonzero amount of time and hence can be observed. On the other hand, they must be carefully taken into account, in order not to equate processes that are distinguishable from a timing viewpoint. In this paper, we recast the definition of Markovian testing equivalence in the framework of a Markovian process calculus including exponentially timed internal actions. Then, we …
