Universal Safety for Timed Petri Nets is PSPACE-complete

ABSTRACT. Timed-arc Petri nets (TPN) are an extension of Petri nets where each token carries one real-valued clock and transitions are guarded by integer inequality constraints on clocks. We consider the model in which newly created tokens can either be reset, or inherit values of input tokens of the transition. The Existential Coverability problem for TPN asks, for a given place p and transition t, whether there exists a number m such that the marking M (m) = m·{(p, 0)} ultimately enables t. Here, M (m) contains exactly m tokens on place p with all clocks set to zero and no other tokens. This problem corresponds to checking safety properties in distributed networks of arbitrarily many (namely m) initially identical timed processes that communicate by handshake. A negative answer certifies that the ‘bad event’ of transition t can never happen regardless of the number m of processes, i. e. , the network is safe for any size. Thus by checking existential coverability, one solves the dual problem of Universal Safety. We show that both problems are decidable and PSPACE-complete. The lower bound is shown by a reduction from the iterated monotone Boolean circuit problem. The upper bound is shown by an acceleration technique for a suitable notion of (infinite) region automata. This moreover leads to a symbolic representation of the set of coverable configurations, which can be computed in exponential space.

Authors

• Patrick Totzke

Keywords

No keywords are indexed for this paper.