Résumé | Markov Chains (MCs) and Probabilistic Automata (PAs) are
widely-recognized mathematical frameworks for the specification and
analysis of systems with non-deterministic and/or stochastic behaviors.
Notions of specification, implementation, satisfaction, and refinement,
together with operators supporting stepwise design, constitute a
specification theory. In the early 1990's, an abstraction of Markov
Chains, called Interval Markov Chains (IMCs) has been proposed as a
specification theory. This talk shows why IMCs are not perfectly suited
to play their role as a specification theory and instead introduces a
new, more permissive, abstraction called Constraint Markov Chains
(CMCs). We introduce all the operators that make CMCs a complete
specification theory and discuss computability and complexity. We then
show how to extend CMCs by mixing them with Modal Transition Systems in
order to propose a specification theory for Probabilistic Automata. |