Constraint Markov Chains

Translated title of the contribution: Constraint Markov Chains

Benoît Caillaud, Benoît Delahaye, Kim Guldstrand Larsen, Axel Legay, Mikkel Larsen Pedersen, Andrzej Wasowski

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

Abstract

Notions of specification, implementation, satisfaction, and refinement, together with operators supporting stepwise design, constitute a specification theory. We construct such a theory for Markov Chains (MCs) employing a new abstraction of a Constraint MC. Constraint MCs permit rich constraints on probability distributions and thus generalize prior abstractions such as Interval MCs. Linear (polynomial) constraints suffice for closure under conjunction (respectively parallel composition). This is the first specification theory for MCs with such closure properties. We discuss its relation to simpler operators for known languages such as probabilistic process algebra. Despite the generality, all operators and relations are computable.
Translated title of the contributionConstraint Markov Chains
Original languageUndefined/Unknown
JournalTheoretical Computer Science
Volume412
Issue number34
Pages (from-to)4373-4404
Number of pages32
ISSN0304-3975
DOIs
Publication statusPublished - 2011

Keywords

  • Specification theory
  • Markov Chains
  • Compositional reasoning
  • Abstraction
  • Process algebra

Fingerprint

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

Cite this