Efficient CTMC Model Checking of Linear Real-Time Objectives

Barbot, Benoit and Chen, Taolue and Han, Tingting and Katoen, Joost-Pieter and Mereacre, Alexandru (2011) Efficient CTMC Model Checking of Linear Real-Time Objectives. In: 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011, 26 March - 3 April 2011, Saarbrücken, Germany.

PDF
Restricted to UT campus only: Request a copy
277Kb

Abstract:	This paper makes verifying continuous-time Markov chains (CTMCs) against deterministic timed automata (DTA) objectives practical. We show that verifying 1-clock DTA can be done by analyzing subgraphs of the product of CTMC C and the region graph of DTA A. This improves upon earlier results and allows to only use standard analysis algorithms. Our graph decomposition approach naturally enables bisimulation minimization as well as parallelization. Experiments with various examples confirm that these optimizations lead to significant speed-ups. We also report on experiments with multiple-clock DTA objectives. The objectives and the size of the problem instances that can be checked with our prototypical tool go (far) beyond what could be checked so far.
Item Type:	Conference or Workshop Item
Copyright:	© 2011 Springer
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/79389
Official URL:	http://dx.doi.org/10.1007/978-3-642-19835-9_12
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page