Skip to Main content Skip to Navigation

Compositional Design Methodology with 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 : A specification theory combines notions of specification and implementation with a satisfaction relation, a refinement relation and a set of operators that together support stepwise design. We propose a new abstraction, Constraint Markov Chains, and use it to construct a specification theory for Markov Chains. Constraint Markov Chains generalize previously known abstractions by allowing arbitrary constraints on probability distributions. Our theory is the first specification theory for Markov Chains closed under conjunction, parallel composition and synchronization. Moreover, all the operators and relations introduced are computable.
Document type :
Complete list of metadata

Cited literature [28 references]  Display  Hide  Download
Contributor : Benoît Delahaye Connect in order to contact the contributor
Submitted on : Tuesday, May 25, 2010 - 12:55:09 PM
Last modification on : Friday, February 4, 2022 - 3:24:01 AM
Long-term archiving on: : Thursday, September 23, 2010 - 12:54:02 PM


Files produced by the author(s)


  • HAL Id : inria-00404304, version 2


Benoit Caillaud, Benoît Delahaye, Kim Guldstrand Larsen, Axel Legay, Mikkel L. Pedersen, et al.. Compositional Design Methodology with Constraint Markov Chains. [Research Report] RR-6993, INRIA. 2009. ⟨inria-00404304v2⟩



Record views


Files downloads