DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2019.23

Partial Order Reduction for Reachability Games

Authors: Frederik Meyer Bønneland, Peter Gjøl Jensen, Kim G. Larsen, Marco Muñiz, and Jiří Srba

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract

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.

Cite as

Frederik Meyer Bønneland, Peter Gjøl Jensen, Kim G. Larsen, Marco Muñiz, and Jiří Srba. Partial Order Reduction for Reachability Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 23:1-23:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{bnneland_et_al:LIPIcs.CONCUR.2019.23,
  author =	{B{\o}nneland, Frederik Meyer and Jensen, Peter Gj{\o}l and Larsen, Kim G. and Mu\~{n}iz, Marco and Srba, Ji\v{r}{\'\i}},
  title =	{{Partial Order Reduction for Reachability Games}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{23:1--23:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.23},
  URN =		{urn:nbn:de:0030-drops-109251},
  doi =		{10.4230/LIPIcs.CONCUR.2019.23},
  annote =	{Keywords: Petri nets, games, synthesis, partial order reduction, stubborn sets}
}

Search Results

Documents authored by Jensen, Peter Gjøl

Partial Order Reduction for Reachability Games

Abstract

Cite as

Thanks for your feedback!

Could not send message