Conference paper
On Probabilistic Automata in Continuous Time
We develop a compositional behavioural model that integrates a variation of probabilistic automata into a conservative extension of interactive Markov chains. The model is rich enough to embody the semantics of generalised stochastic Petri nets. We define strong and weak bisimulations and discuss their compositionality properties.
Weak bisimulation is partly oblivious to the probabilistic branching structure, in order to reflect some natural equalities in this spectrum of models. As a result, the standard way to associate a stochastic process to a generalised stochastic Petri net can be proven sound with respect to weak bisimulation.
Language: | English |
---|---|
Year: | 2010 |
Pages: | 342-351 |
Proceedings: | 25th Annual IEEE Symposium on Logic in Computer Science |
ISBN: | 1424475880 , 1424475899 , 9781424475889 and 9781424475896 |
ISSN: | 10436871 and 25755528 |
Types: | Conference paper |
DOI: | 10.1109/LICS.2010.41 |
Automata Concurrent computing Delay Markov processes Petri nets Probabilistic logic bisimulation bisimulation equivalence compositional behavioural model continuous time discrete time generalised stochastic Petri net semantics interactive Markov chains nondeterminism probabilistic automata process algebra semantic networks weak bisimulation semantics