Universal Safety for Timed Petri Nets is PSPACE-complete

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

doi:10.4230/LIPIcs.CONCUR.2018.6

Universal Safety for Timed Petri Nets is PSPACE-complete

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	29th International Conference on Concurrency Theory (CONCUR 2018)
Editors	Sven Schewe, Lijun Zhang
Publisher	Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
Pages	6:1--6:15
Number of pages	15
ISBN (Print)	978-3-95977-087-3
DOIs	https://doi.org/10.4230/LIPIcs.CONCUR.2018.6
Publication status	Published - 31 Aug 2018
Event	29th International Conference on Concurrency Theory (CONCUR 2018) - Beijing, China Duration: 4 Sep 2018 → 7 Sep 2018 http://lcs.ios.ac.cn/concur2018/

Publication series

Name	Leibniz International Proceedings in Informatics (LIPIcs)
Publisher	Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
Volume	118
ISSN (Print)	1868-8969

Conference

Conference	29th International Conference on Concurrency Theory (CONCUR 2018)
Abbreviated title	CONCUR 2018
Country/Territory	China
City	Beijing
Period	4/09/18 → 7/09/18
Internet address	http://lcs.ios.ac.cn/concur2018/

Access to Document

10.4230/LIPIcs.CONCUR.2018.6Licence: Creative Commons: Attribution (CC-BY)

Abdulla et alAccepted author manuscript, 457 KBLicence: Creative Commons: Attribution (CC-BY)

https://drops.dagstuhl.de/opus/volltexte/2018/9544/Licence: Creative Commons: Attribution (CC-BY)

Cite this

Abdulla, P. A., Atig, M. F., Ciobanu, R., Mayr, R., & Totzke, P. (2018). Universal Safety for Timed Petri Nets is PSPACE-complete. In S. Schewe, & L. Zhang (Eds.), 29th International Conference on Concurrency Theory (CONCUR 2018) (pp. 6:1--6:15). [6] (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 118). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. https://doi.org/10.4230/LIPIcs.CONCUR.2018.6

Abdulla, Parosh Aziz ; Atig, Mohamed Faouzi ; Ciobanu, Radu et al. / Universal Safety for Timed Petri Nets is PSPACE-complete. 29th International Conference on Concurrency Theory (CONCUR 2018). editor / Sven Schewe ; Lijun Zhang. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2018. pp. 6:1--6:15 (Leibniz International Proceedings in Informatics (LIPIcs)).

@inproceedings{f6ddfcf4cdf04c3a8ad7d1a3cbc7d0d1,

title = "Universal Safety for Timed Petri Nets is PSPACE-complete",

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.",

author = "Abdulla, {Parosh Aziz} and Atig, {Mohamed Faouzi} and Radu Ciobanu and Richard Mayr and Patrick Totzke",

year = "2018",

month = aug,

day = "31",

doi = "10.4230/LIPIcs.CONCUR.2018.6",

language = "English",

isbn = "978-3-95977-087-3",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany",

pages = "6:1----6:15",

editor = "Sven Schewe and Lijun Zhang",

booktitle = "29th International Conference on Concurrency Theory (CONCUR 2018)",

note = "29th International Conference on Concurrency Theory (CONCUR 2018), CONCUR 2018 ; Conference date: 04-09-2018 Through 07-09-2018",

url = "http://lcs.ios.ac.cn/concur2018/",

}

Abdulla, PA, Atig, MF, Ciobanu, R, Mayr, R & Totzke, P 2018, Universal Safety for Timed Petri Nets is PSPACE-complete. in S Schewe & L Zhang (eds), 29th International Conference on Concurrency Theory (CONCUR 2018)., 6, Leibniz International Proceedings in Informatics (LIPIcs), vol. 118, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, pp. 6:1--6:15, 29th International Conference on Concurrency Theory (CONCUR 2018), Beijing, China, 4/09/18. https://doi.org/10.4230/LIPIcs.CONCUR.2018.6

Universal Safety for Timed Petri Nets is PSPACE-complete. / Abdulla, Parosh Aziz; Atig, Mohamed Faouzi; Ciobanu, Radu et al.

29th International Conference on Concurrency Theory (CONCUR 2018). ed. / Sven Schewe; Lijun Zhang. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2018. p. 6:1--6:15 6 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 118).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Universal Safety for Timed Petri Nets is PSPACE-complete

AU - Abdulla, Parosh Aziz

AU - Atig, Mohamed Faouzi

AU - Ciobanu, Radu

AU - Mayr, Richard

AU - Totzke, Patrick

PY - 2018/8/31

Y1 - 2018/8/31

N2 - 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.

AB - 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.

UR - https://arxiv.org/abs/1806.08170

U2 - 10.4230/LIPIcs.CONCUR.2018.6

DO - 10.4230/LIPIcs.CONCUR.2018.6

M3 - Conference contribution

SN - 978-3-95977-087-3

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

SP - 6:1--6:15

BT - 29th International Conference on Concurrency Theory (CONCUR 2018)

A2 - Schewe, Sven

A2 - Zhang, Lijun

PB - Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany

T2 - 29th International Conference on Concurrency Theory (CONCUR 2018)

Y2 - 4 September 2018 through 7 September 2018

ER -

Abdulla PA, Atig MF, Ciobanu R, Mayr R, Totzke P. Universal Safety for Timed Petri Nets is PSPACE-complete. In Schewe S, Zhang L, editors, 29th International Conference on Concurrency Theory (CONCUR 2018). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. 2018. p. 6:1--6:15. 6. (Leibniz International Proceedings in Informatics (LIPIcs)). doi: 10.4230/LIPIcs.CONCUR.2018.6

Universal Safety for Timed Petri Nets is PSPACE-complete

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Energy Efficient Control

Cite this

Universal Safety for Timed Petri Nets is PSPACE-complete

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Projects

Energy Efficient Control

Cite this