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 language | English |
---|
Title of host publication | Proceedings of Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME |
---|
Publisher | Springer |
---|
Pages | 176-190 |
---|
Number of pages | 15 |
---|
Publication status | Published - 3 Oct 2005 |
---|
Name | Lecture Notes in Computer Science |
---|
Publisher | Springer |
---|
Volume | 3725 |
---|