BOENNELAND, Frederik M., Peter G. JENSEN, Kim G. LARSEN, Marco MUNIZ a Jiří SRBA. Partial Order Reduction for Reachability Games. Online. In Proceedings of the 30th International Conference on Concurrency Theory (CONCUR'19). Gernmany: Dagstuhl Publishing, 2019, s. 1-15. ISBN 978-3-95977-121-4. Dostupné z: https://dx.doi.org/10.4230/LIPIcs.CONCUR.2019.23.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Partial Order Reduction for Reachability Games
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í Gernmany, Proceedings of the 30th International Conference on Concurrency Theory (CONCUR'19), od s. 1-15, 15 s. 2019.
Nakladatel Dagstuhl Publishing
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
Forma vydání elektronická verze "online"
Kód RIV RIV/00216224:14330/19:00113643
Organizační jednotka Fakulta informatiky
ISBN 978-3-95977-121-4
ISSN 1868-8969
Doi http://dx.doi.org/10.4230/LIPIcs.CONCUR.2019.23
Klíčová slova anglicky partial order reduction; Petri nets; reachability games
Štítky core_A, firank_A
Změnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 3. 5. 2020 13:35.
Anotace
Partial order reductions have been successfully applied to model checking of concurrent systems and practical applications of the technique show nontrivial reduction in the size of the explored state space. We present a theory of partial order reduction based on stubborn sets in the game-theoretical setting of 2-player games with reachability/safety objectives. Our stubborn reduction allows us to prune the interleaving behaviour of both players in the game, and we formally prove its correctness on the class of games played on general labelled transition systems. We then instantiate the framework to the class of weighted Petri net games with inhibitor arcs and provide its efficient implementation in the model checker TAPAAL. Finally, we evaluate our stubborn reduction on several case studies and demonstrate its efficiency.
VytisknoutZobrazeno: 27. 4. 2024 00:29