Evènement pour le groupe Modélisation et Verification

Date 2012-03-15  11:30-12:30
TitreCompositional Specification Theories for Stochastic Systems 
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. 
OrateurBenoît Delahaye 

Aucun document lié à cet événement.

Retour à l'index