Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Brazdil, Tomas; Hermanns, Holger; Krcal, Jan; Kretinsky, Jan; Rehak, Vojtech http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-38826
URL:

; ; ; ;

Verification of Open Interactive Markov Chains

pdf-format:


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.

BibTeX - Entry

@InProceedings{brazdil_et_al:LIPIcs:2012:3882,
  author =	{Tomas Brazdil and Holger Hermanns and Jan Krcal and Jan Kretinsky and Vojtech Rehak},
  title =	{{Verification of Open Interactive Markov Chains}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012) },
  pages =	{474--485},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{Deepak D'Souza and Telikepalli Kavitha and Jaikumar Radhakrishnan},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3882},
  URN =		{urn:nbn:de:0030-drops-38826},
  doi =		{http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2012.474},
  annote =	{Keywords: IMC, compositional verification, synthesis, time bounded reachability, discretization}
}

Keywords: IMC, compositional verification, synthesis, time bounded reachability, discretization
Seminar: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)
Related Scholarly Article:
Issue date: 2012
Date of publication: 2012


DROPS-Home | Fulltext Search | Imprint Published by LZI