An Improved On-The-Fly Tableau Construction for a Real-Time Temporal Logic

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

• Type: Conference
• Year: 2003
• Where: CAV
• Authors: Marc Geilen
• Keywords: CAV 2003, Hardware, Tableau Construction, Temporal Logic, Temporal Logic Formula