Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Decidability of Safety Properties of Timed Multiset Rewriting
| |
|
Decidability of Safety Properties of Timed Multiset Rewriting
Mitsuharu Yamamoto5  , Jean-Marie Cottin6 and Masami Hagiya6
| (5) |
Faculty of Science, Chiba University, Yayoicho 1-33, Inage-ku, Chiba, Japan |
| (6) |
Graduate School of Information Science and Technology, University of Tokyo, Hongo 7-3-1 Bunkyo-ku, Tokyo, Japan |
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
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|