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

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.