TY - JOUR
T1 - Constraint Markov chains
AU - Caillaud, B.
AU - Delahaye, B.
AU - Larsen, Kim Guldstrand
AU - Legay, A.
AU - Pedersen, M.L.
AU - Wa̧sowski, A.
PY - 2011/8/1
Y1 - 2011/8/1
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.
UR - http://www.scopus.com/inward/record.url?scp=79960017505&partnerID=8YFLogxK
U2 - 10.1016/j.tcs.2011.05.010
DO - 10.1016/j.tcs.2011.05.010
M3 - Journal article
AN - SCOPUS:79960017505
SN - 0304-3975
VL - 412
SP - 4373
EP - 4404
JO - Theoretical Computer Science
JF - Theoretical Computer Science
IS - 34
ER -