Temporal Modalities for Concisely Capturing Timing Diagrams

  • Hana Chockler
  • Kathi Fisler
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


Timing diagrams are useful for capturing temporal specifications in which all mentioned events are required to occur. We first show that translating timing diagrams with both partial orders on events and don’t-care regions to LTL potentially yields exponentially larger formulas containing several non-localized terms corresponding to the same event. This raises a more fundamental question: which modalities allow a textual temporal logic to capture such diagrams using a single term for each event? We define the shapes of partial orders that are captured concisely by a hierarchy of textual linear temporal logics containing future and past time operators, as well Laroussinie et al’s forgettable past operator and our own unforeseen future operator. Our results give insight into the temporal abstractions that underlie timing diagrams and suggest that the abstractions in LTL are significantly weaker than those captured by timing diagrams.


Partial Order Temporal Logic Schedule Tree Search Operator Linear Temporal Logic 
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.


  1. 1.
    Amla, N., Emerson, E.A., Namjoshi, K.S.: Efficient decompositional model checking for regular timing diagrams. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 67–81. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. 2.
    Amla, N., Emerson, E.A., Namjoshi, K.S., Trefler, R.J.: Visual specifications for modular reasoning about asynchronous systems. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 226–242. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  3. 3.
    Cerny, E., Berkane, B., Girodias, P., Khordoc, K.: Hierarchical Annotated Action Diagrams. Kluwer Academic Publishers, Dordrecht (1998)zbMATHGoogle Scholar
  4. 4.
    Dillon, L., Kutty, G., Moser, L., Melliar-Smith, P.M., Ramakrishna, Y.S.: A graphical interval logic for specifying concurrent systems. ACM Transactions on Software Engineering and Methodology 3(2), 131–165 (1994)CrossRefGoogle Scholar
  5. 5.
    Fisler, K.: Timing diagrams: Formalization and algorithmic verification. Journal of Logic, Language, and Information 8, 323–361 (1999)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Fisler, K.: On tableau constructions for timing diagrams. In: NASA Langley Formal Methods Workshop (2000)Google Scholar
  7. 7.
    Gabbay, D.: The declarative past and imperative future. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 407–448. Springer, Heidelberg (1989)Google Scholar
  8. 8.
    Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proc. 7th ACM Symp. on Principles of Programming Languages, January 1980, pp. 163–173 (1980)Google Scholar
  9. 9.
    Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: Proc. 17th IEEE Symp. Logic in Computer Science (LICS 2002), pp. 383–392 (2002)Google Scholar
  10. 10.
    Laroussinie, F., Schnoebelen, P.: A hierarchy of temporal logics with past. In: Proc. 11th Symp. on Theoretical Aspects of Computer Science, Caen (February 1994)Google Scholar
  11. 11.
    Moszkowski, B.: A temporal logic for multi-level reasoning about hardware. IEEE Computer, 10–19 (February 1985)Google Scholar
  12. 12.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th ACM Symp. on Principles of Programming Languages, Austin, January 1989, pp. 179–190 (1989)Google Scholar
  13. 13.
    Sistla, A.: Theoretical issues in the design of distributed and concurrent systems. PhD thesis, Harvard University, Cambridge, MA (1983)Google Scholar
  14. 14.
    Sistla, A., Vardi, M., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science 49, 217–237 (1987)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Hana Chockler
    • 1
    • 2
  • Kathi Fisler
    • 1
  1. 1.Department of Computer ScienceWPIWorcesterUSA
  2. 2.MIT CSAILCambridgeUSA

Personalised recommendations