Constraint Markov Chains

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

doi:10.1016/j.tcs.2011.05.010

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 Journal › Journal article › Research › peer-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 contribution	Constraint Markov Chains
Original language	Undefined/Unknown
Journal	Theoretical Computer Science
Volume	412
Issue number	34
Pages (from-to)	4373-4404
Number of pages	32
ISSN	0304-3975
DOIs	https://doi.org/10.1016/j.tcs.2011.05.010
Publication status	Published - 2011

Keywords

Specification theory
Markov Chains
Compositional reasoning
Abstraction
Process algebra

Access to Document

10.1016/j.tcs.2011.05.010

Cite this

@article{7abc60f1f11243b99e4b5be4de9a6730,

title = "Constraint Markov Chains",

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.",

keywords = "Specification theory, Markov Chains, Compositional reasoning, Abstraction, Process algebra, Specification theory, Markov Chains, Compositional reasoning, Abstraction, Process algebra",

author = "Beno{\^i}t Caillaud and Beno{\^i}t Delahaye and Larsen, {Kim Guldstrand} and Axel Legay and Pedersen, {Mikkel Larsen} and Andrzej Wasowski",

year = "2011",

doi = "10.1016/j.tcs.2011.05.010",

language = "Udefineret/Ukendt",

volume = "412",

pages = "4373--4404",

journal = "Theoretical Computer Science",

issn = "0304-3975",

publisher = "Elsevier",

number = "34",

}

TY - JOUR

T1 - Constraint Markov Chains

AU - Caillaud, Benoît

AU - Delahaye, Benoît

AU - Larsen, Kim Guldstrand

AU - Legay, Axel

AU - Pedersen, Mikkel Larsen

AU - Wasowski, Andrzej

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

KW - Specification theory

KW - Markov Chains

KW - Compositional reasoning

KW - Abstraction

KW - Process algebra

KW - Specification theory

KW - Markov Chains

KW - Compositional reasoning

KW - Abstraction

KW - Process algebra

U2 - 10.1016/j.tcs.2011.05.010

DO - 10.1016/j.tcs.2011.05.010

M3 - Tidsskriftartikel

SN - 0304-3975

VL - 412

SP - 4373

EP - 4404

JO - Theoretical Computer Science

JF - Theoretical Computer Science

IS - 34

ER -

Constraint Markov Chains

Abstract

Keywords

Access to Document

Fingerprint

Cite this