AbstractSeveral probabilistic simulation relations for probabilistic systems are defined and evaluated according to two criteria: compositionality and preservation of ``interesting'' properties. Here, the interesting properties of a system are identified with those that are expressible in an untimed version of the Timed Probabilistic concurrent Computation Tree Logic (TPCTL) of Hansson. The definitions are made, and the evaluations carried out, in terms of a general labeled transition system model for concurrent probabilistic computation. The results cover weak simulations, which abstract from internal computation, as well as strong simulations, which do not.
Categories and Subject Descriptors: D.2.1 [Software Engineering]: Requirements/Specifications; D.2.4 [Software Engineering]: Program Verification; D.3.1 [Programming Languages]: Formal Definitions and Theory; F.1.2 [Computation by Abstract Devices]: Modes of Computation
Additional Key Words and Phrases: probabilistic automata, simulation method, specification, temporal logic, verification
Selected references
- Rob van Glabbeek, Scott A. Smolka, Bernhard Steffen, and Chris M. N. Tofts. Reactive, generative, and stratified models of probabilistic processes. In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 130-141, Philadelphia, Pennsylvania, 4-7 June 1990. IEEE Computer Society Press.
- Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137-161, January 1985.
- Bengt Jonsson and Kim Guldstrand Larsen. Specification and refinement of probabilistic processes. In Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, pages 266-277, Amsterdam, The Netherlands, 15-18 July 1991. IEEE Computer Society Press.
- Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1-28, September 1991.
- Daniel J. Lehmann and Michael O. Rabin. On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem. In Conference Record of the Eighth Annual ACM Symposium on Principles of Programming Languages, pages 133-138, Williamsburg, Virginia, January 1981.
- Rocco De Nicola and Frits Vaandrager. Three logics for branching bisimulation (extended abstract). In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 118-129, Philadelphia, Pennsylvania, 4-7 June 1990. IEEE Computer Society Press.
- Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite-state programs. In 26th Annual Symposium on Foundations of Computer Science, pages 327-338, Portland, Oregon, 21-23 October 1985. IEEE.