Start Pruning When Time Gets Urgent: Partial Order Reduction
for Timed Systems

D 2018

Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems

BOENNELAND, Frederik M., Peter G. JENSEN, Kim G. LARSEN, Marco MUNIZ, Jiří SRBA et. al.

Základní údaje

Originální název

Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems

Autoři

BOENNELAND, Frederik M. (208 Dánsko), Peter G. JENSEN (208 Dánsko), Kim G. LARSEN (208 Dánsko), Marco MUNIZ (604 Peru) a Jiří SRBA (203 Česká republika, garant, domácí)

Vydání

Netherlands, Proceedings of the 30th International Conference on Computer Aided Verification (CAV'18), od s. 527-546, 20 s. 2018

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/18:00106625

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-96144-6

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-96145-3_28

UT WoS

000491481600028

Klíčová slova anglicky

partial order reduction; timed-arc Petri nets; stubborn sets

Štítky

core_A, firank_1

Změněno: 16. 5. 2022 14:34, Mgr. Michal Petr

Anotace

V originále

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.

Citovat

BOENNELAND, Frederik M., Peter G. JENSEN, Kim G. LARSEN, Marco MUNIZ a Jiří SRBA. Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems. In Proceedings of the 30th International Conference on Computer Aided Verification (CAV'18). Netherlands: Springer, 2018, s. 527-546. ISBN 978-3-319-96144-6. Dostupné z: https://dx.doi.org/10.1007/978-3-319-96145-3_28.

@inproceedings{1506124,
   author = {Boenneland, Frederik M. and Jensen, Peter G. and Larsen, Kim G. and Muniz, Marco and Srba, Jiří},
   address = {Netherlands},
   booktitle = {Proceedings of the 30th International Conference on Computer Aided Verification (CAV'18)},
   doi = {http://dx.doi.org/10.1007/978-3-319-96145-3_28},
   keywords = {partial order reduction; timed-arc Petri nets; stubborn sets},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Netherlands},
   isbn = {978-3-319-96144-6},
   pages = {527-546},
   publisher = {Springer},
   title = {Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems},
   url = {https://link.springer.com/chapter/10.1007%2F978-3-319-96145-3_28},
   year = {2018}
}

TY  - JOUR
ID  - 1506124
AU  - Boenneland, Frederik M. - Jensen, Peter G. - Larsen, Kim G. - Muniz, Marco - Srba, Jiří
PY  - 2018
TI  - Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems
PB  - Springer
CY  - Netherlands
SN  - 9783319961446
KW  - partial order reduction
KW  - timed-arc Petri nets
KW  - stubborn sets
UR  - https://link.springer.com/chapter/10.1007%2F978-3-319-96145-3_28
L2  - https://link.springer.com/chapter/10.1007%2F978-3-319-96145-3_28
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.
ER  -

BOENNELAND, Frederik M., Peter G. JENSEN, Kim G. LARSEN, Marco MUNIZ a Jiří SRBA. Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems. In \textit{Proceedings of the 30th International Conference on Computer Aided Verification (CAV'18)}. Netherlands: Springer, 2018, s.~527-546. ISBN~978-3-319-96144-6. Dostupné z: https://dx.doi.org/10.1007/978-3-319-96145-3\_{}28.

Podrobný výpis o publikaci