On Probabilistic Automata in Continuous Time

Christian Eisentraut; Holger Hermanns; Lijun Zhang

doi:10.1109/LICS.2010.41

On Probabilistic Automata in Continuous Time

Christian Eisentraut, Holger Hermanns, Lijun Zhang

Research output: Contribution to journal › Conference article › Research › peer-review

Abstract

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.

Original language	English
Journal	Symposium on Logic in Computer Science
Pages (from-to)	342 - 351
ISSN	1043-6871
DOIs	https://doi.org/10.1109/LICS.2010.41
Publication status	Published - 2010
Event	25th Annual IEEE Symposium on Logic in Computer Science - Edinburgh, United Kingdom Duration: 11 Jul 2010 → 14 Jul 2010 Conference number: 25 http://lics.rwth-aachen.de/lics10/

Conference

Conference	25th Annual IEEE Symposium on Logic in Computer Science
Number	25
Country/Territory	United Kingdom
City	Edinburgh
Period	11/07/2010 → 14/07/2010
Internet address	http://lics.rwth-aachen.de/lics10/

Access to Document

10.1109/LICS.2010.41

OpenUrl availability

Full text

Cite this

@inproceedings{4885977c50bf467099fbd1c5fe433997,

title = "On Probabilistic Automata in Continuous Time",

abstract = "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.",

author = "Christian Eisentraut and Holger Hermanns and Lijun Zhang",

year = "2010",

doi = "10.1109/LICS.2010.41",

language = "English",

pages = "342 -- 351",

journal = "Proceedings - Symposium on Logic in Computer Science",

issn = "1043-6871",

publisher = "I E E E Computer Society",

note = "25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010 ; Conference date: 11-07-2010 Through 14-07-2010",

url = "http://lics.rwth-aachen.de/lics10/",

}

TY - GEN

T1 - On Probabilistic Automata in Continuous Time

AU - Eisentraut, Christian

AU - Hermanns, Holger

AU - Zhang, Lijun

N1 - Conference code: 25

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

U2 - 10.1109/LICS.2010.41

DO - 10.1109/LICS.2010.41

M3 - Conference article

SN - 1043-6871

SP - 342

EP - 351

JO - Proceedings - Symposium on Logic in Computer Science

JF - Proceedings - Symposium on Logic in Computer Science

T2 - 25th Annual IEEE Symposium on Logic in Computer Science

Y2 - 11 July 2010 through 14 July 2010

ER -

On Probabilistic Automata in Continuous Time

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this