Projekter pr. år
Abstract
This paper studies compositional reasoning theories for stochastic systems. A specification theory combines notions of specification and implementation with satisfaction and refinement relations, and a set of operators that together support stepwise design. One of the first behavioral specification theories introduced for stochastic systems is the one of Interval Markov Chains (IMCs), which are Markov Chains whose probability distributions are replaced by a conjunction of intervals. In this paper, we show that IMCs are not closed under conjunction, which gives a formal proof of a conjecture made in several recent works.
In order to leverage this problem, we suggested to work with Constraint Markov Chains (CMCs) that is another specification theory where intervals are replaced with general constraints. Contrary to IMCs, one can show that CMCs enjoy the closure properties of a specification theory. In addition, we propose aggressive abstraction procedures for CMCs. Such abstractions can be used either to combat the statespace explosion problem, or to simplify complex constraints. In particular, one can show that, under some assumptions, the behavior of any CMC can be abstracted by an IMC.
Finally, we propose an algorithm for counterexample generation, in case a refinement of two CMCs does not hold. We present a tool that implements our results. Implementing CMCs is a complex process and relies on recent advances made in decision procedures for theory of reals.
In order to leverage this problem, we suggested to work with Constraint Markov Chains (CMCs) that is another specification theory where intervals are replaced with general constraints. Contrary to IMCs, one can show that CMCs enjoy the closure properties of a specification theory. In addition, we propose aggressive abstraction procedures for CMCs. Such abstractions can be used either to combat the statespace explosion problem, or to simplify complex constraints. In particular, one can show that, under some assumptions, the behavior of any CMC can be abstracted by an IMC.
Finally, we propose an algorithm for counterexample generation, in case a refinement of two CMCs does not hold. We present a tool that implements our results. Implementing CMCs is a complex process and relies on recent advances made in decision procedures for theory of reals.
Originalsprog  Engelsk 

Tidsskrift  Performance Evaluation 
Vol/bind  69 
Udgave nummer  78 
Sider (fratil)  379401 
ISSN  01665316 
Status  Udgivet  2012 
Emneord
 Specification
 Abstraction
 Markov Chains
 Compositional reasoning
 Reasoning about fault tolerance
Fingeraftryk
Dyk ned i forskningsemnerne om 'New results for Constraint Markov Chains'. Sammen danner de et unikt fingeraftryk.Projekter
 1 Afsluttet

MTLab  Modelling of Information Technology
Wasowski, A. (CoI), Godskesen, J. C. (PI), Song, L. (CoI), Traonouez, L.M. (CoI) & Biondi, F. (CoI)
01/11/2008 → 31/10/2013
Projekter: Projekt › Forskning