
We present a new aperiodic tile set containing 11 Wang tiles on 4 colors, and
show that this tile set is minimal in the sense that no Wang set with less than
11 tiles is aperiodic, and no Wang set with less than 4 colors is aperiodic.
This gives a final answer to a problem raised by a question asked by Wang in
1961.

We present new results on realtime alternating, private alternating, and
quantum alternating automaton models. Firstly, we show that the emptiness
problem for alternating onecounter automata on unary alphabets is undecidable.
Then, we present two equivalent definitions of realtime private alternating
finite automata (PAFAs). We show that the emptiness problem is undecidable for
PAFAs. Furthermore, PAFAs can recognize some nonregular unary languages,
including the unary squares language, which seems to be difficult even for some
classical counter automata with twoway input. Regarding quantum finite
automata (QFAs), we show that the emptiness problem is undecidable both for
universal QFAs on general alphabets, and for alternating QFAs with two
alternations on unary alphabets. On the other hand, the same problem is
decidable for nondeterministic QFAs on general alphabets. We also show that the
unary squares language is recognized by alternating QFAs with two alternations.

We introduce bud generating systems, which are used for combinatorial
generation. They specify sets of various kinds of combinatorial objects, called
languages. They can emulate contextfree grammars, regular tree grammars, and
synchronous grammars, allowing us to work with all these generating systems in
a unified way. The theory of bud generating systems uses colored operads.
Indeed, an object is generated by a bud generating system if it satisfies a
certain equation in a colored operad. To compute the generating series of the
languages of bud generating systems, we introduce formal power series on
colored operads and several operations on these. Series on colored operads are
crucial to express the languages specified by bud generating systems and allow
us to enumerate combinatorial objects with respect to some statistics. Some
examples of bud generating systems are constructed; in particular to specify
some sorts of balanced trees and to obtain recursive formulas enumerating
these.

We introduce a model of oneway language acceptors (a variant of a checking
stack automaton) and show the following decidability properties: (1) The
deterministic version has a decidable membership problem but has an undecidable
emptiness problem. (2) The nondeterministic version has an undecidable
membership problem and emptiness problem. There are many models of accepting
devices for which there is no difference with these problems between
deterministic and nondeterministic versions, and the same holds for the
emptiness problem. As far as we know, the model we introduce above is the first
oneway model to exhibit properties (1) and (2). We define another family of
oneway acceptors where the nondeterministic version has an undecidable
emptiness problem, but the deterministic version has a decidable emptiness
problem. We also know of no other model with this property in the literature.
We also investigate decidability properties of other variations of checking
stack automata (e.g., allowing multiple stacks, twoway input, etc.).
Surprisingly, twoway deterministic machines with multiple checking stacks and
multiple reversalbounded counters are shown to have a decidable membership
problem, a very general model with this property.

It is well known that the "store language" of every pushdown automaton  the
set of store configurations (state and stack contents) that can appear as an
intermediate step in accepting computations  is a regular language. Here many
models of language acceptors with various data structures are examined, along
with a study of their store languages. For each model, an attempt is made to
find the simplest model that accepts their store languages. Some connections
between store languages of oneway and twoway machines generally are
demonstrated, as with connections between nondeterministic and deterministic
machines. A nice application of these store language results is also presented,
showing a general technique for proving families accepted by many deterministic
models are closed under right quotient with regular languages, resolving some
open questions (and significantly simplifying proofs for others that are known)
in the literature. Lower bounds on the space complexity for recognizing store
languages for the languages to be nonregular are obtained.

The complexity and decidability of various decision problems involving the
shuffle operation are studied. The following three problems are all shown to be
$NP$complete: given a nondeterministic finite automaton (NFA) $M$, and two
words $u$ and $v$, is $L(M)$ not a subset of $u$ shuffled with $v$, is $u$
shuffled with $v$ not a subset of $L(M)$, and is $L(M)$ not equal to $u$
shuffled with $v$? It is also shown that there is a polynomialtime algorithm
to determine, for $NFA$s $M_1, M_2$ and a deterministic pushdown automaton
$M_3$, whether $L(M_1)$ shuffled with $L(M_2)$ is a subset of $L(M_3)$. The
same is true when $M_1, M_2,M_3$ are oneway nondeterministic
$l$reversalbounded $k$counter machines, with $M_3$ being deterministic.
Other decidability and complexity results are presented for testing whether
given languages $L_1, L_2$ and $R$ from various languages families satisfy
$L_1$ shuffled with $L_2$ is a subset of $R$, and $R$ is a subset of $L_1$
shuffled with $L_2$. Several closure results on shuffle are also shown.

We show that any onecounter automaton with $n$ states, if its language is
nonempty, accepts some word of length at most $O(n^2)$. This closes the gap
between the previously known upper bound of $O(n^3)$ and lower bound of
$\Omega(n^2)$. More generally, we prove a tight upper bound on the length of
shortest paths between arbitrary configurations in onecounter transition
systems (weaker bounds have previously appeared in the literature).

The regular separability problem asks, for two given languages, if there
exists a regular language including one of them but disjoint from the other.
Our main result is decidability, and PSpacecompleteness, of the regular
separability problem for languages of one counter automata without zero tests
(also known as one counter nets). This contrasts with undecidability of the
regularity problem for one counter nets, and with undecidability of the regular
separability problem for one counter automata, which is our second result.

Unambiguous automata are nondeterministic automata in which every word has at
most one accepting run. In this paper we give a polynomialtime algorithm for
model checking discretetime Markov chains against $\omega$regular
specifications represented as unambiguous automata. We furthermore show that
the complexity of this model checking problem lies in NC: the subclass of P
comprising those problems solvable in polylogarithmic parallel time. These
complexity bounds match the known bounds for model checking Markov chains
against specifications given as deterministic automata, notwithstanding the
fact that unambiguous automata can be exponentially more succinct than
deterministic automata. We report on an implementation of our procedure,
including an experiment in which the implementation is used to model check LTL
formulas on Markov chains.

Given a partiallyordered finite alphabet $\Sigma$ and a language $L\subseteq
\Sigma^*$, how large can an antichain in $L$ be (where $L$ is given the
lexicographic ordering)? More precisely, since $L$ will in general be infinite,
we should ask about the rate of growth of maximum antichains consisting of
words of length $n$. This fundamental property of partial orders is known as
the width, and in a companion work we show that the problem of computing the
information leakage permitted by a deterministic interactive system modeled as
a finitestate transducer can be reduced to the problem of computing the width
of a certain regular language. In this paper, we show that if $L$ is regular
then there is a dichotomy between polynomial and exponential antichain growth.
We give a polynomialtime algorithm to distinguish the two cases, and to
compute the order of polynomial growth, with the language specified as an NFA.
For contextfree languages we show that there is a similar dichotomy, but now
the problem of distinguishing the two cases is undecidable. Finally, we
generalise the lexicographic order to tree languages, and show that for regular
tree languages there is a trichotomy between polynomial, exponential and doubly
exponential antichain growth.

We study the following natural variation on the classical universality
problem: given a language $L(M)$ represented by $M$ (e.g., a DFA/RE/NFA/PDA),
does there exist an integer $\ell \geq 0$ such that $\Sigma^\ell \subseteq
L(M)$? In the case of an NFA, we show that this problem is NEXPTIMEcomplete,
and the smallest such $\ell$ can be doubly exponential in the number of states.
This particular case was formulated as an open problem in 2009, and our
solution uses a novel and involved construction. In the case of a PDA, we show
that it is recursively unsolvable, while the smallest such $\ell$ is not
bounded by any computable function of the number of states. In the case of a
DFA, we show that the problem is NPcomplete, and $e^{\sqrt{n \log n}
(1+o(1))}$ is an asymptotically tight upper bound for the smallest such $\ell$,
where $n$ is the number of states. Finally, we prove that in all these cases,
the problem becomes computationally easier when the length $\ell$ is also given
in binary in the input: it is polynomially solvable for a DFA, PSPACEcomplete
for an NFA, and coNEXPTIMEcomplete for a PDA.

We propose an input/output conformance testing theory utilizing Modal
Interface Automata with Input Refusals (IRMIA) as novel behavioral formalism
for both the specification and the implementation under test. A modal
refinement relation on IRMIA allows distinguishing between obligatory and
allowed output behaviors, as well as between implicitly underspecified and
explicitly forbidden input behaviors. The theory therefore supports positive
and negative conformance testing with optimistic and pessimistic environmental
assumptions. We further show that the resulting conformance relation on IRMIA,
called modalirioco, enjoys many desirable properties concerning
componentbased behaviors. First, modalirioco is preserved under modal
refinement and constitutes a preorder under certain restrictions which can be
ensured by a canonical input completion for IRMIA. Second, under the same
restrictions, modalirioco is compositional with respect to parallel
composition of IRMIA with multicast and hiding. Finally, the quotient
operator on IRMIA, as the inverse to parallel composition, facilitates
decompositionality in conformance testing to solve the unknowncomponent
problem.

The vertices of any (combinatorial) Kashiwara crystal graph carry a natural
monoid structure given by identifying words labelling vertices that appear in
the same position of isomorphic components of the crystal. Working on a purely
combinatorial and monoidtheoretical level, we prove some foundational results
for these crystal monoids, including the observation that they have decidable
word problem when their weight monoid is a finite rank free abelian group. The
problem of constructing finite complete rewriting systems, and biautomatic
structures, for crystal monoids is then investigated. In the case of Kashiwara
crystals of types $A_n$, $B_n$, $C_n$, $D_n$, and $G_2$ (corresponding to the
$q$analogues of the Lie algebras of these types) these monoids are precisely
the generalised plactic monoids investigated in work of Lecouvey. We construct
presentations via finite complete rewriting systems for all of these types
using a unified proof strategy that depends on Kashiwara's crystal bases and
analogies of Young tableaux, and on Lecouvey's presentations for these monoids.
As corollaries, we deduce that plactic monoids of these types have finite
derivation type and satisfy the homological finiteness properties left and
right $\mathrm{FP}_\infty$. These rewriting systems are then applied to show
that plactic monoids of these types are biautomatic and thus have word problem
soluble in quadratic time.

We develop a $^*$continuous Kleene $\omega$algebra of realtime energy
functions. Together with corresponding automata, these can be used to model
systems which can consume and regain energy (or other types of resources)
depending on available time. Using recent results on $^*$continuous Kleene
$\omega$algebras and computability of certain manipulations on realtime
energy functions, it follows that reachability and B\"uchi acceptance in
realtime energy automata can be decided in a static way which only involves
manipulations of realtime energy functions.

We show that the class of groups with $k$multiple contextfree word problem
is closed under graphs of groups with finite edge groups.

We propose an underapproximate reachability analysis algorithm for programs
running under the POWER memory model, in the spirit of the work on
contextbounded analysis intitiated by Qadeer et al. in 2005 for detecting bugs
in concurrent programs (supposed to be running under the classical SC model).
To that end, we first introduce a new notion of contextbounding that is
suitable for reasoning about computations under POWER, which generalizes the
one defined by Atig et al. in 2011 for the TSO memory model. Then, we provide a
polynomial size reduction of the contextbounded state reachability problem
under POWER to the same problem under SC: Given an input concurrent program P,
our method produces a concurrent program P' such that, for a fixed number of
context switches, running P' under SC yields the same set of reachable states
as running P under POWER. The generated program P' contains the same number of
processes as P, and operates on the same data domain. By leveraging the
standard model checker CBMC, we have implemented a prototype tool and applied
it on a set of benchmarks, showing the feasibility of our approach.

In this work we present a theoretical model for differentiable programming.
We construct an algebraic language that encapsulates formal semantics of
differentiable programs by way of Operational Calculus. The algebraic nature of
Operational Calculus can alter the properties of the programs that are
expressed within the language and transform them into their solutions.
In our model programs are elements of programming spaces and viewed as maps
from the virtual memory space to itself. Virtual memory space is an algebra of
programs, an algebraic data structure one can calculate with. We define the
operator of differentiation ($\partial$) on programming spaces and, using its
powers, implement the general shift operator and the operator of program
composition. We provide the formula for the expansion of a differentiable
program into an infinite tensor series in terms of the powers of $\partial$. We
express the operator of program composition in terms of the generalized shift
operator and $\partial$, which implements a differentiable composition in the
language. Such operators serve as abstractions over the tensor series algebra,
as main actors in our language.
We demonstrate our models usefulness in differentiable programming by using
it to analyse iterators, deriving fractional iterations and their iterating
velocities, and explicitly solve the special case of ReduceSum.

We present a uniform method for translating an arbitrary nondeterministic
finite automaton (NFA) into a deterministic mass action input/output chemical
reaction network (I/O CRN) that simulates it. The I/O CRN receives its input as
a continuous time signal consisting of concentrations of chemical species that
vary to represent the NFA's input string in a natural way. The I/O CRN exploits
the inherent parallelism of chemical kinetics to simulate the NFA in real time
with a number of chemical species that is linear in the size of the NFA. We
prove that the simulation is correct and that it is robust with respect to
perturbations of the input signal, the initial concentrations of species, the
output (decision), and the rate constants of the reactions of the I/O CRN.

Let $b$ be an integer strictly greater than $1$. Each set of nonnegative
integers is represented in base $b$ by a language over $\{0, 1, \dots, b 
1\}$. The set is said to be $b$recognisable if it is represented by a regular
language. It is known that ultimately periodic sets are $b$recognisable, for
every base $b$, and Cobham's theorem implies the converse: no other set is
$b$recognisable in every base $b$.
We consider the following decision problem: let $S$ be a set of nonnegative
integers that is $b$recognisable, given as a finite automaton over $\{0,1,
\dots, b  1\}$, is $S$ periodic? Honkala showed in 1986 that this problem is
decidable. Later on, Leroux used in 2005 the convention to write number
representations with the least significant digit first (LSDF), and designed a
quadratic algorithm to solve a more general problem.
We use here LSDF convention as well and give a structural description of the
minimal automata that accept periodic sets. Then, we show that it can be
verified in linear time if a minimal automaton meets this description. In
general, this yields a $O(b \log(n))$ procedure to decide whether an automaton
with $n$ states accepts an ultimately periodic set of nonnegative integers.

We consider the problem of evaluating in streaming (i.e., in a single
lefttoright pass) a nested word transduction with a limited amount of memory.
A transduction T is said to be height bounded memory (HBM) if it can be
evaluated with a memory that depends only on the size of T and on the height of
the input word. We show that it is decidable in coNPTime for a nested word
transduction defined by a visibly pushdown transducer (VPT), if it is HBM. In
this case, the required amount of memory may depend exponentially on the height
of the word. We exhibit a sufficient, decidable condition for a VPT to be
evaluated with a memory that depends quadratically on the height of the word.
This condition defines a class of transductions that strictly contains all
determinizable VPTs.

We present an Angluinstyle algorithm to learn nominal automata, which are
acceptors of languages over infinite (structured) alphabets. The abstract
approach we take allows us to seamlessly extend known variations of the
algorithm to this new setting. In particular we can learn a subclass of nominal
nondeterministic automata. An implementation using a recently developed
Haskell library for nominal computation is provided for preliminary
experiments.

The \emph{state complexity} of a regular language $L_m$ is the number $m$ of
states in a minimal deterministic finite automaton (DFA) accepting $L_m$. The
state complexity of a regularitypreserving binary operation on regular
languages is defined as the maximal state complexity of the result of the
operation where the two operands range over all languages of state complexities
$\le m$ and $\le n$, respectively. We find a tight upper bound on the state
complexity of the binary operation \emph{overlap assembly} on regular
languages. This operation was introduced by CsuhajVarj\'u, Petre, and Vaszil
to model the process of selfassembly of two linear DNA strands into a longer
DNA strand, provided that their ends "overlap". We prove that the state
complexity of the overlap assembly of languages $L_m$ and $L_n$, where $m\ge 2$
and $n\ge1$, is at most $2 (m1) 3^{n1} + 2^n$. Moreover, for $m \ge 2$ and $n
\ge 3$ there exist languages $L_m$ and $L_n$ over an alphabet of size $n$ whose
overlap assembly meets the upper bound and this bound cannot be met with
smaller alphabets. Finally, we prove that $m+n$ is a tight upper bound on the
overlap assembly of unary languages, and that there are binary languages whose
overlap assembly has exponential state complexity at least $m(2^{n1}2)+2$.

Functional transductions realized by twoway transducers (or, equally, by
streaming transducers or MSO transductions) are the natural and standard notion
of "regular" mappings from words to words. It was shown in 2013 that it is
decidable if such a transduction can be implemented by some oneway transducer,
but the given algorithm has nonelementary complexity. We provide an algorithm
of different flavor solving the above question, that has doubly exponential
space complexity. In the special case of sweeping transducers the complexity is
one exponential less. We also show how to construct an equivalent oneway
transducer, whenever it exists, in doubly or triply exponential time, again
depending on whether the input transducer is sweeping or twoway. In the
sweeping case our construction is shown to be optimal.

Freeze LTL is a temporal logic with registers that is suitable for specifying
properties of data words. In this paper we study the model checking problem for
Freeze LTL on onecounter automata. This problem is known to be undecidable in
general and PSPACEcomplete for the special case of deterministic onecounter
automata. Several years ago, Demri and Sangnier investigated the model checking
problem for the flat fragment of Freeze LTL on several classes of counter
automata and posed the decidability of model checking flat Freeze LTL on
onecounter automata as an open problem. In this paper we resolve this problem
positively, utilising a known reduction to a reachability problem on
onecounter automata with parameterised equality and disequality tests. Our
main technical contribution is to show decidability of the latter problem by
translation to Presburger arithmetic.

We investigate the coordination and control problems of distributed discrete
event systems that are composed of multiple subsystems subject to potential
actuator and/or sensor faults. We model actuator faults as local
controllability loss of certain actuator events and sensor faults as
observability failure of certain sensor readings, respectively. Starting from
automatatheoretic models that characterize behaviors of the subsystems in the
presence of faulty actuators and/or sensors, we establish necessary and
sufficient conditions for the existence of actuator and sensor fault tolerant
supervisors, respectively, and synthesize appropriate local postfault
supervisors to prevent the postfault subsystems from jeopardizing local safety
requirements. Furthermore, we apply an assumeguarantee coordination scheme to
the controlled subsystems for both the nominal and faulty subsystems so as to
achieve the desired specifications of the system. A multirobot coordination
example is used to illustrate the proposed coordination and control
architecture.