Partial Order Reduction for Reachability Games

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F19%3A00113643" target="_blank" >RIV/00216224:14330/19:00113643 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.4230/LIPIcs.CONCUR.2019.23" target="_blank" >http://dx.doi.org/10.4230/LIPIcs.CONCUR.2019.23</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/LIPIcs.CONCUR.2019.23" target="_blank" >10.4230/LIPIcs.CONCUR.2019.23</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Partial Order Reduction for Reachability Games

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Partial Order Reduction for Reachability Games

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2019

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of the 30th International Conference on Concurrency Theory (CONCUR'19)

ISBN

9783959771214

ISSN

1868-8969

e-ISSN

—

Počet stran výsledku

15

Strana od-do

1-15

Název nakladatele

Dagstuhl Publishing

Místo vydání

Gernmany

Místo konání akce

Amsterdam

Datum konání akce

1. 1. 2019

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—