Talks and Poster Presentations (with Proceedings-Entry):
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),
- 2016-04-29; in: "Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning - KR 2016",
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.
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.