Computation of Summaries Using Net Unfoldings

Authors Javier Esparza, Loig Jezequel, Stefan Schwoon

Thumbnail PDF


  • Filesize: 0.57 MB
  • 12 pages

Document Identifiers

Author Details

Javier Esparza
Loig Jezequel
Stefan Schwoon

Cite AsGet BibTex

Javier Esparza, Loig Jezequel, and Stefan Schwoon. Computation of Summaries Using Net Unfoldings. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 225-236, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


We study the following summarization problem: given a parallel composition A=A_1||...||A_n of labelled transition systems communicating with the environment through a distinguished component A_i, efficiently compute a summary S_i such that E||A and E||S_i are trace-equivalent for every environment E. While Si can be computed using elementary automata theory, the resulting algorithm suffers from the state-explosion problem. We present a new, simple but subtle algorithm based on net unfoldings, a partial-order semantics, give some experimental results using an implementation on top of MOLE, and show that our algorithm can handle divergences and compute weighted summaries with minor modifications.
  • Net unfoldings
  • Concurrent systems
  • Petri nets


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail