An Efficient Tableau for Linear Time Temporal Logic

摘要

Practical reasoning aids for dense-time temporal logics are not at all common despite a range of potential applications from verification of concurrent systems to AI. There have been recent suggestions that the temporal mosaic idea can provide implementable tableau-style decision procedures for various linear time temporal logics beyond the standard discrete natural numbers model of time. In this paper we extend the established idea of mosaic tableaux by introducing a novel abstract methodology of partiality which allows a partial mosaic to represent many mosaics. This can significantly reduce the running time of building a tableau. We present partial mosaics, partial mosaic-based tableau and algorithms for building the tableau.