Document Open Access Logo

Modelchecking counting properties of 1-safe nets with buffers in paraPSPACE

Authors M. Praveen, Kamal Lodaya

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2009.2331.pdf
  • Filesize: 264 kB
  • 12 pages

Document Identifiers

Subject Classification

Keywords
  • Petri nets
  • Coverability
  • Boundedness
  • paraPSPACE

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We consider concurrent systems that can be modelled as $1$-safe
  Petri nets communicating through a fixed set of buffers (modelled as
  unbounded places). We identify a parameter $\ben$, which we call
  ``benefit depth'', formed from the communication graph between the
  buffers. We show that for our system model, the coverability and boundedness
  problems can be solved in polynomial space assuming $\ben$ to be a
  fixed parameter, that is, the space requirement is $f(\ben)p(n)$,
  where $f$ is an exponential function and $p$ is a polynomial in
  the size of the input. We then obtain similar complexity bounds for
  modelchecking a logic based on such counting properties.
  This means that systems that have sparse communication patterns can
  be analyzed more efficiently than using previously
  known algorithms for general Petri nets.

Cite As Get BibTex

M. Praveen and Kamal Lodaya. Modelchecking counting properties of 1-safe nets with buffers in paraPSPACE. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 4, pp. 347-358, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009) https://doi.org/10.4230/LIPIcs.FSTTCS.2009.2331

Author Details

M. Praveen
Kamal Lodaya
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact