Sciweavers

Share
CAV
2003
Springer

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

9 years 3 months ago
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.
Marc Geilen
Added 23 Aug 2010
Updated 23 Aug 2010
Type Conference
Year 2003
Where CAV
Authors Marc Geilen
Comments (0)
books