Automata and their interaction: Definitional suggestions

  • Boris A. Trakhtenbrot
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1684)


There is a growing feeling in the community that the current literature on reactive and hybrid systems is plagued by a Babel of models, constructs and formalisms, and by an amazing discord of terminology and notation. Further models and formalisms are engendered, and it is not clear where to stop.

Hence, the urge toward a pithy conceptual/notational setting, supported by a consistent and comprehensive taxonomy for a wide range of formalisms and models.

The paper outlines an automata-based approach to this challenge, which emerged in previous research [PRT, RT] and in teaching experience [T1,


Hybrid System Label Transition System Hybrid Automaton Time Automaton Deterministic Automaton 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Ab.
    Abramsky, S.: Private communication, 1997Google Scholar
  2. AL.
    Abadi, M., Lamport, L.: An old-fashioned recipe for real time. REX workshop on real time: Theory in Practice, 1991Google Scholar
  3. AD.
    Alur, R., Dill, D.: Automata for modelling real-time systems. Proceedings of ICALP90, LNCS 443 (1990) pp. 332–335Google Scholar
  4. AFH.
    Alur, R., Fix, L., Henzinger, T.: A deterministic class of timed automata. Proc. CAV’94, LNCS 818, pp. 1–13Google Scholar
  5. AH.
    Alur, R., Henzinger, T.: Logics and models for real time: theory in practice. LNCS 600 (1992) pp. 74–106Google Scholar
  6. ACHP.
    Alur, A., Courcoubetis, C., Henzinger, T., Pei-Sin, Ho.: Hybrid automata: approach to the specification and verification of hybrid systems. LNCS 736 (1993) pp. 209–229Google Scholar
  7. AO.
    Apt, K. Olderog, E.R.: Verification of Sequential and Concurrent Programs, Springer Verlag, 1991Google Scholar
  8. A.
    Artstein, Z.: Examples of stabilization with hybrid feedback. LNCS 1066 (1996) pp. 173–185Google Scholar
  9. Br.
    Broy, M.: Semantics of finite and infinite networks of concurrent communicating agents. Distributed Computing 2 (1987) 13–31zbMATHCrossRefGoogle Scholar
  10. BW.
    Burks, A.W., Wright, J.B.: Theory of logical nets. Proceedings of the I.R.E., 1953Google Scholar
  11. CM.
    Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation, Addison-Wessley, 1988Google Scholar
  12. DC.
    Dill, D., Clarke, E.: Automatic verification of asynchronous circuits using temporal logic. IEEE Proc. 133 (1986) 276Google Scholar
  13. F.
    Francez, N.: Programm Verification, Addison-Wesley P.C., 1992Google Scholar
  14. G.
    Gordon, M.: Why higher-order logic is a good formalism for specifying and verifying hardware. Formal Aspects of VLSI design, Elsevier Science Publ., pp.153–177, 1986Google Scholar
  15. H.
    Henzinger, T.: The theory of hybrid automata. Proceedings of the IEEE (1996) 278–292Google Scholar
  16. Ka.
    Kahn, G.: The semantics of a simple language for parallel programming, IFIP 74Google Scholar
  17. KT.
    Kobrinsky, N.., Trakhtenbrot, B.A.: Introduction to the Theory of Finite Automata (Russian edition, 1962), Transl. North Holland, 1965Google Scholar
  18. MP1.
    Maler, O., Pnueli, A.: Timing analysis of asynchronous circuits using timed automata. Proceedings CHARME’95, LNCS 987, pp. 189–205Google Scholar
  19. MP2.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, Springer Verlag, 1992Google Scholar
  20. MP3.
    Manna, Z., Pnueli, A.: Models for reactivity. Acta Informatica 30 (1993) 609–678.zbMATHCrossRefMathSciNetGoogle Scholar
  21. Ma.
    Mazurkiewicz, A.: Semantics of concurrent systems: A modular fixed point trace approach. In “Advances in Petri Nets”, LNCS 188, 1984Google Scholar
  22. Mi.
    Milner, R.: Communication and Concurrency, Prentice Hall, 1989Google Scholar
  23. OD.
    Olderog, E.R., Dierks, H.: Decomposing real-time specifications. Intern. Symp. COMPOS’97. LNCS 1536, pp. 465–489Google Scholar
  24. P.
    Pardo, D.: Timed Automata: Transducers and Circuits, M.Sc. Thesis, Tel-Aviv Univ., 1997Google Scholar
  25. PRT.
    Pardo, D., Rabinovich, A., Trakhtenbrot, B.A.: On synchronous circuits over continuous time, Technical Report, Tel Aviv University, 1997Google Scholar
  26. R.
    Rabinovich, A.: Finite automata over continuous time, Technical Report, Tel Aviv University, 1996Google Scholar
  27. RT.
    Rabinovich, A., Trakhtenbrot, B.: From finite automata toward hybrid systems. Proceedings FCT’97, LNCSGoogle Scholar
  28. S.
    Scott, D.: Some definitional suggestions for automata theory. J. of Computer and System Science (1967) 187–212Google Scholar
  29. S1.
    Sontag, E.: Mathematical Control Theory: Deterministic Finite Dimensional Systems, Springer, N.Y., 1990zbMATHGoogle Scholar
  30. S2.
    Sontag, E.: Interconnected Automata and Linear Systems. LNCS, No. 1066 (1996) pp. 436–448Google Scholar
  31. T1.
    Trakhtenbrot, B.A.: Lecture notes on a course on verification of software and hardware systems, Tel Aviv University, Fall 1994Google Scholar
  32. T2.
    Trakhtenbrot, B.A.: Automata and hybrid systems. Lecture Notes on a course at Uppsala University, Fall 1997. See also updating Appendix 1, 1998, Tel Aviv UniversityGoogle Scholar
  33. T3.
    Trakhtenbrot, B.A.: Compositional proofs for networks of processes. Fundamenta Informaticae 20(No. 1,2,3) (1994) 231–275zbMATHMathSciNetGoogle Scholar
  34. T4.
    Trakhtenbrot, B.A.: Origins and metamorphose of the trinity: Logics, nets, automata, Proceedings, LICS’95Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Boris A. Trakhtenbrot
    • 1
  1. 1.Department of Computer Science School of Mathematical SciencesTel Aviv UniversityTel AvivIsrael

Personalised recommendations