Dagstuhl Seminar Proceedings, Volume 7441
Dagstuhl Seminar Proceedings
DagSemProc
https://www.dagstuhl.de/dagpub/1862-4405
https://dblp.org/db/series/dagstuhl
1862-4405
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
7441
2008
https://drops.dagstuhl.de/entities/volume/DagSemProc-volume-7441
07441 Abstracts Collection – Algorithmic-Logical Theory of Infinite Structures
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.
Theories of infinite structures
computable model theory and automatic structures
model checking infinite systems
1-13
Regular Paper
Rod
Downey
Rod Downey
Bakhadyr
Khoussainov
Bakhadyr Khoussainov
Dietrich
Kuske
Dietrich Kuske
Markus
Lohrey
Markus Lohrey
Moshe Y.
Vardi
Moshe Y. Vardi
10.4230/DagSemProc.07441.1
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
07441 Summary – Algorithmic-Logical Theory of Infinite Structures
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.
Theories of infinite structures
computable model theory and automatic structures
model checking infinite systems
1-2
Regular Paper
Rod
Downey
Rod Downey
Bakhadyr
Khoussainov
Bakhadyr Khoussainov
Dietrich
Kuske
Dietrich Kuske
Markus
Lohrey
Markus Lohrey
Moshe Y.
Vardi
Moshe Y. Vardi
10.4230/DagSemProc.07441.2
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Application of verification techniques to inverse monoids
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.
Inverse monoids
word problems
Cayley-graphs
complexity
1-15
Regular Paper
Markus
Lohrey
Markus Lohrey
10.4230/DagSemProc.07441.3
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Compatibility of Shelah and Stupp's and of Muchnik's iteration with fragments of monadic second order logic
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.
Logic in computer science
Rabin's tree theorem
1-14
Regular Paper
Dietrich
Kuske
Dietrich Kuske
10.4230/DagSemProc.07441.4
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
PDL with Intersection and Converse is 2EXP-complete
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$.
Satisfiability
Propositional Dynamic Logic
Computational Complexity
1-17
Regular Paper
Stefan
Göller
Stefan Göller
Markus
Lohrey
Markus Lohrey
Carsten
Lutz
Carsten Lutz
10.4230/DagSemProc.07441.5
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode
Tree Automata Make Ordinal Theory Easy
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.
Ordinals
First Order theory
Monadic Second Order Theory
tree automata
1-11
Regular Paper
Thierry
Cachat
Thierry Cachat
10.4230/DagSemProc.07441.6
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode