Seminarium Teoria Automatów

We consider first order formulae over the signature consisting of the symbols of the alphabet, the symbol $<$ (interpreted as a linear order) and the set $\MOD$ of modular numerical predicates. We study the expressive power of $\FO2[<,MOD]$, the two-variable first order logic over this signature, interpreted over finite words. We give an algebraic characterization of the corresponding regular languages in terms of their syntactic morphisms. It follows that one can decide whether a given regular language is captured by $\FO2[<,MOD]$. Our proofs rely on a combination of arguments from semigroup theory (stamps), model theory (E-F games) and combinatorics.

Using nominal sets, we define a uniform approach to logics over data
words, data trees, data graphs and so on. The key technical result is
that, in the equality symmetry, formulas that quantify over data
values are equivalent to formulas that do not quantify over data
values.

This talk will be about boolean (not necessarily positive)
combinations of open sets. I will present a decidable characterization
of the regular languages of infinite trees that are boolean combination
of open sets. In other words, I will present an algorithm, which inputs a
regular language of infinite trees, and decides if the language is a
boolean combination of open sets. This algorithm uses
algebra and games and will be introduced as a set identities that are satisfied if
and only if a language is a boolean combination of open sets and are
easily decidable.

In the talk, we present a model for recursive programs with resource
consumption. It combines the well-known theory of pushdown systems,
which are capable of modeling recursive programs, and the recent theory
of regular cost functions, which can represent resource consumption. For
these kind of systems, we investigate an extension of the traditional
reachability question between two sets of configurations - bounded
reachability. It asks whether there is a finite bound k such that no
more than k resources are needed to achieve reachability. We introduce a
quantitative variant of first-order logic as a framework to solve
bounded reachability and specify constraints for resource consuming
systems. Moreover, we show that this logic is decidable for an extension
of the well-known class of automatic structures.

The reachability problem for Vector Addition Systems (VASs) is a central problem of net theory. The general problem is known decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition (KLMTS decomposition). Recently from this decomposition, we deduced that a final configuration is not reachable from an initial one if and only if there exists a Presburger inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Preburger formula denotes an inductive invariant, we deduce from this result that there exist checkable certificates of non-reachability in the Presburger arithmetic. In particular, there exists a simple algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas. In this presentation we provide the first proof of the VAS reachability problem that is not based on the KLMST decomposition. The proof is based on the notion of production relations inspired from Hauschildt that directly provides the existence of Presburger inductive invariants.

In this paper we show that wB and wS-regular languages satisfy the following separation-type theorem:

Given two disjoint languages both recognised by wB (resp. wS)-automata, there exists an w-regular language separating them.

In particular if a language and its complement are wB (resp. wS)-regular then the language is w-regular.

The result is especially interesting because wB-regular languages are complements of wS-regular languages (see [BC06]). Therefore, the above theorem shows that these are two mutually dual classes that both have the separation property.

The proof technique is quite simple. It makes noticeable use of the framework for the analysis of wB and wS-regular languages proposed by Szymon Toruńczyk in his PhD thesis.

It is well known that first order logic admits a zero one law: a probability that a random structure of size $n$ tends to a limit of either 0 or 1 as $n$ tends to infinity. The same property holds for other logics, like the infinitary logic $L_\infty$.

A similar result is also known for MSO logic on random free labelled trees (McColm). On the other hand, if we consider random rooted labelled trees, then the probability tends to a limit which need not be 0 or 1 \cite (Woods).

Similar limit laws hold for the class of $d$-regular graphs, or where degrees of vertices have a specific distribution (Lynch).

What happens for random planar graphs?

Technically, all the techniques we are using come from previous papers: we are just merging the logical techniques of McColm with the probabilistic and combinatorial results about random planar graphs of McDiarmid, Steger and Welsh.

There are many problems about which we know a lot in the unrestricted
classes, but are still not researched thoroughly in the restricted case.
One of them was the problem of spectra of formulae. A set of integers S
is a spectrum of phi if n \in S iff phi has a model of size n. It is well
known that S is a spectrum of some formula iff the problem of deciding
whether n \in S is in NP when n is given in unary (equivalently, in NE
when n is given in binary). What happens if we restrict our models to
only bounded degree graphs, or only planar graphs?

We provide complexity theoretic characterizations of sets which are
bounded degree and planar spectra of formulae. In case of bounded degree,
there is a very small (polylogarythmic) gap between our lower and upper
bound. In case of planar spectra (where the formula is not required to
check planarity) the gap is polynomial. We also provide a weaker
complexity theoretic characterization of spectra of formulae which force
planarity.

The model checking problem for some logic L and a class of
graphs C is the problem to decide, on input a graph G from C and a
formula phi from L, whether G satisfies phi.
We first introduce the hierarchies of (collapisble) higher-order
pushdown graphs and then survey the various (un)decidability results on
this hierarchy concerning model checking with respect to different
logics. These results give a rather complete picture of the "logical"
behaviour of these hierarchies.
In contrast, structural results on the collapsible pushdown graph
hierarchy are rare. If time permits we will briefly discuss this lack of
understanding of the hierarchy as well.

We consider the model-checking problem for a quantitative
extension of the modal mu-calculus on two classes of infinite
quantitative transition systems. The first class, initialized linear
hybrid systems, is motivated by verification of systems which
exhibit continuous dynamics. We show that the value of a formula
of the quantitative mu-calculus can be approximated with arbitrary
precision on initialized linear hybrid systems. The other class,
increasing tree rewriting systems, is motivated by efforts to allow
counting formulas in discrete verification. On such systems, we
show that the value of a quantitative formula can be computed
exactly. For both these classes of systems, the problem in the end
reduces to solving a new form of parity games with counters.

Using results on finite-time Muller Games (which are defined using scoring
functions that measure how often a given loop in the arena has been visited) we show
how to determine the winner and a finite-state winning strategy in a Muller
game by solving a safety game. Furthermore, it turns out that one can
even determine the most general non-deterministic strategy that avoids
a certain score for the opponent. This is ongoing research and there
are several interesting open questions I could present.

Dickson’s Lemma is a simple yet powerful tool widely used in
decidability proofs, especially when dealing with counters or related
data structures in algorithmics, verification and model-checking,
constraint solving, logic, etc. While Dickson’s Lemma is well-known,
most computer scientists are not aware of the complexity upper bounds
that are entailed by its use. This is mainly because, on this issue,
the existing literature is not very accessible. We propose a new
analysis of the length of bad sequences over (N^k , ≤), improving on
earlier results and providing upper bounds that are essentially tight.

We consider a sequence $t_1,\ldots,t_k$ of XML documents that is
produced by a sequence of local edit operations. To describe
properties of such a sequence, we use a temporal logic. The logic can
navigate both in time and in the document, e.g.~a formula can say that
every node with label $a$ eventually gets a descendant with label $b$.
For every fixed formula, we provide an evaluation algorithm that works
in time $O(k \cdot \log(n))$, where $k$ is the number of edit
operations and $n$ is the maximal size of document that is produced.
In the algorithm, we  represent of  formulas of the logic by a kind of
automaton, which works on sequences of documents.

(a joint work with Mikołaj Bojańczyk and Bartek Klin)

I will state and prove an analog of the Myhill-Nerode
theorem for register automata. The difficulty comes from
the fact that the input alphabet contains data values and
is thus infinite. We have found and elegant way to overcome
the difficulty, using so called nominal sets, i.e., finite sets
"up to permutation of data". The nominal approach seems to
be very robustly usable in many other contexts; I will sketch
some potential further lines of work.

I will present results about the expressive power of
$FO_2(<_h,<_v)$ on finite trees. In particular I will present a
characterization of this logic on finite trees. $FO_2(<_h,<_v)$
is the two variable fragment of first order logic built from the
descendant and following sibling predicates. The characterization
uses (partially) forest algebras.

The task of XML data exchange is to restructure a document conforming to a source schema under a target schema according to certain mapping rules. The rules are typically expressed as source-to-target dependencies using various kinds of patterns, involving horizontal and vertical navigation, as well as data comparisons. The target schema imposes complex conditions on the structure of solutions, possibly inconsistent with the mapping rules. In consequence, for some source documents there may be no solutions.  I will discuss three computational problems: deciding if all documents of the source schema can be mapped to a document of the target schema (absolute consistency), deciding if a given document of the source schema can be mapped (solution existence), and constructing a solution for a given source document (solution building).  It turns out that the complexity of absolute consistency is rather high in  general, but within the polynomial hierarchy for bounded depth schemas. The combined complexity of solution existence and solution building behaves similarly, but the data complexity is very low. In fact, even for very expressive mapping rules,  based on MSO definable queries, absolute consistency is decidable and data complexity of solution existence is polynomial.  This is joint work with Mikolaj Bojanczyk and Leszek Kolodziejczyk. 

We will look at infinite words which are the leaves in lexicographic order of a deterministic tree (in the case where the order type of this object is omega). When the tree can be generated by an order-1 recursion scheme, the corresponding words are known as morphic words. The natural question is then : what are the words generated by higher-order recursion schemes? I will provide an answer for order 2. 

XPath is a logic for finite data trees, and the downward fragment restricts the syntax by allowing only descending paths. I will show that downward XPath has a decidable satisfiability problem. For this, I will work with an automaton model that captures the logic and has a decidable (Exptime) emptiness problem. 

Dear colleagues, 

On Wednesday, 6 October, we start the new academic year at the Automata Theory Seminar. The room is 5870.  We have are happy to have a new group of international visitors, and also new local people. That is why the first meeting of the seminar will be devoted to introductions. Everybody who wants, gets around 3-4 minutes, and 0.5m2 of blackboard to introduce themselves and the problems they like.  

Hopefully, at the end of the seminar, we will recognize each other, and maybe we can form cooperations inside the seminar.  

Hoping to see you soon, 

Mikolaj 

Timed automata and register automata are well-known  models of computation over timed and data words respectively. The former has clocks that allow to test the lapse of time between two events, whilst the latter includes registers
that may store data values for later comparison. Although these two models behave in appearance  differently, several decision problems have the same (un)decidability and complexity results for both models. As a prominent example, emptiness is decidable for alternating automata
with one clock or register, both with non-primitive recursive complexity. This is not by chance.

There is indeed a tight relationship between the two models. I will show that a run of a timed automaton can be simulated by a register automaton, and conversely that a run of a register automaton can be simulated by a timed automaton. These results allow to transfer  complexity and decidability results back and forth between these two kinds of models.

This is joint work with Diego Figueira and Sławek Lasota.

Evaluating a boolean conjunctive query q over a guarded first-order
theory T is equivalent to checking whether (T & not q) is unsatisfiable.
This problem is relevant to the areas of database theory and
description logic. Since q may not be guarded, well known results
about the decidability, complexity, and finite-model property of the
guarded fragment do not obviously carry over to conjunctive query
answering over guarded theories, and had been left open in general.
Extending Rosati's finite chase we construct finite guarded bisimilar
covers of hypergraphs and relational structures such that the projection
of any small substructure of the cover is tree decomposable in the
base structure. Thus we prove for guarded theories T and UCQs q that
(i) T implies q iff T implies q over finite models; and observe that
(ii) answering UCQs over guarded theories is {2EXPTIME}-complete.
The construction is merely polynomial under reasonable restrictions,
also yielding (iii) existence of polynomial-size conformal covers of
hypergraphs of bounded width; (iv) a new proof of the finite model
property of the clique-guarded fragment; (v) the small model property
of the (clique) guarded fragment with optimal bounds; (vi) a PTIME
solution to the canonisation problem modulo guarded bisimulation,
which yields (vii) a capturing result for guarded-bisimulation-invariant
fragment of PTIME.

This is joint work with Georg Gottlob and Martin Otto.

Paweł 14.30
We consider mu-calculus formulas in a normal form: after a prefix of fixed-point quantifiers follows a quantifier-free expression. We prove that the problem of evaluating (model checking) of such formula in a fixed powerset lattice (expression complexity) is polynomial. Assumptions about the quantifier-free part of the expression are weakest possible: it can be any monotone function given by a computational procedure. 

Więcej informacji: http://mimuw.edu.pl/~automat/