On the Discriminating Power of Testing Equivalences for Reactive Probabilistic Systems: Results and Open Problems
Autor: | Marco Bernardo, Davide Sangiorgi, Valeria Vignudelli |
---|---|
Přispěvatelé: | Università di Urbino, Foundations of Component-based Ubiquitous Systems (FOCUS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO)-Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Gethin Norman, William H. Sanders, Bernardo, Marco, Sangiorgi, Davide, Vignudelli, Valeria |
Jazyk: | angličtina |
Rok vydání: | 2014 |
Předmět: |
Bisimulation
testing equivalence probabilitities process algebra reactive systems Conjecture Concurrency Theory Probabilistic logic [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Nondeterministic algorithm Testing Semantics [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] Computer Science::Logic in Computer Science Probabilistic CTL Probabilistic analysis of algorithms Markov decision process Equivalence (measure theory) Algorithm Probabilistic Processes Computer Science::Formal Languages and Automata Theory Mathematics |
Zdroj: | QEST 2014 QEST 2014, Sep 2014, Florence, Italy. pp.281-296, ⟨10.1007/978-3-319-10696-0_23⟩ Quantitative Evaluation of Systems ISBN: 9783319106953 QEST |
DOI: | 10.1007/978-3-319-10696-0_23⟩ |
Popis: | International audience; Testing equivalences have been deeply investigated on fully nondeterministic processes, as well as on processes featuring probabilities and internal nondeterminism. This is not the case with reactive probabilistic processes, for which it is only known that the discriminating power of probabilistic bisimilarity is achieved when admitting a copying capability within tests. In this paper, we introduce for reactive probabilistic processes three testing equivalences without copying, which are respectively based on reactive probabilistic tests, fully nondeterministic tests, and nondeterministic and probabilistic tests. We show that the three testing equivalences are strictly finer than probabilistic failure-trace equivalence, and that the one based on nondeterministic and probabilistic tests is strictly finer than the other two, which are incomparable with each other. Moreover, we provide a number of facts that lead us to conjecture that (i) may testing and must testing coincide on reactive probabilistic processes and (ii) nondeterministic and probabilistic tests reach the same discriminating power as probabilistic bisimilarity. |
Databáze: | OpenAIRE |
Externí odkaz: |