Decidability of safety properties of timed multiset rewriting

Abstract

We propose timed multiset rewriting as a framework that subsumes timed Petri nets and timed automata. In timed multiset rewriting, which extends multiset rewriting, each element of a multiset has a clock, and a multiset is transformed not only by usual rewriting but also by time elapse. Moreover, we can specify conditions on clocks for rewriting. In this paper, we analyze reachability, boundedness, and coverability of timed multiset rewriting. Decidability of each property on the system depends on the presence of invariant rules and diagonal constraints. First, we show that all three properties are undecidable for systems with invariant rules. Then we show that reachability is undecidable, and both boundedness and coverability are decidable for the system without invariant rules. Finally, we show that all the three properties are undecidable if we include diagonal constraints even when excluding invariant rules.