Abstract
We present alternative characterizations of the testing preorders for probabilistic processes proposed in [CSZ92]. For a given probabilistic process, the characterization takes the form of a mapping from probabilistic traces to the interval [0, 1], where a probabilistic trace is an alternating sequence of actions and probability distributions over actions. Our results, like those of [CSZ92], pertain to divergence-free probabilistic processes, and are presented in two stages: probabilistic tests without internal τ-transitions are considered first, followed by probabilistic tests with τ-transitions. In each case, we show that our alternative characterization is fully abstract with respect to the corresponding testing pre-order, thereby resolving an open problem in [CSZ92]. In the second case, we use the alternative characterization to show that the testing preorder is actually an equivalence relation.
Finally, we give proof techniques, derived from the alternative characterizations, for establishing preorder relationships between probabilistic processes. The utility of these techniques is demonstrated by means of some simple examples.
Research performed while on leave at SUNY Stony Brook.
Research supported in part by NSF/DARPA grant CCR-9014775, NSF grant CCR9120995, ONR Young Investigator Award N00014-92-J-1582, and NSF Young Investigator Award CCR-9257963.
Research supported in part by NSF Grants CCR-9120995 and CCR-9208585, and AFOSR Grant F49620-93-1-0250DEF.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
I. Christoff. Testing equivalences and fully abstract models for probabilistic processes. In J. C. M. Baeten and J. W. Klop, editors, Proceedings of CONCUR ’90 — First Intl. Conf. on Concurrency Theory, volume 458 of Lecture Notes in Computer Science, pages 126–140. Springer-Verlag, 1990.
R. Cleaveland, S. A. Smolka, and A. E. Zwarico. Testing preorders for probabilistic processes. In Proceedings of the 19th ICALP, volume 623 of Lecture Notes in Computer Science, pages 708–719. Springer Verlag, July 1992.
R. DeNicola. Extensional equivalences for transition systems. Acta Informatica, 24: 211–237, 1987.
R. DeNicola and M.C.B. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34: 83–133, 1983.
M.C.B. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.
H. A. Hansson and B. Jonsson. A calculus for communicating systems with time and probabilities. In Proceedings of the 11th IEEE Symposium on Real-Time Systems, pages 278–287, 1990.
K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1): 1–28, September 1992. Preliminary versions of this paper appeared as University of Aalborg technical reports R 88–18 and R 88–29, and in Proceedings of the 16th Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, 1989.
K. G. Larsen and A. Skou. Compositional verification of probabilistic processes. In Proceedings of CONCUR ’92, volume 630 of Lecture Notes in Computer Science, pages 456–471. Springer-Verlag, 1992.
N.A. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceeding the 6th Annual ACM symposium on Principles of Distributed Computing, pages 137–151, 1987.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
R. J. van Glabbeek, S. A. Smolka, B. Steffen, and C. M. N. Tofts. Reactive, generative, and stratified models of probabilistic processes. In Proceedings of the 5th IEEE Symposium on Logic in Computer Science, pages 130–141, Philadelphia, PA, 1990.
S. Wu, S.A. Smolka, and E.W. Stark. Composition and behaviors of probabilistic I/O automata. In Proceedings of CONCUR ’94, Lecture Notes in Computer Science. Springer Verlag, 1994.
W. Yi and Kim G. Larsen. Testing probabilistic and nondeterministic processes. In Protocol Specification, Testing and Verification XII, pages 47–61, 1992.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yuen, S., Cleaveland, R., Dayar, Z., Smolka, S.A. (1994). Fully Abstract Characterizations of Testing Preorders for Probabilistic Processes. In: Jonsson, B., Parrow, J. (eds) CONCUR ’94: Concurrency Theory. CONCUR 1994. Lecture Notes in Computer Science, vol 836. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-48654-1_36
Download citation
DOI: https://doi.org/10.1007/978-3-540-48654-1_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58329-5
Online ISBN: 978-3-540-48654-1
eBook Packages: Springer Book Archive