R. de Haan, S. Szeider:

"Parameterized Complexity Results for Symbolic Model Checking of Temporal Logics";

Talk: 15th International Conference on Principles of Knowledge Representation and Reasoning (KR 2016), Kapstadt, Südafrika; 2016-04-25 - 2016-04-29; in: "Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning - KR 2016", (2016), ISBN: 978-1-57735-755-1; 453 - 462.

Reasoning about temporal knowledge is a fundamental task

in the area of artificial intelligence and knowledge representation.

A key problem in this area is model checking, and

indispensable for the state-of-the-art in solving this problem in

large-scale settings is the technique of bounded model checking.

We investigate the theoretical possibilities of this technique

using parameterized complexity theory. In particular, we

provide a complete parameterized complexity classification

for the model checking problem for symbolically represented

Kripke structures for various fragments of the temporal logics

LTL, CTL and CTL . We argue that a known result from the

literature for a restricted fragment of LTL can be seen as an

fpt-reduction to SAT, and show that such reductions are not

possible for any of the other fragments of the temporal logics

that we consider. As a by-product of our investigation, we

develop a novel parameterized complexity class that can be

seen as a parameterized variant of the Polynomial Hierarchy.

http://publik.tuwien.ac.at/files/publik_256381.pdf

Created from the Publication Database of the Vienna University of Technology.