[Zurück]

R. de Haan, S. Szeider:
"Parameterized Complexity Results for Symbolic Model Checking of Temporal Logics";
Vortrag: 15th International Conference on Principles of Knowledge Representation and Reasoning (KR 2016), Kapstadt, Südafrika; 25.04.2016 - 29.04.2016; in: "Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning - KR 2016", (2016), ISBN: 978-1-57735-755-1; S. 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