HAL - INRIA :: [inria-00404304, version 2] Compositional Design Methodology with Constraint Markov Chains

inria-00404304, version 2

Compositional Design Methodology with Constraint Markov Chains

Benoit Caillaud ()^a^, 1, Benoît Delahaye ()^b^, 1, Kim G. Larsen^c^, 2, Axel Legay ()^a^, 1, Mikkel L. Pedersen^c^, 2, Andrzej Wasowski^d^, 3

N° RR-6993 (2009)

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.

a – INRIA
b – Université de Rennes 1
c – Alborg University, Danemark
d – IT University of Copenhagen
1: S4 (INRIA - IRISA)
CNRS : UMR6074 – INRIA – INSA Rennes – Université de Rennes 1
2: University of Aalborg
University of Aalborg
3: IT University of Copenhagen (IT)
IT University of Copenhagen

Collaboration : Aalborg University, IT University of Copenhagen

inria-00404304, version 2
http://hal.inria.fr/inria-00404304
oai:hal.inria.fr:inria-00404304
From: Benoît Delahaye <>
Submitted on: Tuesday, 25 May 2010 12:55:09
Updated on: Tuesday, 9 November 2010 16:42:17

See detailed view

Associated documents

PDF :

PS :

Export

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="report"><head>Research reports</head>
<biblStruct type="report" xml:id="inria-00404304"><monogr>
<author><persName><forename>Benoit</forename><surname>Caillaud</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA - IRISA</orgName>
<orgName type="team">S4</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR6074</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">INSA Rennes</orgName>
<orgName type="institution">Université de Rennes 1</orgName>
</affiliation>
</author>
<author><persName><forename>Benoît</forename><surname>Delahaye</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA - IRISA</orgName>
<orgName type="team">S4</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR6074</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">INSA Rennes</orgName>
<orgName type="institution">Université de Rennes 1</orgName>
</affiliation>
</author>
<author><persName><forename>Kim G.</forename><surname>Larsen</surname></persName>
<affiliation>
<orgName type="team">University of Aalborg</orgName>
<country>DK</country>
<orgName type="institution">University of Aalborg</orgName>
</affiliation>
</author>
<author><persName><forename>Axel</forename><surname>Legay</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA - IRISA</orgName>
<orgName type="team">S4</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR6074</orgName>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">INSA Rennes</orgName>
<orgName type="institution">Université de Rennes 1</orgName>
</affiliation>
</author>
<author><persName><forename>Mikkel L.</forename><surname>Pedersen</surname></persName>
<affiliation>
<orgName type="team">University of Aalborg</orgName>
<country>DK</country>
<orgName type="institution">University of Aalborg</orgName>
</affiliation>
</author>
<author><persName><forename>Andrzej</forename><surname>Wasowski</surname></persName>
<affiliation>
<orgName type="laboratory">IT</orgName>
<orgName type="team">IT University of Copenhagen</orgName>
<country>DK</country>
<orgName type="institution">IT University of Copenhagen</orgName>
</affiliation>
</author>
<title type="main" level="m">Compositional Design Methodology with Constraint Markov Chains</title><title type="main" level="m">Compositional Design Methodology with Constraint Markov Chains</title><imprint><biblScope type="publicationDate">2009-00-00</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00404304</idno><idno type="HALFile">http://hal.inria.fr/inria-00404304/PDF/RR-6993.pdf</idno></biblStruct>
</listBibl>
</listBibl>