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

Bidragets oversatte titel: 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

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › peer review

25 Citationer (Scopus)

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

Bidragets oversatte titel	Multi-Core Emptiness Checking of Timed Büchi Automata using Inclusion Abstraction
Originalsprog	Engelsk
Titel	Proceedings of the 25th International Conference on Computer Aided Verification (CAV)
Antal sider	16
Vol/bind	8044
Forlag	Springer Publishing Company
Publikationsdato	2013
Sider	968-983
ISBN (Trykt)	978-3-642-39798-1
ISBN (Elektronisk)	978-3-642-39799-8
DOI	https://doi.org/10.1007/978-3-642-39799-8_69
Status	Udgivet - 2013
Begivenhed	25th International Concerence on Computer Aided Verification - Saint Petersburg, Rusland Varighed: 13 jul. 2013 → 19 jul. 2013 Konferencens nummer: 25th

Konference

Konference	25th International Concerence on Computer Aided Verification
Nummer	25th
Land/Område	Rusland
By	Saint Petersburg
Periode	13/07/2013 → 19/07/2013

Navn	Lecture Notes in Computer Science
Vol/bind	8044
ISSN	0302-9743

Adgang til dokumentet

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

MultiCoreEmptinessCheckingofTimedBuchiAutomatausingInclusionAbstractionAccepteret manuskript, 438 KB

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

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

Citationsformater

@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. i Proceedings of the 25th International Conference on Computer Aided Verification (CAV). bind 8044, Springer Publishing Company, Lecture Notes in Computer Science, bind 8044, s. 968-983, 25th International Concerence on Computer Aided Verification, Saint Petersburg, Rusland, 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). Bind 8044 Springer Publishing Company, 2013. s. 968-983 (Lecture Notes in Computer Science, Bind 8044).

Publikation: Bidrag til bog/antologi/rapport/konference proceeding › Konferenceartikel i proceeding › Forskning › 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

Konference

Adgang til dokumentet

AUB Link

Projekter

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

Citationsformater