Using temporal logic to analyse temporal logic: A hierarchical approach based on intervals
This work further develops and perfects the hierarchical interval-oriented methods for analysing conventional propositional linear-time temporal logic (PTL) contained in earlier Outputs 1 and 3. It includes numerous simplified examples, algorithms and proofs. In addition, extensive material on decision procedures for PTL with infinite time has been added, including natural reductions to a normal form in PTL closely resembling Buechi automata. Consequently, some existing practical algorithms for analysing Buechi automata should be adaptable. Following invitations, we presented the work as a BCS-FACS seminar in London and also as a Belgian national seminar on verification in Brussels.
Citation : Moszkowski, B.C. (2007) Using temporal logic to analyse temporal logic: A hierarchical approach based on intervals. Journal of Logic and Computation, 17 (2), pp. 333-409
ISSN : 0955-792X
Research Group : Software Technology Research Laboratory (STRL)