Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userReward Testing Equivalences for Processes
243
0
0.0
(
0
)
Added by
Rob van Glabbeek
Publication date
2019
fields
Informatics Engineering
and research's language is
English
Authors
Rob van Glabbeek
Ask ChatGPT about the research
No Arabic abstract
May and must testing were introduced by De Nicola and Hennessy to define semantic equivalences on processes. May-testing equivalence exactly captures safety properties, and must-testing equivalence liveness properties. This paper proposes reward testing and shows that the resulting semantic equivalence also captures conditional liveness properties. It is strictly finer than both the may- and must-testing equivalence.
rate research
Read More
We introduce a notion of real-valued reward testing for probabilistic processes by extending the traditional nonnegative-reward testing with negative rewards. In this richer testing framework, the may and must preorders turn out to be inverses. We show that for convergent processes with finitely many states and transitions, but not in the presence of divergence, the real-reward must-testing preorder coincides with the nonnegative-reward must-testing preorder. To prove this coincidence we characterise the usual resolution-based testing in terms of the weak transitions of processes, without having to involve policies, adversaries, schedulers, resolutions, or similar structures that are external to the process under investigation. This requires establishing the continuity of our function for calculating testing outcomes.
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 processes or generative/reactive probabilistic processes, only if specific sets of tests are admitted. In this paper, n
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.
In the standard testing theory of DeNicola-Hennessy one process is considered to be a refinement of another if every test guaranteed by the former is also guaranteed by the latter. In the domain of web services this has been recast, with processes viewed as servers and tests as clients. In this way the standard refinement preorder between servers is determined by their ability to satisfy clients. But in this setting there is also a natural refinement preorder between clients, determined by their ability to be satisfied by servers. In more general settings where there is no distinction between clients and servers, but all processes are peers, there is a further refinement preorder based on the mutual satisfaction of peers. We give a uniform account of these three preorders. In particular we give two characterisations. The first is behavioural, in terms of traces and ready sets. The second, for finite processes, is equational.
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 relationships are summarized in a so-called spectrum. However, the equivalences we consider in that paper are only a small subset of those considered in the original spectrum of equivalences for nondeterministic systems introduced by Rob van Glabbeek. In this companion paper we we enlarge the spectrum by considering variants of trace equivalences (completed-trace equivalences), additional decorated-trace equivalences (failure-trace, readiness, and ready-trace equivalences), and variants of bisimulation equivalences (kernels of simulation, completed-simulation, failure-simulation, and ready-simulation preorders). Moreover, we study how the spectrum changes when randomized schedulers are used instead of deterministic ones.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
