TY  - THES
T1  - Model checking finite paths and trees
A1  - Kuhtz,Lars
Y1  - 2011/03/31
N2  - 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 pastime 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. We reduce the evaluation of 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.
KW  -  Algorithmus
KW  - Pfad <Mathematik>
KW  - Baum <Mathematik>
KW  - Logische Schaltung
CY  - Saarbrücken
PB  - Universitäts- und Landesbibliothek
AD  - Postfach 151141, 66041 Saarbrücken
UR  - http://scidok.sulb.uni-saarland.de/volltexte/2011/3555
ER  -