, Volume 27, Issue 2, pp 181–208 | Cite as

Product interval automata

  • Deepak D’souza
  • P. S. Thiagarajan


We identify a subclass of timed automata called product interval automata and develop its theory. These automata consist of a network of timed agents with the key restriction being that there is just one clock for each agent and the way the clocks are read and reset is determined by the distribution of shared actions across the agents. We show that the resulting automata admit a clean theory in both logical and language theoretic terms. We also show that product interval automata are expressive enough to model the timed behaviour of asynchronous digital circuits.


Timed automata distributed systems logic 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Alur R, Dill D L 1994 A theory of timed automata.Theor. Comput. Sci. 126: 183–235MATHCrossRefMathSciNetGoogle Scholar
  2. Alur R, Henzinger T A 1992 Logics and models of real time: A survey. InReal-time: Theory in practice (eds.) J W de Bakkeret al, LNCS 600 (Berlin: Springer-Verlag) pp 74–106CrossRefGoogle Scholar
  3. Alur R, Fix L, Henzinger T A 1994 Event-clock automata: a determinizable class of timed automata.Proc. 6th Int. Conf. on Computer-aided Verification, LNCS 818 (Berlin: Springer-Verlag) pp 1–13Google Scholar
  4. Bengtsson J, Jonsson B, Lilius J, Yi W 1998 Partial order reductions for timed systems.Proc. CONCUR ’98, LNCS 1466 (Berlin: Springer-Verlag)Google Scholar
  5. Brzozowski J A, Seger C-J H 1994Asynchronous circuits (Berlin: Springer-Verlag)Google Scholar
  6. Büchi J R 1960 Weak second-order arithmetic and finite automata.Z. Math. Logik Grundlagen Math. 6: 66–92MATHCrossRefMathSciNetGoogle Scholar
  7. Diekert V, Rozenberg G 1995The book of traces (Singapore: World Scientific)Google Scholar
  8. D’Souza D 2000a Alogical study of distributed timed automata. PhD thesis, Chennai Mathematical Institute (available at Scholar
  9. D’Souza D 2000b A logical characterisation of event recording automata.Proc. 6th Intl. Symp. on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT) LNCS 1926 (Berlin: Springer-Verlag)Google Scholar
  10. D’Souza D, Thiagarajan P S 1998 Distributed interval automata. Internal Report TCS-98-3, Chennai Mathematical Institute, ChennaiGoogle Scholar
  11. D’Souza D, Thiagarajan P S 1999 Product interval automata: A subclass of timed automata.Proc. 19th Foundations of Software Technology and Theoretical Computer Science (FSTTCS), LNCS 1732 (Berlin: Springer-Verlag)Google Scholar
  12. Gabbay D, Pnueli A, Shelah S, Stavi J 1980 The temporal analysis of fairness.Seventh ACM Symposium on Principles of Programming Languages, pp 163–173Google Scholar
  13. Gastin P, Petit A 1992 Asynchronous cellular automaton for infinite traces.Proceedings of ICALP ’92, LNCS 623 (Berlin: Springer-Verlag) pp 583–594Google Scholar
  14. Henriksen J G, Thiagarajan P S 1997 A product version of dynamic linear time temporal logic.Proc. CONCUR ’97, LNCS 1243 (Berlin: Springer-Verlag) pp 45–58Google Scholar
  15. Henzinger T A 1998 It’s about time: Real-time logics reviewed.Proc. CONCUR ’98, LNCS 1466 (Berlin: Springer-Verlag) pp 366–372Google Scholar
  16. Henzinger T A, Kopke P W, Puri A, Varaiya P 1995 What’s decidable about hybrid automata?Proc. 27th Annual Symposium on Theory of Computing (ACM Press) pp 373–382Google Scholar
  17. Henzinger T A, Raskin J-F, Schobbens P-Y 1998 The regular real-time languages.Proc. 25th Int. Colloquium on Automata, Languages, and Programming 1998, LNCS 1443 (Berlin: Springer-Verlag) pp 580–591Google Scholar
  18. Kamp H 1968Tense logic and the theory of linear order. Ph D thesis, University of CaliforniaGoogle Scholar
  19. Maler O, Pnueli A 1995 Timing analysis of asynchronous circuits using timed automata. InProc. CHARME ’95, LNCS 987 (Berlin: Springer-Verlag) pp 189–205Google Scholar
  20. Merlin P, Faber D J 1976 Recoverability of communication protocols.IEEE Trans. Commun. 24: 431–446Google Scholar
  21. Minea M 1999 Partial order reduction for model checking of timed automata. InProc. CONCUR ’99, LNCS 1664 (Berlin: Springer Verlag)Google Scholar
  22. Pnueli A 1977 The temporal logic of programs.Proc. 18th IEEE Symp. on Foundations of Computer Science (IEEE Comput. Soc. Press) pp 46–57Google Scholar
  23. Raskin J-F, Schobbens P-Y 1997 State-clock logic: A decidable real-time logic.Proc. HART ’97: Hybrid and Real-Time Systems, LNCS 1201 (Berlin: Springer-Verlag) pp 33–47CrossRefGoogle Scholar
  24. Sistla A P, Clarke E M 1985 The complexity of propositional linear temporal logic.J. Assoc. Comput. Mach. 32: 733–749MATHMathSciNetGoogle Scholar
  25. Thiagarajan P S 1995 A trace consistent subset of PTL.Proc. CONCUR ’95, LNCS 962 (Berlin: Springer-Verlag) pp 438–452Google Scholar
  26. Thomas W 1990 Automata on infinite objects. InHandbook of theoretical computer science (ed.) J V Leeuwen (Elsevier) vol. B, pp 133–191Google Scholar
  27. Vardi M Y, Wolper P, Sistla A P 1983 Reasoning about infinite computation paths.Proc. 24th IEEE Symposium on Foundations of Computer Science (IEEE Comput. Soc. Press) pp 185–194Google Scholar
  28. Wilke Th 1994 Specifying timed state sequences in powerful decidable logics and timed automata. InFormal techniques in real-time and fault-tolerant systems, LNCS 863 (Berlin: Springer-Verlag) pp 694–715Google Scholar
  29. Yi W, Jonsson B 1994 Decidability of timed language-inclusion for networks of real-time communicating sequential processes.Proc. Foundations of Software Technology and Theoretical Computer Science 94, LNCS 880 (Berlin: Springer-Verlag)Google Scholar
  30. Zielonka W 1987 Notes on finite asynchronous automata.RAIRO — Inf. Theor. Appl. 21: 99–135MathSciNetGoogle Scholar

Copyright information

© Indian Academy of Sciences 2002

Authors and Affiliations

  • Deepak D’souza
    • 1
  • P. S. Thiagarajan
    • 1
  1. 1.Chennai Mathematical InstituteChennaiIndia

Personalised recommendations