For the most recent entries see the Petri Nets Newsletter.

Decidability of Safety Properties of Timed Multiset Rewriting.

Yamamoto, Mitsuharu; Cottin, Jean-Marie; Hagiya, Masami

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.

Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography