Probabilistic Systems:
Formal Verification of Availability Properties
Our research group considers the usage of heuristic search algorithms in the formal analysis of quantitative dependability models. We will enhance the power of stochastic model checking by reconciling it with heuristic directed explicit state model checking (DXMC). The purpose of this activity is two-fold.
-
First, we address the use of directed model checking in the generation
of counter-examples for model checking CSL formulas on stochastic processes like Continuous-Time Markov Chains (CTMCs). The probabilistic nature of the CSL model
checking problem does not ensure that a single path makes the property refuted
(if it is refuted). In other words, the stochastic model checking algorithm
will not be able to determine which part of the model is responsible for the
undesired event of exceeding a given probability bound. We
use DXMC in order to improve this situation.
- Second, we consider CSL model checking on Continuous Time Markov Decision Processes (CTMDPs). CTMDP is a generalization of CTMC in which both probabilistic and nondeterministic choices co-exist. CTMDPs can be considered an orthogonal extension of both CTMCs and standard labeled transition systems (LTSs). Because of the latter, one may view the DXMC approach as a guided search algorithm through a specific subset of CTMDPs (namely LTSs). In order to solve the CSL model checking problem on CTMDPs, one has to construct a best-case/worst-case policy (within a given class of policies) resolving the nondeterministic decisions contained in the CTMDP. We use DXMC as a guided search algorithm through the state space spanned by the nondeterministic fragments of a CTMDP in order to construct a policy which maximizes (or minimizes) the probability to satisfy a timed reachability property. Due to the continuoustime probabilistic nature of the problem, several nontrivial questions have to be addressed.
Publications
- Husain Aljazzar, Holger Hermanns, and Stefan Leue: Counterexamples for Timed Probabilistic Reachability, Proceedings of the 3rd International Conference on Formal Modelling and Analysis of Timed Systems FORMATS'05, Lecture Notes in Computer Science, Springer Verlag. To appear, 2005. (PDF)
- Husain Aljazzar and Stefan Leue: Extended Directed Search for Probabilistic Timed Reachability, Proceedings of 4th International Conference on Formal Modelling and Analysis of Timed Systems FORMATS '06, Lecture Notes in Computer Science, Springer Verlag, 2006. (PDF)