Document

**Published in:** LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Monadic-second order logic (MSO-logic) is successfully applied in both language theory and algorithm design. In the former, properties definable by MSO-formulas are exactly the regular properties on many structures like, most prominently, strings. In the latter, solving a problem for structures of bounded tree width is routinely done by defining it in terms of an MSO-formula and applying general formula-evaluation procedures like Courcelle's. The present paper furthers the study of second-order logics with close connections to language theory and algorithm design beyond MSO-logic.
We introduce a logic that allows to expand a given structure with an existentially quantified tree decomposition of bounded width and test an MSO-definable property for the resulting expanded structure. It is proposed as a candidate for capturing the notion of "context-free graph properties" since it corresponds to the context-free languages on strings, has the same closure properties, and an alternative definition similar to the one of Chomsky and Schützenberger for context-free languages. Besides studying its language-theoretic aspects, we consider its expressive power as well as the algorithmics of its satisfiability and evaluation problems.

Michael Elberfeld. Context-Free Graph Properties via Definable Decompositions. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{elberfeld:LIPIcs.CSL.2016.17, author = {Elberfeld, Michael}, title = {{Context-Free Graph Properties via Definable Decompositions}}, booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)}, pages = {17:1--17:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-022-4}, ISSN = {1868-8969}, year = {2016}, volume = {62}, editor = {Talbot, Jean-Marc and Regnier, Laurent}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.17}, URN = {urn:nbn:de:0030-drops-65575}, doi = {10.4230/LIPIcs.CSL.2016.17}, annote = {Keywords: finite model theory, monadic second-order logic, tree decomposition, context-free languages, expressive power} }

Document

**Published in:** LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Graph canonization is the problem of computing a unique representative, a canon, from the isomorphism class of a given graph. This implies that two graphs are isomorphic exactly if their canons are equal. We show that graphs of bounded tree width can be canonized in deterministic logarithmic space (logspace). This implies that the isomorphism problem for graphs of bounded tree width can be decided in logspace. In the light of isomorphism for trees being hard for the complexity class logspace, this makes the ubiquitous classes of graphs of bounded tree width one of the few classes of graphs for which the complexity of the isomorphism problem has been exactly determined.

Michael Elberfeld and Pascal Schweitzer. Canonizing Graphs of Bounded Tree Width in Logspace. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 32:1-32:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{elberfeld_et_al:LIPIcs.STACS.2016.32, author = {Elberfeld, Michael and Schweitzer, Pascal}, title = {{Canonizing Graphs of Bounded Tree Width in Logspace}}, booktitle = {33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)}, pages = {32:1--32:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-001-9}, ISSN = {1868-8969}, year = {2016}, volume = {47}, editor = {Ollinger, Nicolas and Vollmer, Heribert}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.32}, URN = {urn:nbn:de:0030-drops-57336}, doi = {10.4230/LIPIcs.STACS.2016.32}, annote = {Keywords: algorithmic graph theory, computational complexity, graph isomorphism, logspace, tree width} }

Document

**Published in:** LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

We study the complexity of model checking formulas in first-order logic parameterized by the number of distinct variables in the formula. This problem, which is not known to be fixed-parameter tractable, resisted to be properly classified in the context of parameterized complexity. We show that it is complete for a newly-defined complexity class that we propose as an analog of the classical class PSPACE in parameterized complexity. We support this intuition by the following findings: First, the proposed class admits a definition in terms of alternating Turing machines in a similar way as PSPACE can be defined in terms of polynomial-time alternating machines. Second, we show that parameterized versions of other PSPACE-complete problems, like winning certain pebble games and finding restricted resolution refutations, are complete for this class.

Christoph Berkholz and Michael Elberfeld. Parameterized Complexity of Fixed Variable Logics. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 109-120, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{berkholz_et_al:LIPIcs.FSTTCS.2014.109, author = {Berkholz, Christoph and Elberfeld, Michael}, title = {{Parameterized Complexity of Fixed Variable Logics}}, booktitle = {34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)}, pages = {109--120}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-77-4}, ISSN = {1868-8969}, year = {2014}, volume = {29}, editor = {Raman, Venkatesh and Suresh, S. P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.109}, URN = {urn:nbn:de:0030-drops-48367}, doi = {10.4230/LIPIcs.FSTTCS.2014.109}, annote = {Keywords: Parameterized complexity, polynomial space, first-order logic, pebble games, regular resolutions} }

Document

**Published in:** LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)

An algorithmic meta theorem for a logic and a class C of structures
states that all problems expressible in this logic can be solved
efficiently for inputs from $C$. The prime example is Courcelle's
Theorem, which states that monadic second-order (MSO) definable
problems are linear-time solvable on graphs of bounded tree width. We
contribute new algorithmic meta theorems, which state that
MSO-definable problems are (a) solvable by uniform constant-depth
circuit families (AC0 for decision problems and TC0 for counting
problems) when restricted to input structures of bounded tree depth
and (b) solvable by uniform logarithmic-depth circuit families (NC1
for decision problems and #NC1 for counting problems) when a tree
decomposition of bounded width in term representation is part of the
input. Applications of our theorems include a TC0-completeness proof
for the unary version of integer linear programming with a fixed
number of equations and extensions of a recent result that counting
the number of accepting paths of a visible pushdown automaton lies in
#NC1. Our main technical contributions are a new tree automata model
for unordered, unranked, labeled trees; a method for representing the
tree automata's computations algebraically using convolution circuits;
and a lemma on computing balanced width-3 tree decompositions of trees
in TC0, which encapsulates most of the technical difficulties
surrounding earlier results connecting tree automata and NC1.

Michael Elberfeld, Andreas Jakoby, and Till Tantau. Algorithmic Meta Theorems for Circuit Classes of Constant and Logarithmic Depth. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 66-77, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{elberfeld_et_al:LIPIcs.STACS.2012.66, author = {Elberfeld, Michael and Jakoby, Andreas and Tantau, Till}, title = {{Algorithmic Meta Theorems for Circuit Classes of Constant and Logarithmic Depth}}, booktitle = {29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)}, pages = {66--77}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-35-4}, ISSN = {1868-8969}, year = {2012}, volume = {14}, editor = {D\"{u}rr, Christoph and Wilke, Thomas}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.66}, URN = {urn:nbn:de:0030-drops-34059}, doi = {10.4230/LIPIcs.STACS.2012.66}, annote = {Keywords: algorithmic meta theorem, monadic second-order logic, circuit complexity, tree width, tree depth} }