23 pages, 12 figures. This is an expanded version of the conference paper published in C. Campeanu et al. (eds.), Descriptional Complexity of Formal Systems. DCFS 2016 [Lect. Notes Comp. Sci. 9777], Springer-Verlag, Berlin-Heidelberg-N.Y., 2016, 1-17
We present a few results and several open problems concerning complete deterministic finite automata in which every non-empty subset of the state set occurs as the image of the whole state set under the action of a suitable input word.
A deterministic finite automaton in which every non-empty set of states occurs as the image of the whole state set under the action of a suitable input word is called completely reachable. We characterize such automata in terms of graphs and trees.
A complete deterministic finite automaton in which every non-empty subset of the state set occurs as the image of the whole state set under the action of a suitable input word is called completely reachable. We characterize completely reachable automata in terms of certain directed graphs.
This article focuses on subset reachability in synchronizing automata. First, we provide families of synchronizing automata with subsets which cannot be reached with short words. These families do not fulfil Don's Conjecture about subset reachability. Moreover, they show that some subsets need exponentially long words to be reached, and that the restriction of the conjecture to included subsets also does not hold. Second, we analyze completely reachable automata and provide a counterexample to the conjecture of Bondar and Volkov about the so-called $Γ_1$-graph. We finally prove an alternative …
We characterize complete deterministic finite automata with two input letters in which every non-empty set of states occurs as the image of the whole state set under the action of a suitable input word. The characterization leads to a polynomial-time algorithm for recognizing this class of automata.
We study three notions of directability of fuzzy automata akin to the D1-, D2- and D3-directability of nondeterministic automata. Thus an input word $w$ of a fuzzy automaton is D1-directing if a fixed single state is reachable by $w$ from all states, D2-directing if exactly the same states are reachable by $w$ from every state, and D3-directing if there is a state reachable by $w$ from every state. We study the various sets of directing words of fuzzy automata, prove that the directability properties are decidable, and show how such results can be deduced from the theory of directable nondeter…
Most slowly synchronizing automata over binary alphabets are circular, i.e., containing a letter permuting the states in a single cycle, and their set of synchronizing words has maximal state complexity, which also implies complete reachability.Here, we take a closer look at generalized circular and completely reachable automata. We derive that over a binary alphabet every completely reachable automaton must be circular, a consequence of a structural result stating that completely reachable automata over strictly less letters than states always contain permutational letters. We state sufficien…
We give a new characterization of primitive permutation groups tied to the notion of completely reachable automata. Also, we introduce sync-maximal permutation groups tied to the state complexity of the set of synchronizing words of certain associated automata and show that they are contained between the $2$-homogeneous and the primitive groups. Lastly, we define $k$-reachable groups in analogy with synchronizing groups and motivated by our characterization of primitive permutation groups. But the results show that a $k$-reachable permutation group of degree $n$ with $6 \le k \le n - 6$ is eit…
Tree Regular Model Checking (TRMC) is the name of a family of techniques for analyzing infinite-state systems in which states are represented by terms, and sets of states by Tree Automata (TA). The central problem in TRMC is to decide whether a set of bad states is reachable. The problem of computing a TA representing (an over- approximation of) the set of reachable states is undecidable, but efficient solutions based on completion or iteration of tree transducers exist. Unfortunately, the TRMC framework is unable to efficiently capture both the complex structure of a system and of some of its…
We consider the problem of state-space reduction for nondeterministic weakly-hierarchical visibly pushdown automata (VPA). VPA recognize a robust and algorithmically tractable fragment of context-free languages that is natural for modeling programs. We define an equivalence relation that is sufficient for language-preserving quotienting of VPA. Our definition allows to merge states that have different behavior, as long as they show the same behavior for reachable equivalent stacks. We encode the existence of such a relation as a Boolean partial maximum satisfiability (PMax-SAT) problem and pre…
Under the assumption $\mathcal{P} \neq \mathcal{NP}$, we prove that two natural problems from the theory of synchronizing automata cannot be solved in polynomial time. The first problem is to decide whether a given reachable partial automaton is synchronizing. The second one is, given an $n$-state binary complete synchronizing automaton, to compute its reset threshold within performance ratio less than $d \ln{(n)}$ for a specific constant $d>0$.
We show that if a semisimple synchronizing automaton with $n$ states has a minimal reachable non-unary subset of cardinality $r\ge 2$, then there is a reset word of length at most $(n-1)D(2,r,n)$, where $D(2,r,n)$ is the $2$-packing number for families of $r$-subsets of $[1,n]$.
We consider the first problem that appears in any application of synchronizing automata, namely, the problem of deciding whether or not a given $n$-state $k$-letter automaton is synchronizing. First we generalize results from \cite{RandSynch},\cite{On2Problems} for the case of strongly connected partial automata. Specifically, for $k>1$ we show that an automaton is synchronizing with probability $1-O(\frac{1}{n^{0.5k}})$ and present an algorithm with linear in $n$ expected time, while the best known algorithm is quadratic on each instance. This results are interesting due to their applications…
This paper deals with the CREP (Configuration REachability Problem) for non-uniform cellular automata (CAs). The cells of non-uniform CAs, we have considered here, can use different Wolfram's rules to generate their next states. We report an algorithm which decides whether or not a configuration of a given (non-uniform) cellular automaton is reachable from another configuration. A characterization tool, named Reachability tree, is used to develop theories and the decision algorithm for the CREP. Though the worst case complexity of the algorithm is exponential in time and space, but the average…
The languages of infinite timed words accepted by timed automata are traditionally defined using Buchi-like conditions. These acceptance conditions focus on the set of locations visited infinitely often along a run, but completely ignore quantitative timing aspects. In this paper we propose a natural quantitative semantics for timed automata based on the so-called frequency, which measures the proportion of time spent in the accepting locations. We study various properties of timed languages accepted with positive frequency, and in particular the emptiness and universality problems.
This paper presents the first step of a wider research effort to apply tree automata completion to the static analysis of functional programs. Tree Automata Completion is a family of techniques for computing or approximating the set of terms reachable by a rewriting relation. The completion algorithm we focus on is parameterized by a set E of equations controlling the precision of the approximation and influencing its termination. For completion to be used as a static analysis, the first step is to guarantee its termination. In this work, we thus give a sufficient condition on E and T(F) for c…
We propose two hard problems in cellular automata. In particular the problems are: [DDP$^M_{n,p}$] Given two \emph{randomly} chosen configurations $t$ and $s$ of a cellular automata of length $n$, find the number of transitions $τ$ between $s$ and $t$. [SDDP$^δ_{k,n}$] Given two \emph{randomly} chosen configurations $s$ of a cellular automata of length $n$ and $x$ of length $k<n$, find the configuration $t$ such that $k$ number of cells of $t$ is fixed to $x$ and $t$ is reachable from $s$ within $δ$ transitions. We show that the discrete logarithm problem over the finite field reduces to DDP$^…
The set of synchronizing words of a given $n$-state automaton forms a regular language recognizable by an automaton with $2^n - n$ states. The size of a recognizing automaton for the set of synchronizing words is linked to computational problems related to synchronization and to the length of synchronizing words. Hence, it is natural to investigate synchronizing automata extremal with this property, i.e., such that the minimal deterministic automaton for the set of synchronizing words has $2^n - n$ states. The sync-maximal permutation groups have been introduced in [{\sc S. Hoffmann}, Complete…
Visibly pushdown automata (VPA), introduced by Alur and Madhusuan in 2004, is a subclass of pushdown automata whose stack behavior is completely determined by the input symbol according to a fixed partition of the input alphabet. Since its introduce, VPAs have been shown to be useful in various context, e.g., as specification formalism for verification and as automaton model for processing XML streams. Due to high complexity, however, implementation of formal verification based on VPA framework is a challenge. In this paper we consider the problem of implementing VPA-based model checking algor…
We cast new light on the existing models of one-way deterministic topological automata by introducing a fresh but general, convenient model, in which, as each input symbol is read, an interior system of an automaton, known as a configuration, continues to evolve in a topological space by applying continuous transition operators one by one. The acceptance and rejection of a given input are determined by observing the interior system after the input is completely processed. Such automata naturally generalize one-way finite automata of various types, including deterministic, probabilistic, quantu…
Herein we survey the main results concerning quantum automata and machines with classical control. These machines were originally proposed by Sernadas et al in [37], during the FCT QuantLog project. First, we focus on the expressivity of quantum automata with both quantum and classical states. We revise the result obtained in [32] where it was proved that such automata are able to recognise, with exponentially less states than deterministic finite automata, a family of regular languages that cannot be recognised by other types of quantum automata. Finally, we revise the concept of quantum Turi…
Stochastic languages are the languages recognized by probabilistic finite automata (PFAs) with cutpoint over the field of real numbers. More general computational models over the same field such as generalized finite automata (GFAs) and quantum finite automata (QFAs) define the same class. In 1963, Rabin proved the set of stochastic languages to be uncountable presenting a single 2-state PFA over the binary alphabet recognizing uncountably many languages depending on the cutpoint. In this paper, we show the same result for unary stochastic languages. Namely, we exhibit a 2-state unary GFA, a 2…
The locality of a graph problem is the smallest distance $T$ such that each node can choose its own part of the solution based on its radius-$T$ neighborhood. In many settings, a graph problem can be solved efficiently with a distributed or parallel algorithm if and only if it has a small locality. In this work we seek to automate the study of solvability and locality: given the description of a graph problem $Π$, we would like to determine if $Π$ is solvable and what is the asymptotic locality of $Π$ as a function of the size of the graph. Put otherwise, we seek to automatically synthesize ef…
Individual machines in flexible production lines explicitly expose capabilities at their interfaces by means of parametric skills. Given such a set of configurable machines, a line integrator is faced with the problem of finding and tuning parameters for each machine such that the overall production line implements given safety and temporal requirements in an optimized and robust fashion. We formalize this problem of configuring and orchestrating flexible production lines as a parameter synthesis problem for systems of parametric timed automata, where interactions are based on skills. Paramete…