2026-07-23T15:27:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3882 2024-03-06T10:34:35Z ddc:004 open_access

Verification of Open Interactive Markov Chains Brazdil, Tomas Hermanns, Holger Krcal, Jan Kretinsky, Jan Rehak, Vojtech IMC compositional verification synthesis time bounded reachability discretization 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Tomas Brazdil and Holger Hermanns and Jan Krcal and Jan Kretinsky and Vojtech Rehak 2012 Is Part Of LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2012.474 urn:nbn:de:0030-drops-38826 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.474 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode