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 proceedingKonferenceartikel i proceedingForskningpeer review

22 Citationer (Scopus)
388 Downloads (Pure)

Abstrakt

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 titelMulti-Core Emptiness Checking of Timed Büchi Automata using Inclusion Abstraction
OriginalsprogEngelsk
TitelProceedings of the 25th International Conference on Computer Aided Verification (CAV)
Antal sider16
Vol/bind8044
ForlagSpringer Publishing Company
Publikationsdato2013
Sider968-983
ISBN (Trykt)978-3-642-39798-1
ISBN (Elektronisk)978-3-642-39799-8
DOI
StatusUdgivet - 2013
Begivenhed25th International Concerence on Computer Aided Verification - Saint Petersburg, Rusland
Varighed: 13 jul. 201319 jul. 2013
Konferencens nummer: 25th

Konference

Konference25th International Concerence on Computer Aided Verification
Nummer25th
LandRusland
BySaint Petersburg
Periode13/07/201319/07/2013
NavnLecture Notes in Computer Science
Vol/bind8044
ISSN0302-9743

Citationsformater