Title
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.
Year
DOI
Venue
2002
10.1007/3-540-45739-9_12
FTRTFT
Keywords
Field
DocType
safety properties,time elapse,petri net,timed multiset rewriting,diagonal constraint,invariant rule,real time systems,decidability
Discrete mathematics,Petri net,Multiset,Computer science,Decidability,Reachability,Confluence,Invariant (mathematics),Rewriting,Distributed computing,Undecidable problem
Conference
ISBN
Citations 
PageRank 
3-540-44165-4
1
0.36
References 
Authors
18
3
Name
Order
Citations
PageRank
Mitsuharu Yamamoto19111.09
Jean-Marie Cottin210.36
Masami Hagiya3649102.85