In: W. Damm, E.-R. Olderog (Eds.): Formal Techniques in Real-Time and Fault-Tolerant Systems, 7th International Symposium(FTRTFT 2002) Oldenburg, Germany, September 9-12, 2002, pages 1-165pp. Springer Verlag, LNCS 2469, October 2002.
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.
Keywords: real-time systems; timed Petri nets; timed automata; decidability.