New results for Constraint Markov Chains

Benoit Delahaye, Kim Guldstrand Larsen, Axel Legay, Mikkel Larsen Pedersen, Andrzej Wasowski

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Abstract

This paper studies compositional reasoning theories for stochastic systems. A specification theory combines notions of specification and implementation with satisfaction and refinement relations, and a set of operators that together support stepwise design. One of the first behavioral specification theories introduced for stochastic systems is the one of Interval Markov Chains (IMCs), which are Markov Chains whose probability distributions are replaced by a conjunction of intervals. In this paper, we show that IMCs are not closed under conjunction, which gives a formal proof of a conjecture made in several recent works.

In order to leverage this problem, we suggested to work with Constraint Markov Chains (CMCs) that is another specification theory where intervals are replaced with general constraints. Contrary to IMCs, one can show that CMCs enjoy the closure properties of a specification theory. In addition, we propose aggressive abstraction procedures for CMCs. Such abstractions can be used either to combat the state-space explosion problem, or to simplify complex constraints. In particular, one can show that, under some assumptions, the behavior of any CMC can be abstracted by an IMC.

Finally, we propose an algorithm for counter-example generation, in case a refinement of two CMCs does not hold. We present a tool that implements our results. Implementing CMCs is a complex process and relies on recent advances made in decision procedures for theory of reals.
Original languageEnglish
JournalPerformance Evaluation
Volume69
Issue number7-8
Pages (from-to)379-401
ISSN0166-5316
Publication statusPublished - 2012

Keywords

  • Specification
  • Abstraction
  • Markov Chains
  • Compositional reasoning
  • Reasoning about fault tolerance

Fingerprint

Dive into the research topics of 'New results for Constraint Markov Chains'. Together they form a unique fingerprint.

Cite this