文章基本信息

标题：Efficient Parallel Path Checking for Linear-Time Temporal Logic With Past and Bounds
本地全文：下载
作者：Lars Kuhtz ; Bernd Finkbeiner
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2012
卷号：8
期号：4
页码：1
DOI：10.2168/LMCS-8(4:10)2012
出版社：Technical University of Braunschweig
摘要：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.
其他关键词：linear-time temporal logic (LTL), linear-time temporal logic with past, bounded temporal operators, model checking, path checking, parallel complexity.