Loading...
Please wait, while we are loading the content...
Similar Documents
Verification of open interactive markov chains.
| Content Provider | CiteSeerX |
|---|---|
| Author | Brázdil, Tomáš Hermanns, Holger Krčál, Jan Křetínský, Jan Řehák, Vojtěch |
| Abstract | Interactive Markov chains (IMC) are compositional behavioral models extending both labeled transition systems and continuous-time Markov chains. IMC pair modeling convenience- owed to compositionality properties- with effective verification algorithms and tools- owed to Markov properties. Thus far however, IMC verification did not consider compositionality properties, but considered closed systems. This paper discusses the evaluation of IMC in an open and thus compositional interpretation. For this we embed the IMC into a game that is played with the environment. We devise algorithms that enable us to derive bounds on reachability probabilities that are assured to hold in any composition context. |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Open Interactive Markov Chain Compositionality Property Continuous-time Markov Chain Closed System Composition Context Labeled Transition System Interactive Markov Chain Reachability Probability Compositional Behavioral Model Markov Property Imc Verification Effective Verification Algorithm Compositional Interpretation Imc Pair |
| Content Type | Text |
| Resource Type | Article |
