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