Timed Interfaces

  • Luca de Alfaro
  • Thomas A. Henzinger
  • Mariëlle Stoelinga
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2491)


We present a theory of timed interfaces, which is capable of specifying both the timing of the inputs a component expects from the environment, and the timing of the outputs it can produce. Two timed interfaces are compatible if there is a way to use them together such that their timing expectations are met. Our theory provides algorithms for checking the compatibility between two interfaces and for deriving the composite interface; the theory can thus be viewed as a type system for real-time interaction. Technically, a timed interface is encoded as a timed game between two players, representing the inputs and outputs of the component. The algorithms for compatibility checking and interface composition are thus derived from algorithms for solving timed games.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Abr96.
    S. Abramsky. Semantics of interaction. In Trees in Algebra and Programming, volume 1059 of Lect. Notes in Comp. Sci., page 1. Springer, 1996.Google Scholar
  2. AD94.
    R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.zbMATHCrossRefMathSciNetGoogle Scholar
  3. AH97.
    R. Alur and T.A. Henzinger. Modularity for timed and hybrid systems. In Concurrency Theory, volume 1243 of Lect. Notes in Comp. Sci., pages 74–88. Springer, 1997.Google Scholar
  4. AMPS98.
    E. Asarin, O. Maler, A. Pnueli, and J. Sifakis. Controller synthesis for timed automata. In Proc. IFAC Symp. System Structure and Control, pages 469–474. Elsevier, 1998.Google Scholar
  5. CRR02.
    S. Chaki, S.K. Rajamani, and J. Rehof. Types as models: Model checking message-passing programs. In Proc. Symp. Principles of Programming Languages, pages 45–57. ACM, 2002.Google Scholar
  6. dAH01a.
    L. de Alfaro and T.A. Henzinger. Interface automata. In Proc. Symp. Foundations of Software Engineering, pages 109–120. ACM, 2001.Google Scholar
  7. dAH01b.
    L. de Alfaro and T.A. Henzinger. Interface theories for component-based design. In Embedded Software, volume 2211 of Lect. Notes in Comp. Sci., pages 148–165. Springer, 2001.Google Scholar
  8. dAHM01.
    L. de Alfaro, T.A. Henzinger, and R. Majumdar. Symbolic algorithms for infinite-state games. In Concurrency Theory, volume 2154 of Lect. Notes in Comp. Sci., pages 536–550. Springer, 2001.Google Scholar
  9. Dil88.
    D.L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT Press, 1988.Google Scholar
  10. EJ91.
    E.A. Emerson and C.S. Jutla. Tree automata, mu-calculus, and determinacy. In Proc. Symp. Foundations of Computer Science, pages 368–377. IEEE Computer Society, 1991.Google Scholar
  11. MMT91.
    M. Merritt, F. Modugno, and M. Tuttle. Time constrained automata. In Concurrency Theory, volume 527 of Lect. Notes in Comp. Sci., pages 408–423. Springer, 1991.Google Scholar
  12. MPS95.
    O. Maler, A. Pnueli, and J. Sifakis. On the synthesis of discrete controllers for timed systems. In Theoretical Aspects of Computer Science, volume 900 of Lect. Notes in Comp. Sci., pages 229–242. Springer, 1995.Google Scholar
  13. RGG96.
    E. Rudolph, P. Graubmann, and J. Gabowski. Tutorial on message sequence charts. Computer Networks and ISDN Systems-SDL and MSC, 28:1629–1641, 1996.CrossRefGoogle Scholar
  14. RR01.
    S.K. Rajamani and J. Rehof. A behavioral module system for the pi-calculus. In Static Analysis Symposium, volume 2126 of Lect. Notes in Comp. Sci., pages 375–394. Springer, 2001.Google Scholar
  15. SGSAL98.
    R. Segala, G. Gawlick, J. Søgaard-Andersen, and N. Lynch. Liveness in timed and untimed systems. Information and Computation, 141:119–171, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  16. Tho90.
    W. Thomas. Automata on infinite objects. In J. van Leeuwen, ed., Handbook of Theoretical Computer Science, volume B, pages 135–191. Elsevier, 1990.Google Scholar
  17. Yi90.
    Wang Yi. Real-time behaviour of asynchronous agents. In Concurrency Theory, volume 458 of Lect. Notes in Comp. Sci., pages 502–520. Springer, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Luca de Alfaro
    • 1
  • Thomas A. Henzinger
    • 2
  • Mariëlle Stoelinga
    • 1
  1. 1.Computer EngineeringUniversity of CaliforniaSanta Cruz
  2. 2.EECS, University of CaliforniaBerkeley

Personalised recommendations