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

doi:10.1007/978-3-642-39799-8_69

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

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

25 Citations (Scopus)

629 Downloads (Pure)

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, but some other structural properties are preserved. Based on those, we propose a variation of the classical nested depth-first search (NDFS) algorithm that exploits subsumption. In addition, we extend the multi-core cndfs algorithm with subsumption, providing the first parallel LTL model checking algorithm for timed automata.

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 case study, and the multi-core algorithm yields speedups of up to 40 using 48 cores.

Translated title of the contribution	Multi-Core Emptiness Checking of Timed Büchi Automata using Inclusion Abstraction
Original language	English
Title of host publication	Proceedings of the 25th International Conference on Computer Aided Verification (CAV)
Number of pages	16
Volume	8044
Publisher	Springer Publishing Company
Publication date	2013
Pages	968-983
ISBN (Print)	978-3-642-39798-1
ISBN (Electronic)	978-3-642-39799-8
DOIs	https://doi.org/10.1007/978-3-642-39799-8_69
Publication status	Published - 2013
Event	25th International Concerence on Computer Aided Verification - Saint Petersburg, Russian Federation Duration: 13 Jul 2013 → 19 Jul 2013 Conference number: 25th

Conference

Conference	25th International Concerence on Computer Aided Verification
Number	25th
Country/Territory	Russian Federation
City	Saint Petersburg
Period	13/07/2013 → 19/07/2013

Series	Lecture Notes in Computer Science
Volume	8044
ISSN	0302-9743

Access to Document

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

MultiCoreEmptinessCheckingofTimedBuchiAutomatausingInclusionAbstractionAccepted author manuscript, 438 KB

AUB Link

Search for the material in Aalborg University Library's search engine

MBAT: Model-based Analysis and Testing of Embedded Systems
Nielsen, B. (Project Participant), Larsen, K. G. (Project Participant), David, A. (Project Participant), Mikučionis, M. (Project Participant) & Skou, A. (Project Participant)
Artemis JU
01/11/2011 → 31/10/2014
Project: Research
IDEA4CPS: Foundations for Cyber-Physical Sytems
Larsen, K. G. (Project Licensee), Skou, A. (Project Participant), Nielsen, B. (Project Participant), Bulychev, P. (Project Participant), Ravn, A. P. (Project Participant) & Poulsen, D. B. (Project Participant)
01/04/2011 → 30/04/2015
Project: Research
MT-LAB: MT-LAB A VKR Foundation Center of Excellence
Larsen, K. G. (Project Manager), Skou, A. (Project Participant), Srba, J. (Project Participant), Ravn, A. P. (Project Participant), David, A. (Project Participant) & Wisniewski, R. (Project Participant)
VKR Centre of Excellence
01/10/2008 → 01/10/2013
Project: Research

Cite this

@inproceedings{63e14668e22d49be83e239a41252e8b2,

title = "Multi-Core Emptiness Checking of Timed B{\"u}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{\"u}chi emptiness under the very coarse inclusion abstraction or zone subsumption, an open problem in this field.We show that in general B{\"u}chi emptiness is not preserved under this abstraction, but some other structural properties are preserved. Based on those, we propose a variation of the classical nested depth-first search (NDFS) algorithm that exploits subsumption. In addition, we extend the multi-core cndfs algorithm with subsumption, providing the first parallel LTL model checking algorithm for timed automata.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 case study, and the multi-core algorithm yields speedups of up to 40 using 48 cores.",

author = "Alfons Laarman and Olesen, {Mads Chr.} and Andreas Dalsgaard and Larsen, {Kim G.} and Pol, {Jaco van de}",

year = "2013",

doi = "10.1007/978-3-642-39799-8_69",

language = "English",

isbn = "978-3-642-39798-1",

volume = "8044",

series = "Lecture Notes in Computer Science",

publisher = "Springer Publishing Company",

pages = "968--983",

booktitle = "Proceedings of the 25th International Conference on Computer Aided Verification (CAV)",

address = "United States",

note = "25th International Concerence on Computer Aided Verification ; Conference date: 13-07-2013 Through 19-07-2013",

}

Laarman, A, Olesen, MC, Dalsgaard, A, Larsen, KG & Pol, JVD 2013, Multi-Core Emptiness Checking of Timed Büchi Automata using Inclusion Abstraction. in Proceedings of the 25th International Conference on Computer Aided Verification (CAV). vol. 8044, Springer Publishing Company, Lecture Notes in Computer Science, vol. 8044, pp. 968-983, 25th International Concerence on Computer Aided Verification, Saint Petersburg, Russian Federation, 13/07/2013. https://doi.org/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 et al.
Proceedings of the 25th International Conference on Computer Aided Verification (CAV). Vol. 8044 Springer Publishing Company, 2013. p. 968-983 (Lecture Notes in Computer Science, Vol. 8044).

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

TY - GEN

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 - Pol, Jaco van de

N1 - Conference code: 25th

PY - 2013

Y1 - 2013

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, but some other structural properties are preserved. Based on those, we propose a variation of the classical nested depth-first search (NDFS) algorithm that exploits subsumption. In addition, we extend the multi-core cndfs algorithm with subsumption, providing the first parallel LTL model checking algorithm for timed automata.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 case study, and the multi-core algorithm yields speedups of up to 40 using 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, but some other structural properties are preserved. Based on those, we propose a variation of the classical nested depth-first search (NDFS) algorithm that exploits subsumption. In addition, we extend the multi-core cndfs algorithm with subsumption, providing the first parallel LTL model checking algorithm for timed automata.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 case study, and the multi-core algorithm yields speedups of up to 40 using 48 cores.

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

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

M3 - Article in proceeding

SN - 978-3-642-39798-1

VL - 8044

T3 - Lecture Notes in Computer Science

SP - 968

EP - 983

BT - Proceedings of the 25th International Conference on Computer Aided Verification (CAV)

PB - Springer Publishing Company

T2 - 25th International Concerence on Computer Aided Verification

Y2 - 13 July 2013 through 19 July 2013

ER -

Multi-Core Emptiness Checking of Timed Büchi Automata using Inclusion Abstraction

Abstract

Conference

Access to Document

AUB Link

Projects

MBAT: Model-based Analysis and Testing of Embedded Systems

IDEA4CPS: Foundations for Cyber-Physical Sytems

MT-LAB: MT-LAB A VKR Foundation Center of Excellence

Cite this