All reports by Author Michael Bauland:

__
TR08-028
| 5th December 2007
__

Michael Bauland, Martin Mundhenk, Thomas Schneider, Henning Schnoor, Ilka Schnoor, Heribert Vollmer#### The Tractability of Model-Checking for LTL: The Good, the Bad, and the Ugly Fragments

__
TR07-023
| 26th February 2007
__

Heribert Vollmer, Michael Bauland, Elmar Böhler, Nadia Creignou, Steffen Reith, Henning Schnoor#### The Complexity of Problems for Quantified Constraints

__
TR06-153
| 19th October 2006
__

Michael Bauland, Thomas Schneider, Henning Schnoor, Ilka Schnoor, Heribert Vollmer#### The Complexity of Generalized Satisfiability for Linear Temporal Logic

Revisions: 1

__
TR05-024
| 8th February 2005
__

Michael Bauland, Elmar Böhler, Nadia Creignou, Steffen Reith, Henning Schnoor, Heribert Vollmer#### Quantified Constraints: The Complexity of Decision and Counting for Bounded Alternation

__
TR04-100
| 23rd November 2004
__

Eric Allender, Michael Bauland, Neil Immerman, Henning Schnoor, Heribert Vollmer#### The Complexity of Satisfiability Problems: Refining Schaefer's Theorem

Revisions: 1

Michael Bauland, Martin Mundhenk, Thomas Schneider, Henning Schnoor, Ilka Schnoor, Heribert Vollmer

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.

...
more >>>

Heribert Vollmer, Michael Bauland, Elmar Böhler, Nadia Creignou, Steffen Reith, Henning Schnoor

In this paper we will look at restricted versions of the evaluation problem, the model checking problem, the equivalence problem, and the counting problem for quantified propositional formulas, both with and without bound on the number of quantifier alternations. The restrictions are such that we consider formulas in conjunctive normal-form ... more >>>

Michael Bauland, Thomas Schneider, Henning Schnoor, Ilka Schnoor, Heribert Vollmer

In a seminal paper from 1985, Sistla and Clarke showed

that satisfiability 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 ...
more >>>

Michael Bauland, Elmar Böhler, Nadia Creignou, Steffen Reith, Henning Schnoor, Heribert Vollmer

We consider constraint satisfaction problems parameterized by the set of allowed constraint predicates. We examine the complexity of quantified constraint satisfaction problems with a bounded number of quantifier alternations and the complexity of the associated counting problems. We obtain classification results that completely solve the Boolean case, and we show ... more >>>

Eric Allender, Michael Bauland, Neil Immerman, Henning Schnoor, Heribert Vollmer

Schaefer proved in 1978 that the Boolean constraint satisfaction problem for a given constraint language is either in P or is NP-complete, and identified all tractable cases. Schaefer's dichotomy theorem actually shows that there are at most two constraint satisfaction problems, up to polynomial-time isomorphism (and these isomorphism types are ... more >>>