Article1994314596: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Johannes Lehmann (Diskussion | Beiträge) (Die Seite wurde neu angelegt: „{{Publikation Erster Autor |ErsterAutorVorname=Christel |ErsterAutorNachname=Baier |FurtherAuthors=Joost-Pieter Katoen; Holger Hermanns; Verena Wolf}} {{Article |Journal=Information and Computation |Number=2 |Pages=149--214 |Title=Comparative branching-time semantics for Markov chains |Volume=200 |Year=2005 }} {{Publikation Details |DOI Name=10.1016/J.IC.2005.03.001 |Abstract=This paper presents various semantics in the branching-time spectr…“) |
Johannes Lehmann (Diskussion | Beiträge) K (Textersetzung - „Verifikation und formale quantitative Analyse“ durch „Algebraische und logische Grundlagen der Informatik“) |
||
| Zeile 14: | Zeile 14: | ||
|DOI Name=10.1016/J.IC.2005.03.001 | |DOI Name=10.1016/J.IC.2005.03.001 | ||
|Abstract=This paper presents various semantics in the branching-time spectrum of discrete-time and continuous-time Markov chains (DTMCs and CTMCs). Strong and weak bisimulation equivalence and simulation pre-orders are covered and are logically characterized in terms of the temporal logics Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL). Apart from presenting various existing branching-time relations in a uniform manner, this paper presents the following new results: (i) strong simulation for CTMCs, (ii) weak simulation for CTMCs and DTMCs, (iii) logical characterizations thereof (including weak bisimulation for DTMCs), (iv) a relation between weak bisimulation and weak simulation equivalence, and (v) various connections between equivalences and pre-orders in the continuous- and discrete-time setting. The results are summarized in a branching-time spectrum for DTMCs and CTMCs elucidating their semantics as well as their relationship. | |Abstract=This paper presents various semantics in the branching-time spectrum of discrete-time and continuous-time Markov chains (DTMCs and CTMCs). Strong and weak bisimulation equivalence and simulation pre-orders are covered and are logically characterized in terms of the temporal logics Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL). Apart from presenting various existing branching-time relations in a uniform manner, this paper presents the following new results: (i) strong simulation for CTMCs, (ii) weak simulation for CTMCs and DTMCs, (iii) logical characterizations thereof (including weak bisimulation for DTMCs), (iv) a relation between weak bisimulation and weak simulation equivalence, and (v) various connections between equivalences and pre-orders in the continuous- and discrete-time setting. The results are summarized in a branching-time spectrum for DTMCs and CTMCs elucidating their semantics as well as their relationship. | ||
|Forschungsgruppe= | |Forschungsgruppe=Algebraische und logische Grundlagen der Informatik | ||
}} | }} | ||
Aktuelle Version vom 5. März 2025, 15:45 Uhr
Comparative branching-time semantics for Markov chains
Christel BaierChristel Baier, Joost-Pieter KatoenJoost-Pieter Katoen, Holger HermannsHolger Hermanns, Verena WolfVerena Wolf
Christel Baier, Joost-Pieter Katoen, Holger Hermanns, Verena Wolf
Comparative branching-time semantics for Markov chains
Information and Computation, 200(2):149--214, 2005
Comparative branching-time semantics for Markov chains
Information and Computation, 200(2):149--214, 2005
- KurzfassungAbstract
This paper presents various semantics in the branching-time spectrum of discrete-time and continuous-time Markov chains (DTMCs and CTMCs). Strong and weak bisimulation equivalence and simulation pre-orders are covered and are logically characterized in terms of the temporal logics Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL). Apart from presenting various existing branching-time relations in a uniform manner, this paper presents the following new results: (i) strong simulation for CTMCs, (ii) weak simulation for CTMCs and DTMCs, (iii) logical characterizations thereof (including weak bisimulation for DTMCs), (iv) a relation between weak bisimulation and weak simulation equivalence, and (v) various connections between equivalences and pre-orders in the continuous- and discrete-time setting. The results are summarized in a branching-time spectrum for DTMCs and CTMCs elucidating their semantics as well as their relationship. - Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science
@article{BKHW2005,
author = {Christel Baier and Joost-Pieter Katoen and Holger Hermanns and
Verena Wolf},
title = {Comparative branching-time semantics for Markov chains},
journal = {Information and Computation},
volume = {200},
number = {2},
year = {2005},
pages = {149--214},
doi = {10.1016/J.IC.2005.03.001}
}
