Multi-Core Reachability for Timed Automata

Andreas Dalsgaard, Alfons Laarman, K.G. Larsen, Mads Chr. Olesen, Jan Cornelis van de Pol

  • 12 Citations

Abstract

Model checking of timed automata is a widely used technique. But in order to take advantage of modern hardware, the algorithms need to be parallelized. We present a multi-core reachability algorithm for the more general class of well-structured transition systems, and an implementation for timed automata. Our implementation extends the opaal tool to generate a timed automaton successor generator in c++, that is efficient enough to compete with the UPPAAL model checker, and can be used by the discrete model checker LTSmin, whose parallel reachability algorithms are now extended to handle subsumption of semi-symbolic states. The reuse of efficient lockless data structures guarantees high scalability and efficient memory use. With experiments we show that opaal+LTSmin can outperform the current state-of-the-art, UPPAAL. The added parallelism is shown to reduce verification times from minutes to mere seconds with speedups of up to 40 on a 48-core machine. Finally, strict BFS and (surprisingly) parallel DFS search order are shown to reduce the state count, and improve speedups.
Original languageUndefined
Title of host publication10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012
EditorsM. Jurdzinski, D. Nickovic
Place of PublicationLondon
PublisherSpringer Verlag
Pages91-106
Number of pages16
ISBN (Print)978-3-642-33365-1
DOIs
StatePublished - 18 Sep 2012
Event10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012 - London, United Kingdom

Publication series

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

Conference

Conference10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012
Abbreviated titleFORMATS
CountryUnited Kingdom
CityLondon
Period18/09/1220/09/12
Internet address

Fingerprint

Model checking
Parallel algorithms
Data structures
Scalability
Hardware
Experiments

Keywords

  • METIS-287893
  • Abstraction
  • IR-80819
  • Multi-Core
  • Model Checking
  • well-quasi-ordering
  • EWI-21972
  • lockless
  • lattice-based model checking
  • Timed Automata
  • Symbolic reachability
  • Parallel
  • FMT-MC: MODEL CHECKING
  • hash table

Cite this

Dalsgaard, A., Laarman, A., Larsen, K. G., Olesen, M. C., & van de Pol, J. C. (2012). Multi-Core Reachability for Timed Automata. In M. Jurdzinski, & D. Nickovic (Eds.), 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012 (pp. 91-106). (Lecture Notes in Computer Science; Vol. 7595). London: Springer Verlag. DOI: 10.1007/978-3-642-33365-1_8

Dalsgaard, Andreas; Laarman, Alfons; Larsen, K.G.; Olesen, Mads Chr.; van de Pol, Jan Cornelis / Multi-Core Reachability for Timed Automata.

10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012. ed. / M. Jurdzinski; D. Nickovic. London : Springer Verlag, 2012. p. 91-106 (Lecture Notes in Computer Science; Vol. 7595).

Research output: Scientific - peer-reviewConference contribution

@inbook{4aa2a8736fa4455d87f587cd51a6869e,
title = "Multi-Core Reachability for Timed Automata",
abstract = "Model checking of timed automata is a widely used technique. But in order to take advantage of modern hardware, the algorithms need to be parallelized. We present a multi-core reachability algorithm for the more general class of well-structured transition systems, and an implementation for timed automata. Our implementation extends the opaal tool to generate a timed automaton successor generator in c++, that is efficient enough to compete with the UPPAAL model checker, and can be used by the discrete model checker LTSmin, whose parallel reachability algorithms are now extended to handle subsumption of semi-symbolic states. The reuse of efficient lockless data structures guarantees high scalability and efficient memory use. With experiments we show that opaal+LTSmin can outperform the current state-of-the-art, UPPAAL. The added parallelism is shown to reduce verification times from minutes to mere seconds with speedups of up to 40 on a 48-core machine. Finally, strict BFS and (surprisingly) parallel DFS search order are shown to reduce the state count, and improve speedups.",
keywords = "METIS-287893, Abstraction, IR-80819, Multi-Core, Model Checking, well-quasi-ordering, EWI-21972, lockless, lattice-based model checking, Timed Automata, Symbolic reachability, Parallel, FMT-MC: MODEL CHECKING, hash table",
author = "Andreas Dalsgaard and Alfons Laarman and K.G. Larsen and Olesen, {Mads Chr.} and {van de Pol}, {Jan Cornelis}",
year = "2012",
month = "9",
doi = "10.1007/978-3-642-33365-1_8",
isbn = "978-3-642-33365-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "91--106",
editor = "M. Jurdzinski and D. Nickovic",
booktitle = "10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012",
address = "Germany",

}

Dalsgaard, A, Laarman, A, Larsen, KG, Olesen, MC & van de Pol, JC 2012, Multi-Core Reachability for Timed Automata. in M Jurdzinski & D Nickovic (eds), 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012. Lecture Notes in Computer Science, vol. 7595, Springer Verlag, London, pp. 91-106, 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012, London, United Kingdom, 18-20 September. DOI: 10.1007/978-3-642-33365-1_8

Multi-Core Reachability for Timed Automata. / Dalsgaard, Andreas; Laarman, Alfons; Larsen, K.G.; Olesen, Mads Chr.; van de Pol, Jan Cornelis.

10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012. ed. / M. Jurdzinski; D. Nickovic. London : Springer Verlag, 2012. p. 91-106 (Lecture Notes in Computer Science; Vol. 7595).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Multi-Core Reachability for Timed Automata

AU - Dalsgaard,Andreas

AU - Laarman,Alfons

AU - Larsen,K.G.

AU - Olesen,Mads Chr.

AU - van de Pol,Jan Cornelis

PY - 2012/9/18

Y1 - 2012/9/18

N2 - Model checking of timed automata is a widely used technique. But in order to take advantage of modern hardware, the algorithms need to be parallelized. We present a multi-core reachability algorithm for the more general class of well-structured transition systems, and an implementation for timed automata. Our implementation extends the opaal tool to generate a timed automaton successor generator in c++, that is efficient enough to compete with the UPPAAL model checker, and can be used by the discrete model checker LTSmin, whose parallel reachability algorithms are now extended to handle subsumption of semi-symbolic states. The reuse of efficient lockless data structures guarantees high scalability and efficient memory use. With experiments we show that opaal+LTSmin can outperform the current state-of-the-art, UPPAAL. The added parallelism is shown to reduce verification times from minutes to mere seconds with speedups of up to 40 on a 48-core machine. Finally, strict BFS and (surprisingly) parallel DFS search order are shown to reduce the state count, and improve speedups.

AB - Model checking of timed automata is a widely used technique. But in order to take advantage of modern hardware, the algorithms need to be parallelized. We present a multi-core reachability algorithm for the more general class of well-structured transition systems, and an implementation for timed automata. Our implementation extends the opaal tool to generate a timed automaton successor generator in c++, that is efficient enough to compete with the UPPAAL model checker, and can be used by the discrete model checker LTSmin, whose parallel reachability algorithms are now extended to handle subsumption of semi-symbolic states. The reuse of efficient lockless data structures guarantees high scalability and efficient memory use. With experiments we show that opaal+LTSmin can outperform the current state-of-the-art, UPPAAL. The added parallelism is shown to reduce verification times from minutes to mere seconds with speedups of up to 40 on a 48-core machine. Finally, strict BFS and (surprisingly) parallel DFS search order are shown to reduce the state count, and improve speedups.

KW - METIS-287893

KW - Abstraction

KW - IR-80819

KW - Multi-Core

KW - Model Checking

KW - well-quasi-ordering

KW - EWI-21972

KW - lockless

KW - lattice-based model checking

KW - Timed Automata

KW - Symbolic reachability

KW - Parallel

KW - FMT-MC: MODEL CHECKING

KW - hash table

U2 - 10.1007/978-3-642-33365-1_8

DO - 10.1007/978-3-642-33365-1_8

M3 - Conference contribution

SN - 978-3-642-33365-1

T3 - Lecture Notes in Computer Science

SP - 91

EP - 106

BT - 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012

PB - Springer Verlag

ER -

Dalsgaard A, Laarman A, Larsen KG, Olesen MC, van de Pol JC. Multi-Core Reachability for Timed Automata. In Jurdzinski M, Nickovic D, editors, 10th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2012. London: Springer Verlag. 2012. p. 91-106. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-642-33365-1_8