Compositional verification and optimization of interactive Markov chains

DOI10.1007/978-3-642-40184-8_26MaRDI QIDQ2842120zbMATH OpenOpenAlexFDO

Authors Holger Hermanns, Jan Krčál, Jan Křetínský

Publication date 12 August 2013

Published in CONCUR 2013 – Concurrency Theory (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1305.7332

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Interactive Markov chains (IMC) are compositional behavioural models extending labelled transition systems and continuous-time Markov chains. We provide a framework and algorithms for compositional verification and optimization of IMC with respect to time-bounded properties. Firstly, we give a specification formalism for IMC. Secondly, given a time-bounded property, an IMC component and the assumption that its unknown environment satisfies a given specification, we synthesize a scheduler for the component optimizing the probability that the property is satisfied in any such environment.

Recommendations

• Verification of open interactive Markov chains
• Model Checking Interactive Markov Chains
• The how and why of interactive Markov chains
• scientific article; zbMATH DE number 1397300
• A Tutorial on Interactive Markov Chains

Cited in

(7)

• Compositional design of stochastic timed automata
• Distributed synthesis in continuous time
• Improving time bounded reachability computations in interactive Markov chains
• Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains
• Verification of open interactive Markov chains
• Model checking compositional Markov systems.
• Incremental Verification of Parametric and Reconfigurable Markov Chains

This page was built for publication: Compositional verification and optimization of interactive Markov chains

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2842120)