Skip to Main content Skip to Navigation
Journal articles

Constraint Markov Chains

Benoit Caillaud 1 Benoît Delahaye 1 Kim Guldstrand Larsen 2 Axel Legay 1 Mikkel L. Pedersen 2 Andrzej Wasowski 3 
1 S4 - System synthesis and supervision, scenarios
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
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.
Document type :
Journal articles
Complete list of metadata
Contributor : Benoît Caillaud Connect in order to contact the contributor
Submitted on : Tuesday, December 20, 2011 - 4:40:38 PM
Last modification on : Friday, February 4, 2022 - 3:23:41 AM

Links full text



Benoit Caillaud, Benoît Delahaye, Kim Guldstrand Larsen, Axel Legay, Mikkel L. Pedersen, et al.. Constraint Markov Chains. Theoretical Computer Science, Elsevier, 2011, 412 (34), pp.4373-4404. ⟨10.1016/j.tcs.2011.05.010⟩. ⟨hal-00654003⟩



Record views