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. s. 527-546. ISBN 978-3-319-96144-6. doi:10.1007/978-3-319-96145-3_28. 2018.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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"
WWW 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 0302-9743
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ěnil Změnil: Mgr. Michal Petr, učo 65024. Změněno: 16. 5. 2022 14:34.
Anotace
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.
VytisknoutZobrazeno: 20. 4. 2024 01:50