The model checking problem for intuitionistic propositional logic with one variable is AC1-complete

Intuitionistic implication makes model checking hard

We investigate the complexity of the model checking problem for intuitionistic and modal propositional logics over transitive Kripke models. More specific, we consider intuitionistic logic IPC, basic propositional logic BPL, formal propositional logic FPL, and Jankov's logic KC. We show that the model checking problem is P-complete for the implicational fragments of all these intuitionistic logics. For BPL and FPL we reach P-hardness even on the implicational fragment with only one variable. The same hardness results are obtained for the strictly implicational fragments of their modal companio…

The Tractability of Model-Checking for LTL: The Good, the Bad, and the Ugly Fragments

In a seminal paper from 1985, Sistla and Clarke showed that the model-checking problem for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the set of temporal operators used. If, in contrast, the set of propositional operators is restricted, the complexity may decrease. This paper systematically studies the model-checking problem for LTL formulae over restricted sets of propositional and temporal operators. For almost all combinations of temporal and propositional operators, we determine whether the model-checking problem is tractable (in P) or intractable (N…

Parametrised Complexity of Model Checking and Satisfiability in Propositional Dependence Logic

In this paper, we initiate a systematic study of the parametrised complexity in the field of Dependence Logics which finds its origin in the Dependence Logic of Väänänen from 2007. We study a propositional variant of this logic (PDL) and investigate a variety of parametrisations with respect to the central decision problems. The model checking problem (MC) of PDL is NP-complete. The subject of this research is to identify a list of parametrisations (formula-size, treewidth, treedepth, team-size, number of variables) under which MC becomes fixed-parameter tractable. Furthermore, we show that th…

Complexity of Model Checking for Modal Dependence Logic

Modal dependence logic (MDL) was introduced recently by Väänänen. It enhances the basic modal language by an operator =(). For propositional variables p_1,...,p_n the atomic formula =(p_1,...,p_(n-1),p_n) intuitively states that the value of p_n is determined solely by those of p_1,...,p_(n-1). We show that model checking for MDL formulae over Kripke structures is NP-complete and further consider fragments of MDL obtained by restricting the set of allowed propositional and modal connectives. It turns out that several fragments, e.g., the one without modalities or the one without propositional …

命题包含与独立性逻辑的参数化复杂性

Parameterised Complexity of Propositional Inclusion and Independence Logic

本文系统研究命题包含逻辑与独立性逻辑中模型检查和可满足性的参数化复杂性，表明多数参数化下问题处于 FPT 或为 paraNP 完全。

Complexity of Propositional Logics in Team Semantics

We classify the computational complexity of the satisfiability, validity and model-checking problems for propositional independence, inclusion, and team logic. Our main result shows that the satisfiability and validity problems for propositional team logic are complete for alternating exponential-time with polynomially many alternations.