On the Complexity of Temporal-Logic Path Checking

DOI10.1007/978-3-662-43951-7_8MaRDI QIDQ5167829zbMATH OpenOpenAlexFDO

Authors Daniel Bundala, Joël Ouaknine

Publication date 1 July 2014

Published in Automata, Languages, and Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1312.7603

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Given a formula in a temporal logic such as LTL or MTL, a fundamental problem is the complexity of evaluating the formula on a given finite word. For LTL, the complexity of this task was recently shown to be in NC. In this paper, we present an NC algorithm for MTL, a quantitative (or metric) extension of LTL, and give an NCC algorithm for UTL, the unary fragment of LTL. At the time of writing, MTL is the most expressive logic with an NC path-checking algorithm, and UTL is the most expressive fragment of LTL with a more efficient path-checking algorithm than for full LTL (subject to standard complexity-theoretic assumptions). We then establish a connection between LTL path checking and planar circuits, which we exploit to show that any further progress in determining the precise complexity of LTL path checking would immediately entail more efficient evaluation algorithms than are known for a certain class of planar circuits. The connection further implies that the complexity of LTL path checking depends on the Boolean connectives allowed: adding Boolean exclusive or yields a temporal logic with P-complete path-checking problem.

Recommendations

• scientific article; zbMATH DE number 2196601
• Efficient parallel path checking for linear-time temporal logic with past and bounds
• Complexity analysis of a unifying algorithm for model checking interval temporal logic
• Complexity analysis of a unifying algorithm for model checking interval temporal logic
• scientific article; zbMATH DE number 177267
• scientific article; zbMATH DE number 177521
• Parametrised complexity of satisfiability in temporal logic
• A model checker for linear time temporal logic
• Model-checking timed temporal logics

Cited in

(5)

• A survey of challenges for runtime verification from advanced application domains (beyond software)
• Weak Kripke structures and LTL
• Efficient parallel path checking for linear-time temporal logic with past and bounds
• scientific article; zbMATH DE number 7056237 (Why is no real title available?)
• scientific article; zbMATH DE number 5201490 (Why is no real title available?)

This page was built for publication: On the Complexity of Temporal-Logic Path Checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5167829)