Decidability of Safety Properties of Timed Multiset Rewriting

  • Mitsuharu Yamamoto
  • Jean-Marie Cottin
  • Masami Hagiya
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2469)


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 


  1. 1.
    Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96 (1992) 73–155zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Cervesato, I., Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: A meta-notation for protocol analysis. In: IEEE CSFW. (1999) 55–69Google Scholar
  3. 3.
    Kosiuczenko, P., Wirsing, M.: Timed rewriting logic for the specification of time-sensitive systems. In Schwichtenberg, H., ed.: Proceedings of the Internat. Summer School on Proof and Computation. (1995)Google Scholar
  4. 4.
    Ölveczky, P.C., Meseguer, J.: Specifying real-time systems in rewriting logic. In: Electronic Notes in Theoretical Computer Science. Volume 4. (1996)Google Scholar
  5. 5.
    Kanovich, M., Okada, M., Scedrov, A.: Specifying real-time finite-state systems in linear logic (1998)Google Scholar
  6. 6.
    Hagiya, M., Yamamoto, M., Cottin, J.M.: Symbolic analysis of timed multiset rewriting and its application to protocol analysis (extended abstract). In: Rewriting in Proof and Computation, International Workshop, RPC’01, The Research Institute of Electrical Communication (RIEC), Tohoku University (2001) 34–41Google Scholar
  7. 7.
    Bozzano, M., Delzanno, G., Martelli, M.: An effective bottom-up semantics for first-order linear logic programs. In: FLOPS. (2001) 138–152Google Scholar
  8. 8.
    Cerone, A., Maggiolo-Schettini, A.: Time-based expressivity of time Petri nets for system specification. Theoretical Computer Science 216 (1999) 1–53zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126 (1994) 183–236zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Henzinger, T.: The theory of hybrid automata. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS’ 96), New Brunswick, New Jersey (1996) 278–292Google Scholar
  11. 11.
    Ruiz, V.V., Gomez, F.C., de Frutos Escrig, D.: On non-decidability of reachability for timed-arc Petri nets. In: Proc. 8th Int. Workshop on Petri Net and Performance Models (PNPM’99), 8-10 October 1999, Zaragoza, Spain. (1999) 188–196Google Scholar
  12. 12.
    de Frutos Escrig, D., Ruiz, V.V., Alonso, O.M.: Decidability of properties of timed-arc Petri nets. In Nielsen, M., Simpson, D., eds.: Lecture Notes in Computer Science: 21st International Conference on Application and Theory of Petri Nets (ICATPN 2000), Aarhus, Denmark, June 2000. Volume 1825., Springer-Verlag (2000) 187–206Google Scholar
  13. 13.
    Abdulla, P.A., Nylén, A.: Timed Petri nets and BQOs. In: Proc. ICATPN’2001, 22nd Int. Conf. on application and theory of Petri nets. Volume 2075 of LNCS. (2001) 53–70CrossRefGoogle Scholar
  14. 14.
    T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine: Symbolic Model Checking for Real-Time Systems. In: 7th. Symposium of Logics in Computer Science, Santa-Cruz, California, IEEE Computer Scienty Press (1992) 394–406Google Scholar
  15. 15.
    Alur, R., Henzinger, T.A.: Real-time system = discrete system + clock variables. International Journal on Software Tools for Technology Transfer 1 (1997) 86–109zbMATHCrossRefGoogle Scholar
  16. 16.
    Abdulla, P.A., Jonsson, B.: Verifying networks of timed processes. Lecture Notes in Computer Science 1384 (1998) 298–312Google Scholar
  17. 17.
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere ! Theoretical Computer Science 256 (2001) 64–92CrossRefMathSciNetGoogle Scholar
  18. 18.
    Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Are timed automata updatable ? In: Proc. 12th Int. Conf. Computer Aided Verification (CAV’2000), Chicago, IL, USA, July 2000. Volume 1855., Springer (2000) 464–479CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Mitsuharu Yamamoto
    • 1
  • Jean-Marie Cottin
    • 2
  • Masami Hagiya
    • 2
  1. 1.Faculty of ScienceChiba UniversityChibaJapan
  2. 2.Graduate School of Information Science and TechnologyUniversity of TokyoTokyoJapan

Personalised recommendations