Fixpoint Representations of Characteristic Sets of Linear-Time Temporal Formulas

摘要

An algebraic-axiomatic method for computing existential and universal characteristic sets of linear-time temporal logic formulas on directed graphs is presented. The set of all nodes v of a given graph (model) such that all (respectively, some) infinite walks starting from v satisfy a formula is called the universal (respectively, existential) characteristic set of the formula. Computation of the characteristic set is reduced to finding the least or greatest fixpoint of a system of set equations. Representations of the characteristic set of the logic L obtained are model-independent, in the sense that the same representation holds for all graphs, and regardless of whether or not they are finite or infinite.