TY - GEN

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

AU - Geilen, M.C.W.

AU - Dams, D.R.

PY - 2000

Y1 - 2000

N2 - 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.

AB - 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.

U2 - 10.1007/3-540-45352-0_23

DO - 10.1007/3-540-45352-0_23

M3 - Conference contribution

SN - 978-3-540-41055-3

T3 - Lecture Notes in Computer Science

SP - 276

EP - 290

BT - Formal techniques in real-time and fault-tolerant systems : 6th international symposium, Pune, India, September 20 - 22, 2000 ; proceedings / FTRTFT 2000

A2 - Joseph, M.

PB - Springer

CY - Berlin

T2 - conference; FTRTFT2000, Pune, India; 2000-09-20; 2000-09-22

Y2 - 20 September 2000 through 22 September 2000

ER -