2011 | OriginalPaper | Buchkapitel
Linear-Time and May-Testing in a Probabilistic Reactive Setting
verfasst von : Lucia Acciai, Michele Boreale, Rocco De Nicola
Erschienen in: Formal Techniques for Distributed Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We consider reactive probabilistic labelled transition systems (
rplts
), a model where internal choices are refined by probabilistic choices. In this setting, we study the relationship between linear-time and may-testing semantics, where an angelic view of nondeterminism is taken. Building on the model of
d-trees
of Cleaveland et al., we first introduce a clean model of probabilistic may-testing, based on simple concepts from measure theory. In particular, we define a probability space where statements of the form “
p
may pass test
o
” naturally correspond to measurable events. We then obtain an observer-independent characterization of the may-testing preorder, based on comparing the probability of
sets
of traces, rather than of
individual
traces. This entails that may-testing is strictly finer than linear-time semantics. Next, we characterize the may-testing preorder in terms of the probability of satisfying safety properties, expressed as languages of infinite
trees
rather than traces. We then identify a significative subclass of
rplts
where linear and may-testing semantics do coincide: these are the
separated
rplts
, where actions are partitioned into probabilistic and nondeterministic ones, and at each state only one type is available.