Two Methods for Checking Formulas of Temporal Logic

摘要

The dissertation presents two methods for determining satisfiability or validityof 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 and, if so, reporting a model of the formula. The classical algorithm for this task defines possible states as settings of the truth-values of particular formulas which are relevant to the given formula; possible states are constructed and then linked according to their associated formulas' constraints on temporally adjacent states, and then certain fulfillment-conditions are checked. The second method presented in this dissertation is a deduction-calculus for determining the validity of predicate temporal formulas. The new deduction-calculus presented employs a refined, conservative version of this translation from temporal forms to expressions with time reified. Quantifications are elided, and addition is used instead of classical complicated combinations of comparisons.