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

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

Publikation: Artikel i tidsskrift og konference artikel i tidsskrift › Tidsskriftartikel › Forskning › 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.

Bidragets oversatte titel	Constraint Markov Chains
Originalsprog	Udefineret/Ukendt
Tidsskrift	Theoretical Computer Science
Vol/bind	412
Udgave nummer	34
Sider (fra-til)	4373-4404
Antal sider	32
ISSN	0304-3975
DOI	https://doi.org/10.1016/j.tcs.2011.05.010
Status	Udgivet - 2011

Emneord

Specification theory
Markov Chains
Compositional reasoning
Abstraction
Process algebra

Adgang til dokumentet

10.1016/j.tcs.2011.05.010

Citationsformater

@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

Emneord

Adgang til dokumentet

Fingeraftryk

Citationsformater