Skip to main content
SpringerLink
Log in

A Complete Axiomatisation for Timed Automata

  • Conference paper
  • First Online:
Book cover FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1974))

  • 548 Accesses

Abstract

In this paper we present a complete proof system for timed automata. It extends our previous axiomatisation of timed bisimulation for the class of loop-free timed automata with unique fixpoint induction. To our knowledge, this is the first algebraic theory for the whole class of timed automata with a completeness result, thus fills a gap in the theory of timed automata. The proof of the completeness result relies on the notion of symbolic timed bisimulation, adapted from the work on value-passing processes.

Supported by a grant from National Science Foundation of China.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. E. Asarin, P. Caspi and O. Maler. A Kleene theorem for timed automata. In proceedings of LICS’97, 1997.

    Google Scholar 

  2. R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235. 1994.

    Article  MATH  MathSciNet  Google Scholar 

  3. L. Aceto and A. Jeffrey. A complete axiomatization of timed bisimulation for a class of timed regular behaviours. Theoretical Computer Science, 152(2):251–268. 1995.

    Article  MATH  MathSciNet  Google Scholar 

  4. M. Boreale. Symbolic Bisimulation for Timed Processes. InAMAST’96, LNCS 1101 pp.321–335. Springer-Verlag. 1996.

    Google Scholar 

  5. P. Bouyer and A. Petit. Decomposition and Composition of Timed Automata. In ICALP’99, LNCS 1644, pp. 210–219. Springer-Verlag. 1999.

    Google Scholar 

  6. S. Bornot and J. Sifakis. An Algebraic Framework for Urgency. In Calculational System Design, NATO Science Series, Computer and Systems Science 173, Marktoberdorf, July 1998.

    Google Scholar 

  7. K. Čeräns. Decidability of Bisimulation Equivalences for Parallel Timer Processes. In CAV’92, LNCS 663, pp.302–315. Springer-Verlag. 1992.

    Google Scholar 

  8. P.R. D’Argenio and Ed Brinksma. A Calculus for Timed Automata (Extended Abstract). In FTRTFTS’96, LNCS 1135, pp.110–129. 1996.

    Google Scholar 

  9. M. Hennessy and H. Lin. Symbolic bisimulations. Theoretical Computer Science, 138:353–389, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  10. M. Hennessy and H. Lin. Proof systems for message-passing process algebras. Formal Aspects of Computing, 8:408–427, 1996.

    Article  Google Scholar 

  11. H. Lin and Y. Wang. A proof system for timed automata. Fossacs’2000, LNCS 1784. March 2000.

    Google Scholar 

  12. H. Lin and Y. Wang. A complete proof system for timed automata (Full version). Available at: http://www.it.uu.se/research/reports/.

  13. R. Milner. A complete inference system for a class of regular behaviours. J. Computer and System Science, 28:439–466, 1984.

    Article  MATH  MathSciNet  Google Scholar 

  14. R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

    Google Scholar 

  15. Wang Yi. A Calculus of Real Time Systems. Ph.D. thesis, Chalmers University, 1991.

    Google Scholar 

  16. Wang Yi, Paul Pettersson, and Mats Daniels. Automatic Verification of Real-Time Communicating Systems By Constraint-Solving. In Proc. of the 7th International Conference on Formal Description Techniques, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences, China

    Huimin Lin

  2. Department of Computer Systems, Uppsala University, Uppsala

    Wang Yi

Authors
  1. Huimin Lin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wang Yi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, Indian Institute of Technology, Delhi, Hauz Khas, 110016, New Delhi, India

    Sanjiv Kapoor  & Sanjiva Prasad  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lin, H., Yi, W. (2000). A Complete Axiomatisation for Timed Automata. In: Kapoor, S., Prasad, S. (eds) FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2000. Lecture Notes in Computer Science, vol 1974. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44450-5_22

Download citation

  • DOI: https://doi.org/10.1007/3-540-44450-5_22

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41413-1

  • Online ISBN: 978-3-540-44450-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation