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.