The How and Why of Interactive Markov Chains
| Autor: | Hermanns, H., Katoen, Joost P., de Boer, F.S, Bonsangue, S.H., Leuschel, M |
|---|---|
| Rok vydání: | 2010 |
| Předmět: |
Fault tree analysis
Bisimulation Markov chain Computer science EWI-18444 020207 software engineering 0102 computer and information sciences 02 engineering and technology 01 natural sciences Computer Science::Other 010201 computation theory & mathematics Reachability METIS-271027 IR-73120 0202 electrical engineering electronic engineering information engineering Stochastic Petri net Algorithm |
| Zdroj: | Formal Methods for Components and Objects ISBN: 9783642170706 FMCO Symposium on Formal Methods for Components and Objects, FMCO 2009, 311-337 STARTPAGE=311;ENDPAGE=337;TITLE=Symposium on Formal Methods for Components and Objects, FMCO 2009 |
| ISSN: | 0302-9743 |
| DOI: | 10.1007/978-3-642-17071-3_16 |
| Popis: | This paper reviews the model of interactive Markov chains (IMCs, for short), an extension of labelled transition systems with exponentially delayed transitions. We show that IMCs are closed under parallel composition and hiding, and show how IMCs can be compositionally aggregated prior to analysis by e.g., bisimulation minimisation or aggressive abstraction based on simulation pre-congruences. We survey some recent analysis techniques for IMCs, i.e., explaining how measures such as reachability probabilities can be obtained. Finally, we demonstrate that IMCs are a natural (and simple) semantic model for stochastic process algebras and generalised stochastic Petri nets and can be used for engineering formalisms such as AADL and dynamic fault trees. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|