Dagstuhl Seminar Proceedings, Volume 7441

Document

07441 Abstracts Collection – Algorithmic-Logical Theory of Infinite Structures

Authors: Rod Downey, Bakhadyr Khoussainov, Dietrich Kuske, Markus Lohrey, and Moshe Y. Vardi

Abstract

From 28.10. to 02.11.2007, the Dagstuhl Seminar 07441 ``Algorithmic-Logical Theory of Infinite Structures'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

Cite as

Rod Downey, Bakhadyr Khoussainov, Dietrich Kuske, Markus Lohrey, and Moshe Y. Vardi. 07441 Abstracts Collection – Algorithmic-Logical Theory of Infinite Structures. In Algorithmic-Logical Theory of Infinite Structures. Dagstuhl Seminar Proceedings, Volume 7441, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{downey_et_al:DagSemProc.07441.1,
  author =	{Downey, Rod and Khoussainov, Bakhadyr and Kuske, Dietrich and Lohrey, Markus and Vardi, Moshe Y.},
  title =	{{07441 Abstracts Collection – Algorithmic-Logical Theory of Infinite Structures}},
  booktitle =	{Algorithmic-Logical Theory of Infinite Structures},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7441},
  editor =	{Rod Downey and Bakhadyr Khoussainov and Dietrich Kuske and Markus Lohrey and Moshe Y. Vardi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07441.1},
  URN =		{urn:nbn:de:0030-drops-14122},
  doi =		{10.4230/DagSemProc.07441.1},
  annote =	{Keywords: Theories of infinite structures , computable model theory and automatic structures , model checking infinite systems}
}

Document

DOI: 10.4230/DagSemProc.07441.2

07441 Summary – Algorithmic-Logical Theory of Infinite Structures

Authors: Rod Downey, Bakhadyr Khoussainov, Dietrich Kuske, Markus Lohrey, and Moshe Y. Vardi

Abstract

One of the important research fields of theoretical and applied computer science and mathematics is the study of algorithmic, logical and model theoretic properties of structures and their interactions. By a structure we mean typical objects that arise in computer science and mathematics such as data structures, programs, transition systems, graphs, large databases, XML documents, algebraic systems including groups, integers, fields, Boolean algebras and so on.

Cite as

Rod Downey, Bakhadyr Khoussainov, Dietrich Kuske, Markus Lohrey, and Moshe Y. Vardi. 07441 Summary – Algorithmic-Logical Theory of Infinite Structures. In Algorithmic-Logical Theory of Infinite Structures. Dagstuhl Seminar Proceedings, Volume 7441, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{downey_et_al:DagSemProc.07441.2,
  author =	{Downey, Rod and Khoussainov, Bakhadyr and Kuske, Dietrich and Lohrey, Markus and Vardi, Moshe Y.},
  title =	{{07441 Summary – Algorithmic-Logical Theory of Infinite Structures}},
  booktitle =	{Algorithmic-Logical Theory of Infinite Structures},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7441},
  editor =	{Rod Downey and Bakhadyr Khoussainov and Dietrich Kuske and Markus Lohrey and Moshe Y. Vardi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07441.2},
  URN =		{urn:nbn:de:0030-drops-14111},
  doi =		{10.4230/DagSemProc.07441.2},
  annote =	{Keywords: Theories of infinite structures , computable model theory and automatic structures , model checking infinite systems}
}

Document

DOI: 10.4230/DagSemProc.07441.3

Application of verification techniques to inverse monoids

Authors: Markus Lohrey

Abstract

The word problem for inverse monoids generated by a set $Gamma$ subject to relations of the form $e=f$, where $e$ and $f$ are both idempotents in the free inverse monoid generated by $Gamma$, is investigated. It is shown that for every fixed monoid of this form the word problem can be solved in polynomial time which solves an open problem of Margolis and Meakin. For the uniform word problem, where the presentation is part of the input, EXPTIME-completeness is shown. For the Cayley-graphs of these monoids, it is shown that the first-order theory with regular path predicates is decidable. Regular path predicates allow to state that there is a path from a node $x$ to a node $y$ that is labeled with a word from some regular language. As a corollary, the decidability of the generalized word problem is deduced. Finally, some results on free partially commutative inverse monoids are presented.

Cite as

Markus Lohrey. Application of verification techniques to inverse monoids. In Algorithmic-Logical Theory of Infinite Structures. Dagstuhl Seminar Proceedings, Volume 7441, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{lohrey:DagSemProc.07441.3,
  author =	{Lohrey, Markus},
  title =	{{Application of verification techniques to inverse monoids}},
  booktitle =	{Algorithmic-Logical Theory of Infinite Structures},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7441},
  editor =	{Rod Downey and Bakhadyr Khoussainov and Dietrich Kuske and Markus Lohrey and Moshe Y. Vardi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07441.3},
  URN =		{urn:nbn:de:0030-drops-14109},
  doi =		{10.4230/DagSemProc.07441.3},
  annote =	{Keywords: Inverse monoids, word problems, Cayley-graphs, complexity}
}

Document

DOI: 10.4230/DagSemProc.07441.4

Compatibility of Shelah and Stupp's and of Muchnik's iteration with fragments of monadic second order logic

Authors: Dietrich Kuske

Abstract

We investigate the relation between the theory of the iterations in the sense of Shelah-Stupp and of Muchnik, resp., and the theory of the base structure for several logics. These logics are obtained from the restriction of set quantification in monadic second order logic to certain subsets like, e.g., finite sets, chains, and finite unions of chains. We show that these theories of the Shelah-Stupp iteration can be reduced to corresponding theories of the base structure. This fails for Muchnik's iteration.

Cite as

Dietrich Kuske. Compatibility of Shelah and Stupp's and of Muchnik's iteration with fragments of monadic second order logic. In Algorithmic-Logical Theory of Infinite Structures. Dagstuhl Seminar Proceedings, Volume 7441, pp. 1-14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{kuske:DagSemProc.07441.4,
  author =	{Kuske, Dietrich},
  title =	{{Compatibility of Shelah and Stupp's and of Muchnik's iteration with fragments of monadic second order logic}},
  booktitle =	{Algorithmic-Logical Theory of Infinite Structures},
  pages =	{1--14},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7441},
  editor =	{Rod Downey and Bakhadyr Khoussainov and Dietrich Kuske and Markus Lohrey and Moshe Y. Vardi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07441.4},
  URN =		{urn:nbn:de:0030-drops-14078},
  doi =		{10.4230/DagSemProc.07441.4},
  annote =	{Keywords: Logic in computer science, Rabin's tree theorem}
}

Document

DOI: 10.4230/DagSemProc.07441.5

PDL with Intersection and Converse is 2EXP-complete

Authors: Stefan Göller, Markus Lohrey, and Carsten Lutz

Abstract

The logic ICPDL is the expressive extension of Propositional Dynamic Logic (PDL), which admits intersection and converse as program operators. The result of this paper is containment of ICPDL-satisfiability in $2$EXP, which improves the previously known non-elementary upper bound and implies $2$EXP-completeness due to an existing lower bound for PDL with intersection (IPDL). The proof proceeds showing that every satisfiable ICPDL formula has model of tree width at most two. Next, we reduce satisfiability in ICPDL to $omega$-regular tree satisfiability in ICPDL. In the latter problem the set of possible models is restricted to trees of an $omega$-regular tree language. In the final step,$omega$-regular tree satisfiability is reduced the emptiness problem for alternating two-way automata on infinite trees. In this way, a more elegant proof is obtained for Danecki's difficult result that satisfiability in IPDL is in $2EXP$.

Cite as

Stefan Göller, Markus Lohrey, and Carsten Lutz. PDL with Intersection and Converse is 2EXP-complete. In Algorithmic-Logical Theory of Infinite Structures. Dagstuhl Seminar Proceedings, Volume 7441, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{goller_et_al:DagSemProc.07441.5,
  author =	{G\"{o}ller, Stefan and Lohrey, Markus and Lutz, Carsten},
  title =	{{PDL with Intersection and Converse is 2EXP-complete}},
  booktitle =	{Algorithmic-Logical Theory of Infinite Structures},
  pages =	{1--17},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7441},
  editor =	{Rod Downey and Bakhadyr Khoussainov and Dietrich Kuske and Markus Lohrey and Moshe Y. Vardi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07441.5},
  URN =		{urn:nbn:de:0030-drops-14093},
  doi =		{10.4230/DagSemProc.07441.5},
  annote =	{Keywords: Satisfiability, Propositional Dynamic Logic, Computational Complexity}
}

Document

DOI: 10.4230/DagSemProc.07441.6

Tree Automata Make Ordinal Theory Easy

Authors: Thierry Cachat

Abstract

We give a new simple proof of the decidability of the First Order Theory of $(w^{w^i},+)$ and the Monadic Second Order Theory of $(w^i,<)$, improving the complexity in both cases. Our algorithm is based on tree automata and a new representation of (sets of) ordinals by (infinite) trees.

Cite as

Thierry Cachat. Tree Automata Make Ordinal Theory Easy. In Algorithmic-Logical Theory of Infinite Structures. Dagstuhl Seminar Proceedings, Volume 7441, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{cachat:DagSemProc.07441.6,
  author =	{Cachat, Thierry},
  title =	{{Tree Automata Make Ordinal Theory Easy}},
  booktitle =	{Algorithmic-Logical Theory of Infinite Structures},
  pages =	{1--11},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7441},
  editor =	{Rod Downey and Bakhadyr Khoussainov and Dietrich Kuske and Markus Lohrey and Moshe Y. Vardi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07441.6},
  URN =		{urn:nbn:de:0030-drops-14082},
  doi =		{10.4230/DagSemProc.07441.6},
  annote =	{Keywords: Ordinals, First Order theory, Monadic Second Order Theory, tree automata}
}

Dagstuhl Seminar Proceedings, Volume 7441

Publication Details

Access Numbers

Documents

07441 Abstracts Collection – Algorithmic-Logical Theory of Infinite Structures

Abstract

Cite as

07441 Summary – Algorithmic-Logical Theory of Infinite Structures

Abstract

Cite as

Application of verification techniques to inverse monoids

Abstract

Cite as

Compatibility of Shelah and Stupp's and of Muchnik's iteration with fragments of monadic second order logic

Abstract

Cite as

PDL with Intersection and Converse is 2EXP-complete

Abstract

Cite as

Tree Automata Make Ordinal Theory Easy

Abstract

Cite as

Filters

Thanks for your feedback!

Could not send message