Multi-core emptiness checking of timed Büchi automata using inclusion abstraction

Alfons Laarman, Mads Chr. Olesen, Andreas Dalsgaard, Kim G. Larsen, Jaco van de Pol

  • 14 Citations

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 languageEnglish
Title of host publicationComputer Aided Verification
Subtitle of host publication25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings
EditorsNatasha Sharygina, Helmut Veith
Place of PublicationLondon
PublisherSpringer
Pages968-983
Number of pages18
ISBN (Print)978-3-642-39798-1
DOIs
StatePublished - 13 Jul 2013
Event25th International Conference on Computer Aided Verification, CAV 2013 - Saint Petersburg, Russian Federation

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume8044
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference25th International Conference on Computer Aided Verification, CAV 2013
Abbreviated titleCAV
CountryRussian Federation
CitySaint Petersburg
Period13/07/1319/07/13

Fingerprint

Timed automata
Inclusion
Model checking
Depth-first search
Liveness
Experimental evaluation
Structural properties
Search algorithm
Open problems
Scalability

Keywords

  • FMT-MC: MODEL CHECKING
  • METIS-296351
  • subsumption
  • inclusion abstraction
  • Timed Automata
  • UPPAAL
  • opaal
  • Parallel
  • LTL
  • LTSMIN
  • LU abstraction
  • liveness
  • Model Checking
  • Multi-Core
  • NDFS
  • Büchi emptiness
  • IR-84627
  • CNDFS
  • EWI-23158

Cite this

Laarman, A., Olesen, M. C., Dalsgaard, A., Larsen, K. G., & van de Pol, J. (2013). Multi-core emptiness checking of timed Büchi automata using inclusion abstraction. In N. Sharygina, & H. Veith (Eds.), Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings (pp. 968-983). (Lecture Notes in Computer Science; Vol. 8044). London: Springer. DOI: 10.1007/978-3-642-39799-8_69

Laarman, Alfons; Olesen, Mads Chr.; Dalsgaard, Andreas; Larsen, Kim G.; van de Pol, Jaco / Multi-core emptiness checking of timed Büchi automata using inclusion abstraction.

Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. ed. / Natasha Sharygina; Helmut Veith. London : Springer, 2013. p. 968-983 (Lecture Notes in Computer Science; Vol. 8044).

Research output: Scientific - peer-reviewConference contribution

@inbook{4ec02d4bc50041349c7f36c9407c8de0,
title = "Multi-core emptiness checking of timed Büchi automata using inclusion abstraction",
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.",
keywords = "FMT-MC: MODEL CHECKING, METIS-296351, subsumption, inclusion abstraction, Timed Automata, UPPAAL, opaal, Parallel, LTL, LTSMIN, LU abstraction, liveness, Model Checking, Multi-Core, NDFS, Büchi emptiness, IR-84627, CNDFS, EWI-23158",
author = "Alfons Laarman and Olesen, {Mads Chr.} and Andreas Dalsgaard and Larsen, {Kim G.} and {van de Pol}, Jaco",
year = "2013",
month = "7",
doi = "10.1007/978-3-642-39799-8_69",
isbn = "978-3-642-39798-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "968--983",
editor = "Natasha Sharygina and Helmut Veith",
booktitle = "Computer Aided Verification",

}

Laarman, A, Olesen, MC, Dalsgaard, A, Larsen, KG & van de Pol, J 2013, Multi-core emptiness checking of timed Büchi automata using inclusion abstraction. in N Sharygina & H Veith (eds), Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. Lecture Notes in Computer Science, vol. 8044, Springer, London, pp. 968-983, 25th International Conference on Computer Aided Verification, CAV 2013, Saint Petersburg, Russian Federation, 13-19 July. DOI: 10.1007/978-3-642-39799-8_69

Multi-core emptiness checking of timed Büchi automata using inclusion abstraction. / Laarman, Alfons; Olesen, Mads Chr.; Dalsgaard, Andreas; Larsen, Kim G.; van de Pol, Jaco .

Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. ed. / Natasha Sharygina; Helmut Veith. London : Springer, 2013. p. 968-983 (Lecture Notes in Computer Science; Vol. 8044).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Multi-core emptiness checking of timed Büchi automata using inclusion abstraction

AU - Laarman,Alfons

AU - Olesen,Mads Chr.

AU - Dalsgaard,Andreas

AU - Larsen,Kim G.

AU - van de Pol,Jaco

PY - 2013/7/13

Y1 - 2013/7/13

N2 - 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.

AB - 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.

KW - FMT-MC: MODEL CHECKING

KW - METIS-296351

KW - subsumption

KW - inclusion abstraction

KW - Timed Automata

KW - UPPAAL

KW - opaal

KW - Parallel

KW - LTL

KW - LTSMIN

KW - LU abstraction

KW - liveness

KW - Model Checking

KW - Multi-Core

KW - NDFS

KW - Büchi emptiness

KW - IR-84627

KW - CNDFS

KW - EWI-23158

U2 - 10.1007/978-3-642-39799-8_69

DO - 10.1007/978-3-642-39799-8_69

M3 - Conference contribution

SN - 978-3-642-39798-1

T3 - Lecture Notes in Computer Science

SP - 968

EP - 983

BT - Computer Aided Verification

PB - Springer

ER -

Laarman A, Olesen MC, Dalsgaard A, Larsen KG, van de Pol J. Multi-core emptiness checking of timed Büchi automata using inclusion abstraction. In Sharygina N, Veith H, editors, Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. London: Springer. 2013. p. 968-983. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-642-39799-8_69