D 2019

Partial Order Reduction for Reachability Games

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

Basic information

Original name

Partial Order Reduction for Reachability Games

Authors

BOENNELAND, Frederik M. (208 Denmark), Peter G. JENSEN (208 Denmark), Kim G. LARSEN (208 Denmark), Marco MUNIZ (604 Peru) and Jiří SRBA (203 Czech Republic, guarantor, belonging to the institution)

Edition

Gernmany, Proceedings of the 30th International Conference on Concurrency Theory (CONCUR'19), p. 1-15, 15 pp. 2019

Publisher

Dagstuhl Publishing

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

electronic version available online

RIV identification code

RIV/00216224:14330/19:00113643

Organization unit

Faculty of Informatics

ISBN

978-3-95977-121-4

ISSN

DOI

Keywords in English

partial order reduction; Petri nets; reachability games

Tags

Změněno: 3/5/2020 13:35, RNDr. Pavel Šmerk, Ph.D.

Abstract

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.