Abstract
This paper contributes to the multi-core model checking of timed automata (TA) with respect to liveness properties, by investigating checking of TA Büchi emptiness under the very coarse inclusion abstraction or zone subsumption, an open problem in this field.
We show that in general Büchi emptiness is not preserved under this abstraction. However, we prove that some other structural properties are preserved. Solving the problem partly, we propose a variation of the classic nested depth-first search (NDFS) algorithm that takes advantage of these properties thereby exploiting inclusion abstraction. In addition, we extend the multi-core CNDFS algorithm with subsumption, providing the first parallel LTL model checking algorithm for timed automata. We prove both algorithms correct and show that other, more aggressive variations are incorrect.
The algorithms are implemented in LTSmin, and experimental evaluations show the effectiveness and scalability of both contributions: subsumption halves the number of states in the real-world FDDI and CSMA case studies, and the multi-core algorithm yields speedups of up to 40 on a 48 cores.
Original language | English |
---|---|
Title of host publication | Computer Aided Verification |
Subtitle of host publication | 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings |
Editors | Natasha Sharygina, Helmut Veith |
Place of Publication | Berlin, Heidelberg |
Publisher | Springer |
Pages | 968-983 |
Number of pages | 18 |
ISBN (Electronic) | 978-3-642-39799-8 |
ISBN (Print) | 978-3-642-39798-1 |
DOIs | |
Publication status | Published - 13 Jul 2013 |
Event | 25th International Conference on Computer Aided Verification, CAV 2013 - Saint Petersburg, Russian Federation Duration: 13 Jul 2013 → 19 Jul 2013 Conference number: 25 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 8044 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 25th International Conference on Computer Aided Verification, CAV 2013 |
---|---|
Abbreviated title | CAV |
Country/Territory | Russian Federation |
City | Saint Petersburg |
Period | 13/07/13 → 19/07/13 |
Keywords
- FMT-MC: MODEL CHECKING
- Subsumption
- Inclusion abstraction
- Timed automata
- UPPAAL
- Opaal
- Parallel
- LTL
- LTSMIN
- LU abstraction
- liveness
- Model checking
- Multi-core
- NDFS
- Büchi emptiness
- CNDFS
- n/a OA procedure