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

M.C.W. Geilen, D.R. Dams

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

11 Citations (Scopus)
3 Downloads (Pure)

Abstract

Temporal logic is a useful tool for specifying correctness properties of reactive programs. In particular, real-time temporal logics have been developed for expressing quantitative timing aspects of systems. A tableau construction is an algorithm that translates a temporal logic formula into a finite-state automaton that accepts precisely all the models of the formula. It is a key ingredient to checking satisfiability of a formula as well as to the automata-theoretic approach to model checking. An improvement to the efficiency of tableau constructions has been the development of on-the-fly versions. In the real-time domain, tableau constructions have been developed for various logics and their complexities have been studied. However, there has been considerably less work aimed at improving and implementing them. In this paper, we present an on-the-fly tableau construction for a linear temporal logic with dense time, a fragment of Metric Interval Temporal Logic that is decidable in PSPACE. We have implemented a prototype of the algorithm and give experimental results. Being on-the-fly, our algorithm is expected to use less memory and to give smaller tableaux in many cases in practice than existing constructions.
Original languageEnglish
Title of host publicationFormal techniques in real-time and fault-tolerant systems : 6th international symposium, Pune, India, September 20 - 22, 2000 ; proceedings / FTRTFT 2000
EditorsM. Joseph
Place of PublicationBerlin
PublisherSpringer
Pages276-290
ISBN (Print)978-3-540-41055-3
DOIs
Publication statusPublished - 2000
Eventconference; FTRTFT2000, Pune, India; 2000-09-20; 2000-09-22 -
Duration: 20 Sep 200022 Sep 2000

Publication series

NameLecture Notes in Computer Science
Volume1926
ISSN (Print)0302-9743

Conference

Conferenceconference; FTRTFT2000, Pune, India; 2000-09-20; 2000-09-22
Period20/09/0022/09/00
OtherFTRTFT2000, Pune, India

Fingerprint

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

Cite this