Start Pruning When Time Gets Urgent

Partial Order Reduction for Timed Systems

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

2 Citationer (Scopus)
96 Downloads (Pure)

Resumé

Partial order reduction for timed systems is a challenging topic due to the dependencies among events induced by time acting as a global synchronization mechanism. So far, there has only been a limited success in finding practically applicable solutions yielding significant state space reductions. We suggest a working and efficient method to facilitate stubborn set reduction for timed systems with urgent behaviour. We first describe the framework in the general setting of timed labelled transition systems and then instantiate it to the case of timed-arc Petri nets. The basic idea is that we can employ classical untimed partial order reduction techniques as long as urgent behaviour is enforced. Our solution is implemented in the model checker TAPAAL and the feature is now broadly available to the users of the tool. By a series of larger case studies, we document the benefits of our method and its applicability to real-world scenarios.
OriginalsprogEngelsk
TitelInternational Conference on Computer Aided Verification : CAV 2018: Computer Aided Verification
ForlagSpringer
Publikationsdato18 jul. 2018
Sider527-546
ISBN (Trykt)978-3-319-96144-6
ISBN (Elektronisk)978-3-319-96145-3
DOI
StatusUdgivet - 18 jul. 2018
BegivenhedInternational Conference on Computer Aided Verification - Oxford, Storbritannien
Varighed: 14 jul. 201817 jul. 2018

Konference

KonferenceInternational Conference on Computer Aided Verification
LandStorbritannien
ByOxford
Periode14/07/201817/07/2018
NavnLecture Notes in Computer Science
Vol/bind10981
ISSN0302-9743

Citer dette

Bønneland, F. M., Jensen, P. G., Larsen, K. G., Muniz, M., & Srba, J. (2018). Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems. I International Conference on Computer Aided Verification: CAV 2018: Computer Aided Verification (s. 527-546). Springer. Lecture Notes in Computer Science, Bind. 10981 https://doi.org/10.1007/978-3-319-96145-3_28
Bønneland, Fredrik Meyer ; Jensen, Peter Gjøl ; Larsen, Kim Guldstrand ; Muniz, Marco ; Srba, Jiri. / Start Pruning When Time Gets Urgent : Partial Order Reduction for Timed Systems. International Conference on Computer Aided Verification: CAV 2018: Computer Aided Verification. Springer, 2018. s. 527-546 (Lecture Notes in Computer Science, Bind 10981).
@inproceedings{5f4f1956cf0245a584203cd6c80baba6,
title = "Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems",
abstract = "Partial order reduction for timed systems is a challenging topic due to the dependencies among events induced by time acting as a global synchronization mechanism. So far, there has only been a limited success in finding practically applicable solutions yielding significant state space reductions. We suggest a working and efficient method to facilitate stubborn set reduction for timed systems with urgent behaviour. We first describe the framework in the general setting of timed labelled transition systems and then instantiate it to the case of timed-arc Petri nets. The basic idea is that we can employ classical untimed partial order reduction techniques as long as urgent behaviour is enforced. Our solution is implemented in the model checker TAPAAL and the feature is now broadly available to the users of the tool. By a series of larger case studies, we document the benefits of our method and its applicability to real-world scenarios.",
author = "B{\o}nneland, {Fredrik Meyer} and Jensen, {Peter Gj{\o}l} and Larsen, {Kim Guldstrand} and Marco Muniz and Jiri Srba",
year = "2018",
month = "7",
day = "18",
doi = "10.1007/978-3-319-96145-3_28",
language = "English",
isbn = "978-3-319-96144-6",
pages = "527--546",
booktitle = "International Conference on Computer Aided Verification",
publisher = "Springer",
address = "Germany",

}

Bønneland, FM, Jensen, PG, Larsen, KG, Muniz, M & Srba, J 2018, Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems. i International Conference on Computer Aided Verification: CAV 2018: Computer Aided Verification. Springer, Lecture Notes in Computer Science, bind 10981, s. 527-546, International Conference on Computer Aided Verification, Oxford, Storbritannien, 14/07/2018. https://doi.org/10.1007/978-3-319-96145-3_28

Start Pruning When Time Gets Urgent : Partial Order Reduction for Timed Systems. / Bønneland, Fredrik Meyer; Jensen, Peter Gjøl; Larsen, Kim Guldstrand; Muniz, Marco; Srba, Jiri.

International Conference on Computer Aided Verification: CAV 2018: Computer Aided Verification. Springer, 2018. s. 527-546 (Lecture Notes in Computer Science, Bind 10981).

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review

TY - GEN

T1 - Start Pruning When Time Gets Urgent

T2 - Partial Order Reduction for Timed Systems

AU - Bønneland, Fredrik Meyer

AU - Jensen, Peter Gjøl

AU - Larsen, Kim Guldstrand

AU - Muniz, Marco

AU - Srba, Jiri

PY - 2018/7/18

Y1 - 2018/7/18

N2 - Partial order reduction for timed systems is a challenging topic due to the dependencies among events induced by time acting as a global synchronization mechanism. So far, there has only been a limited success in finding practically applicable solutions yielding significant state space reductions. We suggest a working and efficient method to facilitate stubborn set reduction for timed systems with urgent behaviour. We first describe the framework in the general setting of timed labelled transition systems and then instantiate it to the case of timed-arc Petri nets. The basic idea is that we can employ classical untimed partial order reduction techniques as long as urgent behaviour is enforced. Our solution is implemented in the model checker TAPAAL and the feature is now broadly available to the users of the tool. By a series of larger case studies, we document the benefits of our method and its applicability to real-world scenarios.

AB - Partial order reduction for timed systems is a challenging topic due to the dependencies among events induced by time acting as a global synchronization mechanism. So far, there has only been a limited success in finding practically applicable solutions yielding significant state space reductions. We suggest a working and efficient method to facilitate stubborn set reduction for timed systems with urgent behaviour. We first describe the framework in the general setting of timed labelled transition systems and then instantiate it to the case of timed-arc Petri nets. The basic idea is that we can employ classical untimed partial order reduction techniques as long as urgent behaviour is enforced. Our solution is implemented in the model checker TAPAAL and the feature is now broadly available to the users of the tool. By a series of larger case studies, we document the benefits of our method and its applicability to real-world scenarios.

U2 - 10.1007/978-3-319-96145-3_28

DO - 10.1007/978-3-319-96145-3_28

M3 - Article in proceeding

SN - 978-3-319-96144-6

SP - 527

EP - 546

BT - International Conference on Computer Aided Verification

PB - Springer

ER -

Bønneland FM, Jensen PG, Larsen KG, Muniz M, Srba J. Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems. I International Conference on Computer Aided Verification: CAV 2018: Computer Aided Verification. Springer. 2018. s. 527-546. (Lecture Notes in Computer Science, Bind 10981). https://doi.org/10.1007/978-3-319-96145-3_28