TY - GEN
T1 - On the semantics of Markov automata
AU - Deng, Yuxin
AU - Hennessy, Matthew
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/79960023661
U2 - 10.1007/978-3-642-22012-8_24
DO - 10.1007/978-3-642-22012-8_24
M3 - 会议稿件
AN - SCOPUS:79960023661
SN - 9783642220111
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 307
EP - 318
BT - Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Proceedings
T2 - 38th International Colloquium on Automata, Languages and Programming, ICALP 2011
Y2 - 4 July 2011 through 8 July 2011
ER -