BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-95-1551
       ENTRY:: July 10, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Two Methods for Checking Formulas of Temporal Logic
        TYPE:: Thesis
        TYPE:: Technical Report
      AUTHOR:: McGuire, Hugh W.
        DATE:: June 1995
       PAGES:: 152
    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
	       past or are metric. Then, whereas classical proofs of
               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.
       NOTES:: [Adminitrivia V1/Prg/19950710]
         END:: STAN//CS-TR-95-1551