We present a new aperiodic tileset containing 11 Wang tiles on 4 colors, and we show that this tileset is minimal, in the sense that no Wang set with either fewer than 11 tiles or fewer than 4 colors is aperiodic. This gives a definitive answer to the problem raised 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 one-counter 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 two-way 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 context-free 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 one-way 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 one-way model to exhibit properties (1) and (2). We define another family of one-way 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, two-way input, etc.). Surprisingly, two-way deterministic machines with multiple checking stacks and multiple reversal-bounded 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 one-way and two-way 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 non-regular 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 polynomial-time 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 one-way nondeterministic $l$-reversal-bounded $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 one-counter automaton with $n$ states, if its language is non-empty, 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 one-counter 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 PSpace-completeness, 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 polynomial-time algorithm for model checking discrete-time 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 poly-logarithmic 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 partially-ordered 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 finite-state 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 polynomial-time algorithm to distinguish the two cases, and to compute the order of polynomial growth, with the language specified as an NFA. For context-free 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 NEXPTIME-complete, 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 NP-complete, 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, PSPACE-complete for an NFA, and co-NEXPTIME-complete for a PDA.

We propose an input/output conformance testing theory utilizing Modal Interface Automata with Input Refusals (IR-MIA) as novel behavioral formalism for both the specification and the implementation under test. A modal refinement relation on IR-MIA 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 IR-MIA, called modal-irioco, enjoys many desirable properties concerning component-based behaviors. First, modal-irioco is preserved under modal refinement and constitutes a preorder under certain restrictions which can be ensured by a canonical input completion for IR-MIA. Second, under the same restrictions, modal-irioco is compositional with respect to parallel composition of IR-MIA with multi-cast and hiding. Finally, the quotient operator on IR-MIA, as the inverse to parallel composition, facilitates decompositionality in conformance testing to solve the unknown-component 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 monoid-theoretical 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 real-time 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 real-time energy functions, it follows that reachability and B\"uchi acceptance in real-time energy automata can be decided in a static way which only involves manipulations of real-time energy functions.

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

We propose an under-approximate reachability analysis algorithm for programs running under the POWER memory model, in the spirit of the work on context-bounded 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 context-bounding 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 context-bounded 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 left-to-right 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 Angluin-style 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 non-deterministic 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 regularity-preserving 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 Csuhaj-Varj\'u, Petre, and Vaszil to model the process of self-assembly 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 (m-1) 3^{n-1} + 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^{n-1}-2)+2$.

Functional transductions realized by two-way 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 one-way transducer, but the given algorithm has non-elementary 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 one-way transducer, whenever it exists, in doubly or triply exponential time, again depending on whether the input transducer is sweeping or two-way. 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 one-counter automata. This problem is known to be undecidable in general and PSPACE-complete for the special case of deterministic one-counter 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 one-counter automata as an open problem. In this paper we resolve this problem positively, utilising a known reduction to a reachability problem on one-counter 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 automata-theoretic 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 post-fault supervisors to prevent the post-fault subsystems from jeopardizing local safety requirements. Furthermore, we apply an assume-guarantee coordination scheme to the controlled subsystems for both the nominal and faulty subsystems so as to achieve the desired specifications of the system. A multi-robot coordination example is used to illustrate the proposed coordination and control architecture.