
We clarify the succinctness of the different omegaautomata 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 hyperRabin and hyperStreett automata, which we call hyperdual, 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 identityfree 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 Kleenelike 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 firstorder 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 PSPACEupper bound.
The best known lower bounds are as for word equations, i.e. NP.
The method can be extended to the scenario in which treeregular
constraints for the variables are present,
in which case the problem is EXPTIMEcomplete.

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 higherdimensional 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 invivo computation throughout experiments and recently proven even programmable artificially so as to selfassemble 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 halfadder to Turing machine along with several programming techniques of use, with hope that they will inspire invivo architectures of CFdriven selfassemblable computers, which could be even heritable.