Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
426079 | Information and Computation | 2013 | 30 Pages |
Abstract
Markov automata describe systems in terms of events which may be nondeterministic, may occur probabilistically, or may be subject to time delays. We define a novel notion of weak bisimulation for such systems and prove that this provides both a sound and complete proof methodology for a natural extensional behavioural equivalence between such systems, a generalisation of reduction barbed congruence, the well-known touchstone equivalence for a large variety of process description languages.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Yuxin Deng, Matthew Hennessy,