This paper establishes a lower bound on the number of states necessary in the worst case to simulate an n-state two-way nondeterministic finite automaton (2NFA) by a one-way unambiguous finite automaton (UFA). It is proved that for every n, there is a language recognized by an n-state 2NFA that requires a UFA with at least ∑ _k=1^n (k - 1)! k! {[ n; k ]}{[ n+1; k ]} = ( n^2n+2 / e^2n ) states, where {[ n; k ]} denotes Stirling’s numbers of the second kind. This result is proved by estimating the rank of a certain matrix, which describes every possible behaviour of n-state 2NFAs during their computation.
Prior work of Gavryushkin, Khoussainov, Jain and Stephan investigated what algebraic structures can be realised in worlds given by a positive (= recursively enumerable) equivalence relation which partitions the natural numbers into infinitely many equivalence classes. The present work investigates the infinite one-one numbered recursively enumerable (r.e.) families realised by such relations and asks how the choice of the equivalence relation impacts the learnability properties of these classes when studying learnability in the limit from positive examples, also known as learning from text. For all choices of such positive equivalence relations, for each of the following entries, there are one-one numbered r.e. families which satisfy it: (a) they are behaviourally correctly learnable but not vacillatorily learnable; (b) they are explanatorily learnable but not confidently learnable; (c) they are not behaviourally correctly learnable. Furthermore, there is a positive equivalence relation which enforces that (d) every vacillatorily learnable one-one numbered family of languages closed under this equivalence relation is already explanatorily learnable and cannot be confidently learnable.
Cadences are structurally maximal arithmetic progressions of indices corresponding to equal characters in an underlying string. This paper provides a polynomial time detection algorithm for 3-cadences in grammar-compressed binary strings. This algorithm also translates to a linear time detection algorithm for 3-cadences in uncompressed binary strings. Furthermore, this paper proves that several variants of the cadence detection problem are NP-complete for grammar-compressed strings. As a consequence, the equidistant subsequence matching problem with patterns of length three is NP-complete for grammar-compressed ternary strings.
Fusion grammars are a novel approach to the generation of hypergraph languages. A fusion grammar is a hypergraph grammar which provides a start hypergraph of small connected components. To get large connected hypergraphs, they can be copied multiple times and can be fused by the application of fusion rules. In this paper, we analyze the non-emptiness problem for connection-preserving fusion grammars and show that this is an NP complete problem. We show this by relating language generation by connection-preserving fusion grammars to some variant of integer linear programming.
Since the famous construction of “the hardest context-free language” by Greibach (1973), the existence of hardest languages under homomorphic reductions has been investigated for quite a few language families. This paper shows that for one-way real-time cellular automata, also known as trellis automata, there is no hardest language, whereas for linear-time cellular automata, the hardest language is constructed.
In this paper, we examine the problem of finding unit refutations of Horn constraint systems (HCSs). Recall that a Horn constraint is a linear constraint in which every coefficient belongs to the set {0,1,-1} and in which at most one coefficient is positive. In the current work, we extend the notion of unit refutations from CNF formulas to systems of linear constraints. Recall that for CNF formulas a unit resolution refutation is one in which every resolution step uses a one-literal (unit) clause. The equivalent notion in linear systems requires every inference step to use a one-variable (absolute) constraint. We analyze two problems associated with unit refutations of Horn constraint systems. In the length-bounded tree-like unit refutation (TLUR _D ) problem, we ask if a given Horn constraint system has a tree-like unit refutation using at most L inference steps. In the optimal tree-like unit refutation (TLUR _Opt ) problem, we ask for a tree-like unit refutation with the fewest inference steps. We show that the former problem is NP-complete and the latter is NPO-complete. We also show that the TLUR _D problem does not admit a polynomial size kernel with respect to a natural output parameter under some well-accepted complexity theoretic assumptions.
We present Mealy machines with a single timer (MM1Ts), a class of models that is both sufficiently expressive to describe the real-time behavior of many realistic applications, and can be learned efficiently. We show how learning algorithms for MM1Ts can be obtained via a reduction to the problem of learning Mealy machines. We describe an implementation of an MM1T learner on top of LearnLib, and compare its performance with recent algorithms proposed by Aichernig et al. and An et al. on several realistic benchmarks.
(Non)-Deterministic finite automata are one of the simplest models of computation studied in automata theory. Here we study them through the lens of succinct data structures. Towards this goal, we design a data structure for any deterministic automaton D having n states over a σ-letter alphabet Σ using (σ−1)nlogn(1+o(1)) bits, that determines, given a string x, whether D accepts x in optimal O(|x|) time. We also consider the case when there are N<σn non-failure transitions, and obtain various time-space trade-offs. Here some of our results are better than the recent work of Cotumaccio and Prezza (SODA 2021). We also exhibit a data structure for non-deterministic automaton N using σn2+n bits that takes O(n2|x|) time for string membership checking. Finally, we also provide time and space efficient algorithms for performing several standard operations on the languages accepted by finite automata.
We develop a generic framework to extend the logics LTL, CTL+ and CTL⁎ by automata-based connectives from formal language classes and analyse this framework with regard to regular languages, visibly pushdown languages, deterministic and non-deterministic context-free languages. More precisely, we consider how the use of different automata classes changes the expressive power of the logics and provide algorithms for the satisfiability and model checking problems induced by the use of different classes of automata. For the model checking problem, we treat not only finite Kripke transition systems, but also visibly pushdown systems and pushdown systems. We provide completeness or undecidability results in all cases and show that the extensions we consider can formulate properties not expressible in classical temporal logics or regular extensions thereof.
Formal languages are in the core of models of computation and their behavior. A rich family of models for many classes of languages have been widely studied. Hyperproperties lift conventional trace-based languages from a set of execution traces to a set of sets of executions. Hyperproperties have been shown to be a powerful formalism for expressing and reasoning about information-flow security policies and important properties of cyber-physical systems. Although there is an extensive body of work on formal-language representation of trace properties, we currently lack such a general characterization for hyperproperties. We introduce hyperlanguages over finite words and models for expressing them. Essentially, these models express multiple words by using assignments to quantified word variables . Relying on the standard models for regular languages, we propose hyperregular expressions and finite-word hyperautomata (NFH) , for modeling the class of regular hyperlanguages . We demonstrate the ability of regular hyperlanguages to express hyperproperties for finite traces. We explore the closure properties and the complexity of the fundamental decision problems such as nonemptiness, universality, membership, and containment for various fragments of NFH.
In this paper we continue the research on usefulness of information examining the effect of supplementary information on the complexity of solving a problem (see Rovan and Sádovský [ 7 ] for an overview). We use deterministic finite automata for a formal setting. Given a problem (a regular language) L prob we measure the complexity of its solution – a DFA A prob such that L prob = L ( A prob ) – using the state complexity. A supplementary information (advice) L adv given by A adv is useful if a simpler problem L new given by A new exists such that L prob = L new ∩ L adv and both L new and L adv are simpler than L prob . This is formalized via the notion of decomposability of finite automata (see [ 1 ] for DFA case and [ 7 ] for NFA case). We address the problem of decomposability of unary regular languages and give a characterization of λ -cyclic languages upon deterministic decomposability.
We introduce context-free grammars with lookahead. The grammars are an extension of both context-free grammars and parsing expression grammars, hence we can handle the two grammars in a unified way. To accommodate lookahead, we use a language with lookahead, which is a set of string pairs. We considered the grammar as a system of equations and give the language with lookahead by the limit of iterations from the empty set. The language class is closed under union, intersection, complement, and a weak version of concatenation and Kleene star.
We consider weighted graphs with parameterized weights and we propose an algorithm that, given such a graph and a source node, builds a collection of trees, each one describing the shortest paths from the source to all the other nodes of the graph for a particular zone of the parameter space. Moreover, the union of these zones covers the full parameter space: given any valuation of the parameters, one of the trees gives the shortest paths from the source to all the other nodes of the graph when the weights are computed using this valuation.
Revealing the power of nondeterministic computation and co-nondeterministic computation is one of the central problems in computational complexity. In this paper, we consider the two computation and deterministic computation in Boolean circuits. We give the first separations on the power of deterministic circuits, nondeterministic circuits, and co-nondeterministic circuits in general circuits. More precisely, we prove the following facts.
We study aperiodic balanced sequences over finite alphabets. A sequence \(\mathbf {v}\) of this type is fully characterised by a Sturmian sequence \(\mathbf {u}\) and two constant gap sequences \(\mathbf {y}\) and \(\mathbf {y}'\). We study the language of \(\mathbf {v}\), with focus on return words to its factors. We provide a uniform lower bound on the asymptotic critical exponent of all sequences \(\mathbf {v}\) arising by \(\mathbf {y}\) and \(\mathbf {y}'\). It is a counterpart to the upper bound on the least critical exponent of \(\mathbf {v}\) conjectured and partially proved recently in works of Baranwal, Rampersad, Shallit and Vandomme. We deduce a method computing the exact value of the asymptotic critical exponent of \(\mathbf {v}\) provided the associated Sturmian sequence \(\mathbf {u}\) has a quadratic slope. The method is used to compare the critical and the asymptotic critical exponent of balanced sequences over an alphabet of size \(d\le 10\) which are conjectured by Rampersad et al. to have the least critical exponent.
We address the problem of the exhaustive generation of a particular class of polyominoes, corresponding to partially directed animals with a bounded number of holes. We apply an approach based on discrete dynamical systems to develop an algorithm that generates each polyomino in constant amortized time and space O(n). By implementing the algorithm in C++ we have obtained new sequences that do not appear in the On-Line Encyclopedia of Integer Sequences.
We introduce the notion of t-approximated determinisation and the t-twinning property of weighted tree automata (\(\mathrm {WTA}\)) over the tropical semiring. We provide an algorithm that accomplishes t-approximated determinisation of an input automaton \(\mathscr {A}\), whenever it terminates. Moreover, we prove that the t-twinning property of \(\mathscr {A}\) is a sufficient condition for the termination of our algorithm. Ultimately, we show decidability of the t-twinning property for \(\mathrm {WTA}\).
The PLP conjecture for monoids states that for every monoid M, either M is universal (that is, for every language \(L \subseteq \varSigma ^*\) there is a program over M which accepts the language L) or it has the polynomial length property (that is, every program over the monoid M has an equivalent program of length \({\mathsf {poly}}(n)\)). The conjecture has been confirmed (Tesson-Therien (2001)) for the case of groups and several subclasses of aperiodic monoids such as the variety DA and the monoids divided by the monoid U. However, the case of the set of monoids divided by the monoid \(\mathsf {BA}_2\) is still open, which if resolved, confirms the conjecture for all aperiodic monoids.
We introduce the notion of group-weighted tree automata over commutative groups and characterise sequentialisability of such automata. In particular, we introduce a fitting notion for tree distance and prove the equivalence between sequentialisability, the so-called Lipschitz property, and the so-called twinning property.
Term rewriting for rational terms, i.e. infinite terms with a finite number of different subterms, has been considered e.g. in Corradini Gadducci (1998) and Aoto Ketema (2012). In this paper, we consider rational term rewriting by a set of commutativity rules i.e. rules of the form f(x,y) → f(y,x) , based on the framework of Aoto Ketema (2012). A rewrite step with a commutativity rule is specified via a regular set of redex positions, thus via a finite automaton. We present some finite automata constructions that correspond to (in particular) taking inverse rewrite steps, merging two branching rewrite steps, and merging two consecutive rewrite steps. As a corollary, we show that rational rewrite steps by the commutativity rules are closed under taking equivalence of the rewrite steps.
