Document Open Access Logo

Universal Safety for Timed Petri Nets is PSPACE-complete

Authors Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr, Patrick Totzke

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2018.6.pdf
  • Filesize: 456 kB
  • 15 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
Keywords
  • timed networks
  • safety checking
  • Petri nets
  • coverability

Metrics

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

Abstract

A timed network consists of an arbitrary number of initially identical 1-clock timed automata, interacting via hand-shake communication. In this setting there is no unique central controller, since all automata are initially identical. We consider the universal safety problem for such controller-less timed networks, i.e., verifying that a bad event (enabling some given transition) is impossible regardless of the size of the network. 
This universal safety problem is dual to the existential coverability problem for timed-arc Petri nets, i.e., does there exist a number m of tokens, such that starting with m tokens in a given place, and none in the other places, some given transition is eventually enabled.
We show that these problems are PSPACE-complete.

Cite As Get BibTex

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr, and Patrick Totzke. Universal Safety for Timed Petri Nets is PSPACE-complete. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CONCUR.2018.6

Author Details

Parosh Aziz Abdulla
  • Uppsala University, Sweden
Mohamed Faouzi Atig
  • Uppsala University, Sweden
Radu Ciobanu
  • University of Edinburgh, UK
Richard Mayr
  • University of Edinburgh, UK
Patrick Totzke
  • University of Edinburgh, UK

Funding

This work was supported by the EPSRC, grant EP/M027651/1.

References

  1. Parosh Aziz Abdulla, Karlis Čerāns, Bengt Jonsson, and Yih-Kuen Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, 160(1-2):109-127, 2000. Google Scholar
  2. Parosh Aziz Abdulla, Johann Deneux, and Pritha Mahata. Multi-clock timed networks. In Annual IEEE Symposium on Logic in Computer Science (LICS), pages 345-354, 2004. Google Scholar
  3. Parosh Aziz Abdulla, Pritha Mahata, and Richard Mayr. Dense-timed Petri nets: Checking Zenoness, token liveness and boundedness. Logical Methods in Computer Science, 3(1), 2007. Google Scholar
  4. Parosh Aziz Abdulla and Aletta Nylén. Timed Petri nets and BQOs. In International Conference on Application and Theory of Petri Nets (ICATPN), volume 2075 of LNCS, pages 53-70. Springer, 2001. Google Scholar
  5. R. Alur and D. L. Dill. A theory of timed automata. tcs, 126(2):183-235, 1994. Google Scholar
  6. Benjamin Aminof, Sasha Rubin, Florian Zuleger, and Francesco Spegni. Liveness of parameterized timed networks. In International Colloquium on Automata, Languages and Programming (ICALP), volume 9135 of LNCS, 2015. Google Scholar
  7. Rémi Bonnet, Alain Finkel, Serge Haddad, and Fernando Rosa-Velardo. Comparing Petri data nets and timed Petri nets. Technical Report LSV-10-23, LSV Cachan, 2010. Google Scholar
  8. Patricia Bouyer, Serge Haddad, and Pierre-Alain Reynier. Timed Petri nets and timed automata: On the discriminating power of Zeno sequences. In International Colloquium on Automata, Languages and Programming (ICALP), pages 420-431. Springer, 2006. Google Scholar
  9. David de Frutos Escrig, Valentín Valero Ruiz, and Olga Marroquín Alonso. Decidability of properties of timed-arc Petri nets. In International Conference on Application and Theory of Petri Nets (ICATPN), volume 1825 of LNCS, pages 187-206. Springer, 2000. Google Scholar
  10. Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! tcs, 256(1-2):63-92, 2001. Google Scholar
  11. Eric Goles, Pedro Montealegre, Ville Salo, and Ilkka Törmä. PSPACE-completeness of majority automata networks. Theor. Comput. Sci., 609(1):118-128, 2016. Google Scholar
  12. Serge Haddad, Sylvain Schmitz, and Philippe Schnoebelen. The ordinal recursive complexity of timed-arc Petri nets, data nets, and other enriched nets. In Annual IEEE Symposium on Logic in Computer Science (LICS), pages 355-364, 2012. Google Scholar
  13. Lasse Jacobsen, Morten Jacobsen, Mikael H. Møller, and Jiří Srba. Verification of timed-arc Petri nets. In International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM), volume 6543 of LNCS, pages 46-72, 2011. Google Scholar
  14. Ranko Lazić, Tom Newcomb, Joël Ouaknine, A.W. Roscoe, and James Worrell. Nets with tokens which carry data. Fundamenta Informaticae, 88(3):251-274, 2008. Google Scholar
  15. Valentin Valero Ruiz, Fernando Cuartero Gomez, and David de Frutos Escrig. On non-decidability of reachability for timed-arc Petri nets. In International Workshop on Petri Nets and Performance Models. IEEE Computer Society, 1999. Google Scholar
  16. Jiří Srba. Timed-arc Petri nets vs. networks of timed automata. In International Conference on Application and Theory of Petri Nets (ICATPN), volume 3536 of LNCS, pages 385-402. Springer, 2005. Google Scholar
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