DiRePro : 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 and Stefan Leue: K*: A Heuristic Search Algorithm for Finding the k Shortest PathsArtificial Intelligence. Accepted for publication, 2011
  • Husain Aljazzar, Florian Leitner-Fischer, Stefan Leue and Dimitar Simeonov: DiPro - A Tool for Probabilistic Counterexample GenerationIn Proceedings of 18th International SPIN Workshop on Model Checking of Software (SPIN 2011), 2011. (PDF)
  • Boudewijn R. Haverkort, Matthias Kuntz, Florian Leitner-Fischer, Anne Remke and Stephan Roolvink: Probabilistic verification of Architectural software models using SoftArc and PrismIn: Proceedings of the ESREL 2010 Annual Conference, 5-9 Sept 2010, Greece, Rhodos. pp. 852-860. Taylor & Francis. ISBN 978-0-415-60427-7, 2010. (PDF)
  • B.R. Haverkort, M. Kuntz, A. Remke, S. Roolvink: Formal Performability Evaluation of Architectural Models of Critical Infrastructures., In: Proceedings of the ESREL 2010 Annual Conference, 5-9 Sept 2010, Greece, Rhodos. pp. 27-34. Taylor & Francis Group. ISBN 978-0-415-60427-7, 2010. (PDF)
  • B.R. Haverkort, M. Kuntz, A. Remke, S. Roolvink, M.I.A. Stoelinga: Evaluating Repair Strategies for a Water-Treatment Facility using ArcadeIn: 2010 IEEE/IFIP International Conference on Dependable Systems & Networks (DSN), 28 June - 1 July 2010, Chicago, IL, USA. pp. 419-424. IEEE Computer Society Press. ISBN 978-1-4244-7499-8, 2010. (PDF)
  • Husain Aljazzar and Stefan Leue: K*: Heuristics-Guided, On-the-Fly k Shortest Paths Search., Sixth Workshop on Model Checking and Artificial Intelligence (MoChArt 2010), 2010. (PDF)
  • Husain Aljazzar and Matthias Kuntz and Florian Leitner-Fischer and Stefan Leue: Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative EvaluationIn: Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems, 2010. (PDF)
  • Husain Aljazzar: Directed Diagnostics of System Dependability Models, Doctoral Dissertation, University of Konstanz, 2009. (PDF)
  • Husain Aljazzar and Stefan Leue: Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model CheckingIEEE Transactions on Software Engineering, IEEE computer Society Digital Library, IEEE Computer Society, 2009. (PDF)
  • Stefan Edelkamp, Viktor Schuppan, Dragan Bosnacki, Anton Wijs, Ansgar Fehnker and Husain Aljazzar: Survey on Directed Model Checking, Volume 5348, Pages 65-89, Model Checking and Artificial Intelligence, 5th International Workshop, MoChArt '08. Revised Selected and Invited Papers, Lecture Notes in Computer Science, Springer Verlag, 2009. (PDF)
  • Husain Aljazzar and Stefan Leue: Generation of Counterexamples for Model Checking of Markov Decision ProcessesProceedings of 6th International Conference on the Quantitative Evaluation of SysTems (QEST '09), IEEE Computer Society Press, 2009 (PDF)
  • H. Aljazzar, M. Fischer, L. Grunske, M. Kuntz, F. Leitner-Fischer, S. Leue: Safety Analysis of an Airbag System using Probabilistic FMEA and Probabilistic Counter ExamplesProceedings of 6th International Conference on the Quantitative Evaluation of SysTems (QEST '09), IEEE Computer Society Press, 2009. (PDF)
  • Husain Aljazzar and Stefan Leue: Debugging of Dependability Models Using Interactive Visualization of CounterexamplesProceedings of 5th International Conference on the Quantitative Evaluation of SysTems (QEST), IEEE Computer Society Press, to appear, 2008.
  • Husain Aljazzar and Stefan Leue: K*: A Directed On-The-Fly Algorithm for Finding the k Shortest PathsTechnical Report soft-08-03, Chair for Software Engineering, University of Konstanz, 2008. (PDF)
  • Husain Aljazzar and Stefan Leue: Counterexamples for Model Checking of Markov Decision ProcessesTechnical Report soft-08-01, Chair for Software Engineering, University of Konstanz, 2007 (PDF)
  • Husain Aljazzar and Stefan Leue: Extended Directed Search for Probabilistic Timed Reachability, Pages 33-51, Proceedings of 4th International Conference on Formal Modelling and Analysis of Timed Systems FORMATS '06, Lecture Notes in Computer Science, Springer Verlag, 2006. (PDF)
  • Husain Aljazzar and Stefan Leue: Extended Directed Search for Probabilistic Timed ReachabilityTechnical Report soft-06-03, Chair for Software Engineering, University of Konstanz, 2006. (PDF)
  • 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)