Path checking, the special case of the model checking problem where the model under consideration is a single path, plays an important role in monitoring, testing, and verification. We prove that for linear-time temporal logic (LTL), path checking can be efficiently parallelized. In addition to the core logic, we consider the extensions of LTL with bounded-future (BLTL) and past-time (LTL+Past) operators. Even though both extensions improve the succinctness of the logic exponentially, path checking remains efficiently parallelizable: Our algorithm for LTL, LTL+Past, and BLTL+Past is in AC^1(logDCFL) \subseteq NC.
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.
Wir prasentieren effiziente parallele Algorithmen zum Uberprufen der Erfulltheit von temporal logischen Formeln auf Pfaden und Baumen. Wir zeigen, dass fur die Logik LTL das Uberprufen von Ausfuhrungspfaden in der Komplexitatsklasse AC1(logDCFL) liegt. Fur die Logik CTL ist das Uberprufen von Baumen in AC2(logDCFL). Fur Erweiterungen von LTL mit Vergangenheit und beschrankten zeitlichen Modalitaten beweisen wir, dass Pfade ebenfalls in AC1(logDCFL) uberpruft werden konnen, obwohl die Logik exponentiell kompakter ist als einfaches LTL. Unsere Resultate bielden eine Grundlage fur effiziente Algorithmen fur verschiedene Anwendungen in den Bereichen der Systemuberwachung, des Testens und der Verfikation sowie fur die Anfragebearbeitung fur Baumdatenstrukturen, wie zum Beispiel XML Dokumente. Die prasentierten Algorithmen zum Uberprufen von Pfaden und Baumen basieren auf effizient parallelen Strategien zur Evaluierung von monotonen Boolschen Schaltkreisen. Wir reduzieren die Evaluierung von Produkt-Schaltkreisen auf das Problem der Evaluierung von monoton planaren Boolschen Schaltkreisen, bei denen sich alle Eingaben auf dem auseren Rand befinden. Fur monotone Boolsche Schaltkreise, die das Produkt von einem Baum und einem Pfad sind, geben wir eine AC1-Reduktion an. Fur monotone Boolsche Schaltkreise, die das Produkt von zwei Baumen sind, geben wir eine AC2-Reduktion an. Wir entwickeln eine Klassifizierung von Kripkestrukturen im Hinblick auf die Komplexitat des Erfulltheitsproblems fur LTL: Kripkestrukturen, fur die das Problem PSPACE-vollstandig ist, Kripkestrukturen, fur die das Problem coNP- vollstandig ist, und Kripkestrukturen, fur die das Problem in NC liegt.
'%3e%3cpath fill='%23012169' d='M0 0v30h60V0z'/%3e%3cpath stroke='%23fff' stroke-width='6' d='m0 0 60 30m0-30L0 30'/%3e%3cpath stroke='%23C8102E' stroke-width='4' d='m0 0 60 30m0-30L0 30' clip-path='url(%23b)'/%3e%3cpath stroke='%23fff' stroke-width='10' d='M30 0v30M0 15h60'/%3e%3cpath stroke='%23C8102E' stroke-width='6' d='M30 0v30M0 15h60'/%3e%3c/g%3e%3c/svg%3e)
