Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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)
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)
Cerny, E., Berkane, B., Girodias, P., Khordoc, K.: Hierarchical Annotated Action Diagrams. Kluwer Academic Publishers, Dordrecht (1998)
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)
Fisler, K.: Timing diagrams: Formalization and algorithmic verification. Journal of Logic, Language, and Information 8, 323–361 (1999)
Fisler, K.: On tableau constructions for timing diagrams. In: NASA Langley Formal Methods Workshop (2000)
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)
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)
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)
Laroussinie, F., Schnoebelen, P.: A hierarchy of temporal logics with past. In: Proc. 11th Symp. on Theoretical Aspects of Computer Science, Caen (February 1994)
Moszkowski, B.: A temporal logic for multi-level reasoning about hardware. IEEE Computer, 10–19 (February 1985)
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)
Sistla, A.: Theoretical issues in the design of distributed and concurrent systems. PhD thesis, Harvard University, Cambridge, MA (1983)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chockler, H., Fisler, K. (2005). Temporal Modalities for Concisely Capturing Timing Diagrams. In: Borrione, D., Paul, W. (eds) Correct Hardware Design and Verification Methods. CHARME 2005. Lecture Notes in Computer Science, vol 3725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11560548_15
Download citation
DOI: https://doi.org/10.1007/11560548_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29105-3
Online ISBN: 978-3-540-32030-2
eBook Packages: Computer ScienceComputer Science (R0)