Model Checking Finite Paths and Trees
Lars Kuhtz
This thesis presents efficient parallel algorithms for checking temporal logic formulas over finite paths and trees. We show that LTL path checking is in AC1 (logDCFL) and CTL tree checking is in AC2 (logDCFL). For LTL with past-time and bounded modalities, which is an exponentially more succinct logic, we show that the path checking problem remains in AC1 (logDCFL). Our results provide a foundation for efficient algorithms of various applications in monitoring, testing, and verification as well as for query processing for tree-datastructures, e.g. XML documents.
The presented path and tree checking algorithms are based on efficient parallel evaluation strategies for monotone Boolean circuits. Let a product circuit be a circuit with a graph that is a normal graph product. We reduce the evaluation of certain product circuits to the problem of evaluating one-input-face monotone planar Boolean circuits: for a monotone Boolean circuit that is a product of a tree and a path, we provide an AC1- reduction; for a monotone Boolean circuit that is a product of two trees, we provide an AC2-reduction.
We develop a classification of Kripke structures with respect to the complexity of LTL model checking: Kripke structures for which the problem is PSPACE-complete, Kripke structures for which the problem is coNP-complete, and Kripke structures for which the problem is in NC.
PhD Thesis.