Partial Order Reduction for Reachability Games
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Partial Order Reduction for Reachability Games
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
—
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2019
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of the 30th International Conference on Concurrency Theory (CONCUR'19)
ISBN
9783959771214
ISSN
1868-8969
e-ISSN
—
Number of pages
15
Pages from-to
1-15
Publisher name
Dagstuhl Publishing
Place of publication
Gernmany
Event location
Amsterdam
Event date
Jan 1, 2019
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—