DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2015.456

Unfolding-based Partial Order Reduction

Authors: César Rodríguez, Marcelo Sousa, Subodh Sharma, and Daniel Kroening

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract

Partial order reduction (POR) and net unfoldings are two alternative methods to tackle state-space explosion caused by concurrency. In this paper, we propose the combination of both approaches in an effort to combine their strengths. We first define, for an abstract execution model, unfolding semantics parameterized over an arbitrary independence relation. Based on it, our main contribution is a novel stateless POR algorithm that explores at most one execution per Mazurkiewicz trace, and in general, can explore exponentially fewer, thus achieving a form of super-optimality. Furthermore, our unfolding-based POR copes with non-terminating executions and incorporates state caching. On benchmarks with busy-waits, among others, our experiments show a dramatic reduction in the number of executions when compared to a state-of-the-art DPOR.

Cite as

César Rodríguez, Marcelo Sousa, Subodh Sharma, and Daniel Kroening. Unfolding-based Partial Order Reduction. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 456-469, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{rodriguez_et_al:LIPIcs.CONCUR.2015.456,
  author =	{Rodr{\'\i}guez, C\'{e}sar and Sousa, Marcelo and Sharma, Subodh and Kroening, Daniel},
  title =	{{Unfolding-based Partial Order Reduction}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{456--469},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.456},
  URN =		{urn:nbn:de:0030-drops-53637},
  doi =		{10.4230/LIPIcs.CONCUR.2015.456},
  annote =	{Keywords: Partial order reduction, unfoldings, concurrency, model checking}
}

Document

DOI: 10.4230/OASIcs.FSFMA.2013.47

An Improved Construction of Petri Net Unfoldings

Authors: César Rodríguez and Stefan Schwoon

Published in: OASIcs, Volume 31, 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)

Abstract

Petri nets are a well-known model language for concurrent systems. The unfolding of a Petri net is an acyclic net bisimilar to the original one. Because it is acyclic, it admits simpler decision problems though it is in general larger than the net. In this paper, we revisit the problem of efficiently constructing an unfolding. We propose a new method that avoids computing the concurrency relation and therefore uses less memory than some other methods but still represents a good time-space tradeoff. We implemented the approach and report on experiments.

Cite as

César Rodríguez and Stefan Schwoon. An Improved Construction of Petri Net Unfoldings. In 1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013). Open Access Series in Informatics (OASIcs), Volume 31, pp. 47-52, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{rodriguez_et_al:OASIcs.FSFMA.2013.47,
  author =	{Rodr{\'\i}guez, C\'{e}sar and Schwoon, Stefan},
  title =	{{An Improved Construction of Petri Net Unfoldings}},
  booktitle =	{1st French Singaporean Workshop on Formal Methods and Applications (FSFMA 2013)},
  pages =	{47--52},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-56-9},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{31},
  editor =	{Choppy, Christine and Sun, Jun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FSFMA.2013.47},
  URN =		{urn:nbn:de:0030-drops-40875},
  doi =		{10.4230/OASIcs.FSFMA.2013.47},
  annote =	{Keywords: Concurrency, Petri nets, partial orders, unfoldings}
}

Search Results

Documents authored by Rodríguez, César

Unfolding-based Partial Order Reduction

Abstract

Cite as

An Improved Construction of Petri Net Unfoldings

Abstract

Cite as

Thanks for your feedback!

Could not send message