Partial Order Reduction for Reachability Games

D 2019

Partial Order Reduction for Reachability Games

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

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

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

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ěněno: 3. 5. 2020 13:35, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Citovat

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.

@inproceedings{1646345,
   author = {Boenneland, Frederik M. and Jensen, Peter G. and Larsen, Kim G. and Muniz, Marco and Srba, Jiří},
   address = {Gernmany},
   booktitle = {Proceedings of the 30th International Conference on Concurrency Theory (CONCUR'19)},
   doi = {http://dx.doi.org/10.4230/LIPIcs.CONCUR.2019.23},
   keywords = {partial order reduction; Petri nets; reachability games},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Gernmany},
   isbn = {978-3-95977-121-4},
   pages = {1-15},
   publisher = {Dagstuhl Publishing},
   title = {Partial Order Reduction for Reachability Games},
   year = {2019}
}

TY  - JOUR
ID  - 1646345
AU  - Boenneland, Frederik M. - Jensen, Peter G. - Larsen, Kim G. - Muniz, Marco - Srba, Jiří
PY  - 2019
TI  - Partial Order Reduction for Reachability Games
PB  - Dagstuhl Publishing
CY  - Gernmany
SN  - 9783959771214
KW  - partial order reduction
KW  - Petri nets
KW  - reachability games
N2  - 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.
ER  -

BOENNELAND, Frederik M., Peter G. JENSEN, Kim G. LARSEN, Marco MUNIZ a Jiří SRBA. Partial Order Reduction for Reachability Games. Online. In \textit{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.

Podrobný výpis o publikaci