zbMATH — the first resource for mathematics

Bisimulation through probabilistic testing. (English) Zbl 0756.68035
A test language and a notion of probabilistic testability of concurrent process properties are presented. Properties expressed as formulas within Hennessy-Milner logic are testable and as a consequence non-bisimilar processes can be distinguished through testing. A new process relation called \({2\over3}\)-bisimulation is introduced. The relation lies strictly between that of simulation and bisimulation. For probabilistic transition systems for which there is a limit to the probability of transitions it is proved that two processes are \({2\over3}\)-bisimilar iff they satisfy the same limited modal logic formulas. Probabilistic modal logic is introduced and it is shown that the induced notion of probabilistic bisimilarity characterizes the limit as to the distinguishing power of the test language. The probabilistic bisimulation is strictly stronger than bisimulation.

68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI
[1] Abramsky, S., Observation equivalence as a testing equivalence, Theoret. comput. sci., 53, 225, (1987) · Zbl 0626.68016
[2] Bloom, B.; Meyer, A., A remark on bisimulation between probabilistic processes, (), 26-40
[3] Bloom, B.; Istrail, S.; Meyer, A., Bisimulation can’t be traced: preliminary report, (), 229-239
[4] Chung, K.L., ()
[5] Cox, D.; Hinkley, D., ()
[6] de Nicola, R.; Hennessy, M., Testing equivalences for proceses, Theoret. comput. sci., 34, 83, (1983) · Zbl 0985.68518
[7] Dijkstra, E., Notes on structured programming, (), 1-82
[8] Hennessy, M.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. assoc. comput. Mach., 137, (1985) · Zbl 0629.68021
[9] Hughes, G.; Cresswell, M., ()
[10] Larsen, K.G., Context-dependent bisimulation between processes, ()
[11] Larsen, K.G., Proof systems for hennessy-milner logic with recursion, (), 215-230
[12] Milner, R., Calculus of communicating systems, () · Zbl 0452.68027
[13] Milner, R., Modal characterization of observable machine behaviour, () · Zbl 0474.68074
[14] Milner, r., Calculi for synchrony and asynchrony, Theoret. comput. sci., 25, 267, (1963) · Zbl 0512.68026
[15] Park, D., Concurrency and automata on infinite sequences, (), 167-183
[16] Phillips, I., Refusal testing, (), 304-313 · Zbl 0594.68022
[17] Plotkin, G., A structural approach to operational semantics, () · Zbl 1082.68062
[18] Pnueli, A., Linear and branching structures in the semantics and logics of reactive systems, (), 15-32
[19] Skou, A., Validation of concurrent processes, with emphasis of testing, ()
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.