Temporal Modalities for Concisely Capturing Timing Diagrams

Hana Chockler, Kathi Fisler

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

3 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationProceedings of Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME
PublisherSpringer
Pages176-190
Number of pages15
Publication statusPublished - 3 Oct 2005

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume3725

Fingerprint

Dive into the research topics of 'Temporal Modalities for Concisely Capturing Timing Diagrams'. Together they form a unique fingerprint.

Cite this