@inproceedings{fc00892f354d454299a8b5fde24a97c6,
title = "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 model-checking. 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.",
author = "M.C.W. Geilen",
year = "2003",
doi = "10.1007/978-3-540-45069-6\_37",
language = "English",
isbn = "978-3-540-40524-5",
series = "Lecture notes in computer science",
publisher = "Springer",
pages = "394--406",
editor = "\{Hunter, Jr.\}, W.A. and F. Somenzi",
booktitle = "Computer Aided Verification CAV 2003",
address = "Germany",
note = "conference; CAV 2003, Boulder, CO, USA; 2003-07-08; 2003-07-12 ; Conference date: 08-07-2003 Through 12-07-2003",
}