Invited speakers

We clarify the succinctness of the different omega-automata types and the size blowup involved in boolean operations on them. We argue that there are good reasons for the classic acceptance conditions, while there is also place for additional acceptance conditions, especially in the deterministic setting; Boolean operations on deterministic automata with the classic acceptance conditions involve an exponential size blowup, which can be avoided by using stronger acceptance conditions. In particular, we analyze the combination of hyper-Rabin and hyper-Streett automata, which we call hyper-dual, and show that in the deterministic setting it allows for exponential succinctness compared to the classic types, boolean operations on it only involve a quadratic size blowup, and its nonemptiness, universality, and containment checks are in PTIME.

We provide a finite set of axioms for identity-free Kleene lattices, which we prove sound and complete for the equational theory of their relational models. Our proof builds on the completeteness theorem for Kleene algebra, and on a novel automata construction that makes it possible to extract axiomatic proofs using a Kleene-like algorithm.

Given a ranked signature, context are terms with a single occurrence of a special symbol • (outside of the signature), which represents a missing subterm. One can naturally build equations over contexts: the context variables are treated as symbols of arity one and a subtitution $S$ assigns to each such a variable a context $S(X)$. A substitution $S$ is extended to terms with context variables in a natural way: $S(X(t))$ is a context $S(X)$ in which the unique occurrence of • is replaced with $S(t)$. For historical reasons, the satisfiability of context equations is usually referred to as context unification. Context unification generalizes word equations and first-order term unification (which are decidable) and is subsumed by second order unification (which is undecidable) and its decidability status remained open for almost two decades. In this talk I will show a PSPACE algorithm for this problem. The idea is to apply simple compression rules (replacing pairs of neighbouring function symbols) to the solution of the context equation; to this end we appropriately modify the equation (without the knowledge of the actual solution) so that compressing the solution can be simulated by compressing parts of the equation. When the compression operations are appropriately chosen, then the size of the instance is polynomial during the whole algorithm, thus giving a PSPACE-upper bound. The best known lower bounds are as for word equations, i.e. NP. The method can be extended to the scenario in which tree-regular constraints for the variables are present, in which case the problem is EXPTIME-complete.

RNA is a chain of ribonucleotides of four kinds (denoted respectively by the letters A, C, G, U).While being synthesized sequentially from its template DNA (transcription), it folds upon itself into intricate higher-dimensional structures in such a way that the free energy is minimized, that is, the more hydrogen bonds between ribonucletoides or larger entropy a structure has, the more likely it is chosen, and furthermore the minimization is done locally. This phenomenon is called cotranscriptional folding (CF). It has turned out to play significant roles in in-vivo computation throughout experiments and recently proven even programmable artificially so as to self-assemble a specific RNA rectangular tile structure in vitro. The next step is to program a computation onto DNA in such a way that the computation can be “called” by cotranscriptional folding. In this novel paradigm of computation, what programmers could do is only twofold: designing a template DNA and setting environmental parameters. Oritatami is an introductory “toy” model to this paradigm of computation. In this model, programmers are also allowed to employ an arbitrarily large finite alphabet as well as an arbitrarily complex rule set for binding. We shall present known architectures of computing in the oritatami model from a simple half-adder to Turing machine along with several programming techniques of use, with hope that they will inspire in-vivo architectures of CF-driven self-assemblable computers, which could be even heritable.