2026-07-24T06:00:52Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9544 2024-03-06T10:44:41Z ddc:004 open_access

Universal Safety for Timed Petri Nets is PSPACE-complete Abdulla, Parosh Aziz Atig, Mohamed Faouzi Ciobanu, Radu Mayr, Richard Totzke, Patrick timed networks safety checking Petri nets coverability 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Parosh Aziz Abdulla and Mohamed Faouzi Atig and Radu Ciobanu and Richard Mayr and Patrick Totzke 2018 Is Part Of LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2018.6 urn:nbn:de:0030-drops-95447 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.6 eng https://creativecommons.org/licenses/by/3.0/legalcode