Report Number: CS-TR-95-1551
Institution: Stanford University, Department of Computer Science
Title: Two Methods for Checking Formulas of Temporal Logic
Author: McGuire, Hugh W.
Date: June 1995
Abstract: This dissertation presents two methods for determining satisfiability or validity of formulas of Discrete Metric Annotated Linear Temporal Logic. This logic is convenient for representing and verifying properties of reactive and concurrent systems, including software and electronic circuits. The first method presented here is an algorithm for automatically deciding whether any given propositional temporal formula is satisfiable. This new algorithm efficiently extends the classical `semantic tableau'-algorithm to formulas with temporal operators which refer to the correctness for such algorithms are existential, the proof here is constructive; it shows that for any given formula being checked, any model of the formula is embedded in the tableau. The second method presented in this dissertation is a deduction-calculus for determining the validity of predicate temporal formulas. This new deduction-calculus employs a refined, conservative version of classical approaches involving translation from temporal forms to first-order expressions with time reified. Here, quantifications are elided, and addition is used instead of classical complicated combinations of comparisons. This scheme facilitates integration of powerful techniques such as associative-commutative unification and a Presburger decision-algorithm.
http://i.stanford.edu/pub/cstr/reports/cs/tr/95/1551/CS-TR-95-1551.pdf