An improved on-the-fly tableau construction for a real-time temporal logic

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

12 Citations (Scopus)

Abstract

Temporal logic is popular for specifying correctness properties of reactive systems. Real-time temporal logics add the ability to express quantitative timing aspects. Tableau constructions are algorithms that translate a temporal logic formula into a finite-state automaton that accepts precisely all the models of the formula. On-the-fly versions of tableau-constructions enable their practical application for model-checking. In a previous paper we presented an on-the-fly tableaux construction for a fragment of Metric Interval Temporal Logic in dense time. The interpretation of the logic was constrained to a special kind of timed state sequences, with intervals that are always left-closed and right-open. In this paper we present a non-trivial extension to this tableau construction for the same logic fragment, that lifts this constraint.
Original languageEnglish
Title of host publicationComputer Aided Verification CAV 2003
EditorsW.A. Hunter, Jr., F. Somenzi
Place of PublicationBerlin
PublisherSpringer
Pages394-406
ISBN (Print)978-3-540-40524-5
DOIs
Publication statusPublished - 2003
Eventconference; CAV 2003, Boulder, CO, USA; 2003-07-08; 2003-07-12 -
Duration: 8 Jul 200312 Jul 2003

Publication series

NameLecture notes in computer science
Volume2725

Conference

Conferenceconference; CAV 2003, Boulder, CO, USA; 2003-07-08; 2003-07-12
Period8/07/0312/07/03
OtherCAV 2003, Boulder, CO, USA

Fingerprint

Dive into the research topics of 'An improved on-the-fly tableau construction for a real-time temporal logic'. Together they form a unique fingerprint.

Cite this