Search

A mutating finite automaton (MFA) is a nondeterministic finite automaton (NFA) which changes its morphology over discrete time by a sequence of mutations, one mutation at each time instant. A mutation involves the insertion and/or removal of a set of states and/or transitions. This results in a sequence of NFAs, one mutated NFA for each mutation. Some application domains, including model-based diagnosis and monitoring of active systems in artificial intelligence and model-based testing in software engineering, require online determinization of MFAs. Determinizing an MFA online means generating a deterministic finite automaton (DFA) as soon as a mutation occurs, which is equivalent to the mutated NFA. Since the classical Subset Construction determinization algorithm may be inadequate for MFAs, a conservative algorithm is proposed, called Subset Restructuring, that generates the new DFA by restructuring the previous DFA based on the mutation occurred, instead of building it from scratch. Experimental results indicate the effectiveness of the approach, especially so when large MFAs change in time by small mutations.

In this work we present the algorithms to produce deterministic finite automaton (DFA) for extended operators in regular expressions like intersection, subtraction and complement. The method like “overriding” of the source NFA(NFA not defined) with subset construction rules is used. The past work described only the algorithm for AND-operator (or intersection of regular languages); in this paper the construction for the MINUS-operator (and complement) is shown.

Given a strong bimonoid P, we introduce three different behaviors of a weighted finite automaton over P (called a P − valued finite automaton), named the initial object semantics, final object semantics and run semantics. We define four forms for a P − valued nondeterministic finite automaton ( P − NFA) and three forms for a P − valued deterministic finite automaton ( P − DFA). Under the above-mentioned semantics, the equivalence and differences among the four forms of P − NFAs are discussed and the equivalence among the three forms of P − DFAs are given. Moreover, we show that some equivalence depends on right distributivity or left distributivity, or even requires P to degenerate into a semiring.

Let $S$ be a string of length $n$ with characters from an alphabet of size $\sigma$. The \emph{subsequence automaton} of $S$ (often called the \emph{directed acyclic subsequence graph}) is the minimal deterministic finite automaton accepting all subsequences of $S$. A straightforward construction shows that the size (number of states and transitions) of the subsequence automaton is $O(n\sigma)$ and that this bound is asymptotically optimal. In this paper, we consider subsequence automata with \emph{default transitions}, that is, special transitions to be taken only if none of the regular transitions match the current character, and which do not consume the current character. We show that with default transitions, much smaller subsequence automata are possible, and provide a full trade-off between the size of the automaton and the \emph{delay}, i.e., the maximum number of consecutive default transitions followed before consuming a character. Specifically, given any integer parameter $k$, $1 < k \leq \sigma$, we present a subsequence automaton with default transitions of size $O(nk\log_{k}\sigma)$ and delay $O(\log_k \sigma)$. Hence, with $k = 2$ we obtain an automaton of size $O(n \log \sigma)$ and delay $O(\log \sigma)$. On the other extreme, with $k = \sigma$, we obtain an automaton of size $O(n \sigma)$ and delay $O(1)$, thus matching the bound for the standard subsequence automaton construction. Finally, we generalize the result to multiple strings. The key component of our result is a novel hierarchical automata construction of independent interest., Comment: Corrected typos

The classical subset construction for non-deterministic automata can be generalized to other side-effects captured by a monad. The key insight is that both the state space of the determinized automaton and its semantics---languages over an alphabet---have a common algebraic structure: they are Eilenberg-Moore algebras for the powerset monad. In this paper we study the reverse question to determinization. We will present a construction to associate succinct automata to languages based on different algebraic structures. For instance, for classical regular languages the construction will transform a deterministic automaton into a non-deterministic one, where the states represent the join-irreducibles of the language accepted by a (potentially) larger deterministic automaton. Other examples will yield alternating automata, automata with symmetries, CABA-structured automata, and weighted automata.

For each regular language L we describe a family of canonical nondeterministic acceptors (nfas). Their construction follows a uniform recipe: build the minimal dfa for L in a locally finite variety V , and apply an equivalence between the category of finite V -algebras and a suitable category of finite structured sets and relations. By instantiating this to different varieties, we recover three well-studied canonical nfas: V = boolean algebras yields the atomaton of Brzozowski and Tamm, V = semilattices yields the jiromaton of Denis, Lemay and Terlutte, and V = Z 2 -vector spaces yields the minimal xor automaton of Vuillemin and Gama. Moreover, we obtain a new canonical nfa called the distromaton by taking V = distributive lattices. Each of these nfas is shown to be minimal relative to a suitable measure, and we derive sufficient conditions for their state-minimality. Our approach is coalgebraic, exhibiting additional structure and universal properties of the canonical nfas.

Finite automata are exploited in several domains, including language processing, artificial intelligence, automatic control, and software engineering. Let \({\mathcal {N}}\) be a nondeterministic finite automaton (NFA) and \({\mathcal {D}}\) the deterministic finite automaton (DFA) equivalent to \({\mathcal {N}}\). Assume to decrement \({\mathcal {N}}\) by \(\varDelta {\mathcal {N}}\), thus obtaining the decremented NFA \({\mathcal {N}}' = {\mathcal {N}}\setminus \varDelta {\mathcal {N}}\), where some states and/or transitions are missing. Consider determinizing \({\mathcal {N}}'\). Instead of determinizing \({\mathcal {N}}'\) from scratch using the classical Subset Construction algorithm, we propose Decremental Subset Construction, an algorithm which generates the DFA \({\mathcal {D}}'\) equivalent to \({\mathcal {N}}'\) by updating \({\mathcal {D}}\) based on \({\mathcal {N}}\) and \(\varDelta {\mathcal {N}}\). This way, only the actions necessary to transform \({\mathcal {D}}\) into \({\mathcal {D}}'\) are applied. Although evidence from worst-case complexity analysis indicates that Decremental Subset Construction is not better than Subset Construction, in practice, when \({\mathcal {N}}\) is large and \(\varDelta {{\mathcal {N}}}\) relatively small, Decremental Subset Construction may outperform Subset Construction significantly.

Refinement checking answers the question on whether an implementation model is a refinement of a specification model, which is of great value for system verification. Some refinement relationships, e.g., trace refinement and failures/divergence refinement, have been recognized for different verification purposes. In general, refinement checking algorithms often rely on subset construction, which incurs in the state space explosion problem. Recently the anti-chain based approach has been suggested for trace refinement checking, and the results show a significant improvement. In this paper, we investigate the problems of applying the anti-chain approach to timed refinement checking (a timed implementation vs. a timed or untimed specification) and probabilistic refinement checking (a probabilistic implementation vs. a non-probabilistic specification), and show that the state space can be reduced considerably by employing the anti-chain approach. All the algorithms have been integrated into the model checking tool PAT, and the experiments have been conducted to show the efficiency of the application of anti-chains.

For the past time a number of algorithms were presented to produce a deterministic finite automaton (DFA) for the regular expression. These algorithms could be divided into what they used as an initial data from which to produce DFA. The method to produce DFA from non-deterministic finite automaton (NFA) by a subset construction could be generalized for extended regular expressions, including intersection, negation and subtraction of the regular languages. In this article the modified algorithm of subset construction is presented; this algorithm produces a unigram DFA for the regular expression with extensions (specifically AND-operator). General Terms Pattern Recognition; Finite Automata; Algorithms.

We revisit the problem of deciding by means of a finite automaton whether a string is uniquely decodable from its bigram counts. An efficient algorithm for constructing a polynomial-size Nondeterministic Finite Automaton (NFA) that decides unique decodability is given. This NFA may be simulated efficiently in time and space. Conversely, we show that the minimum deterministic finite automaton for deciding unique decodability has exponentially many states in alphabet size, and compute the correct order of magnitude of the exponent.

Recent studies on fuzzy automata are influenced by algebraic techniques to tackle issues like reduction, minimization and their languages. Fuzzy automaton homomorphism is one such majorally discussed technique. This paper is concerned with the group of (weak) fuzzy automaton automorphisms and constructions of all (weak) fuzzy automaton automorphisms over arbitrary fuzzy automaton. It is shown that (1) every arbitrary fuzzy automaton is decomposed into distinct primaries, (2) primaries are maximal singly generated fuzzy automata and (3) every weak fuzzy automaton homomorphism on an arbitrary fuzzy automaton is uniquely determined into weak fuzzy automaton homomorphisms on all its primaries. Therefore, the discussion begun over strongly connected fuzzy automaton and continue constructions as well as characterizations of (weak) fuzzy automaton homomorphisms, isomorphisms, endomorphisms and automorphisms sequentially over perfect fuzzy automaton, singly generated fuzzy automaton and primaries of fuzzy automaton. Finally, it is obtained that the group of weak fuzzy automaton automorphisms and its cardinality over arbitrary fuzzy automaton.

Every regular expression can be transformed into a Nondeterministic Finite Automaton (NFA) with or without  transitions. A well known algorithm called subset construction technique is used for conversion of NFA into DFA. In this paper, initially, the construction of the position automaton is given for the same. Also, the algorithm to convert this Position Automaton into DFA using subset construction technique is discussed. AMS MSC2010 Certification: 68Q45, 68Q70

A nondeterministic weighted finite automaton (WFA) maps an input word to a numerical value. Applications of weighted automata include formal verification of quantitative properties, as well as text, speech, and image processing. Many of these applications require the WFAs to be deterministic, or work substantially better when the WFAs are deterministic. Unlike NFAs, which can always bedeterminized, not all WFAs have an equivalent deterministic weighted automaton (DWFA). In \cite{Moh97}, Mohri describes a determinization construction for a subclass of WFA. He also describes a property of WFAs (the {\em twins property}), such that all WFAs that satisfy thetwins property are determinizable and the algorithm terminates on them. Unfortunately, many natural WFAs cannot be determinized. In this paper we study {\em approximated determinization\/} of WFAs. We describe an algorithm that, given a WFA $\A$ and an approximation factor $t \geq 1$, constructs a DWFA $\A'$ that{\em $t$-determinizes\/} $\A$. Formally, for all words $w \in \Sigma^*$, the value of $w$ in $\A'$ is at least its value in $\A$ and at most $t$times its value in $\A$. Our construction involves two new ideas:attributing states in the subset construction by both upper and lower residues, and collapsing attributed subsets whose residues can be tightened. The larger the approximation factor is, the more attributed subsets we can collapse. Thus, $t$-determinization is helpful not only for WFAs that cannot be determinized, but also in cases determinization is possible but results in automata that are too big to handle. In addition, $t$-determinization is useful for reasoning about the competitive ratio of on line algorithms. We also describe a property (the {\em $t$-twins property}) and use it in order to characterize $t$-determinizable WFAs. Finally, we describea polynomial algorithm for deciding whether a given WFA has the $t$-twins property.

Deep packet inspection, in which packet payloads are matched against a large set of patterns, is an important algorithm in many networking applications. Nondeterministic Finite Automaton (NFA) and Deterministic Finite Automaton (DFA) are the basis of existing algorithms. However, both NFA and DFA are not ideal for real-world rule sets: NFA has the minimum storage, but the maximum memory bandwidth; while DFA has the minimum memory bandwidth, but the maximum storage. Specifically, NFA and DFA cannot handle the presence of character sets, wildcards, and repetitions of character sets or wildcards in real-world rule sets. In this paper, we propose and evaluate a dual Finite Automaton (dual FA) to address these shortcomings. The dual FA consists of a linear finite automaton (LFA) and an extended deterministic finite automaton (EDFA). The LFA is simple to implement, and it provides an alternative approach to handle the repetition of character sets and wildcards (which could otherwise cause the state explosion problem in a DFA) without increasing memory bandwidth. We evaluate the automaton in real-world rule sets using different synthetic payload streams. The results show that dual FA can reduce the number of states up to five orders of magnitude while their memory bandwidth is close to minimum.

Regular expression matching is the state of the art in signature based intrusion detection systems. A regular expression matching algorithm used in intrusion detection systems is expected to process data at a speed linear in size of the incoming data and also to be able to run on network devices with limited memory. Traditional DFA and NFA based algorithms fail to meet either of these two requirements. The existing techniques try to either modify a DFA or a NFA, or combine both these to find a trade off between speed and memory requirements. The idea we propose in this paper is orthogonal to existing techniques. We propose a new approach to store a finite automaton in memory which otherwise is stored as a transition table. Our approach can be used by existing algorithms to further reduce the memory requirements with a minimal increase in the processing speed.

We exhibit the construction of a deterministic automaton that, given k > 0, recognizes the (regular) language of k-differentiable words. Our approach follows a scheme of Crochemore et al. based on minimal forbidden words. We extend this construction to the case of C\infinity-words, i.e., words differentiable arbitrary many times. We thus obtain an infinite automaton for representing the set of C\infinity-words. We derive a classification of C\infinity-words induced by the structure of the automaton. Then, we introduce a new framework for dealing with \infinity-words, based on a three letter alphabet. This allows us to define a compacted version of the automaton, that we use to prove that every C\infinity-word admits a repetition in C\infinity whose length is polynomially bounded., Comment: Accepted for publication

SUMMARY This paper shows a design method for a regular expression matching circuit based on a decomposed automaton. To implement a regular expression matching circuit, first, we convert a regular expression into a non-deterministic finite automaton (NFA). Then, to reduce the number of states, we convert the NFA into a merged-states non-deterministic finite automaton with unbounded string transition (MNFAU) using a greedy algorithm. Next, to realize it by a feasible amount of hardware, we decompose the MNFAU into a deterministic finite automaton (DFA) and an NFA. The DFA part is implemented by an off-chip memory and a simple sequencer, while the NFA part is implemented by a cascade of logic cells. Also, in this paper, we show that the MNFAU based implementation has lower area complexity than the DFA and the NFA based ones. Experiments using regular expressions form SNORT shows that, as for the embedded memory size per a character, the MNFAU is 17.17-148.70 times smaller than DFA methods. Also, as for the number of LCs (Logic Cells) per a character, the MNFAU is 1.56-5.12 times smaller than NFA methods. This paper describes detail of the MEMOCODE2010 HW/SW co-design contest for which we won the first place award.

Deterministic finite automata (DFAs) are constructed for various purposes in computational biology. Little attention, however, has been given to the efficient construction of minimal DFAs. In this article, we define simple non-deterministic finite automata (NFAs) and prove that the standard subset construction transforms NFAs of this type into minimal DFAs. Furthermore, we show how simple NFAs can be constructed from two types of pattern popular in bioinformatics, namely (sets of) generalized strings and (generalized) strings with a Hamming neighborhood.

We present the first (polynomial-time) algorithm for reducing a given deterministic finite state automaton (DFA) into a hyper-minimized DFA, which may have fewer states than the classically minimized DFA. The price we pay is that the language recognized by the new machine can differ from the original on a finite number of inputs. These hyper-minimized automata are optimal, in the sense that every DFA with fewer states must disagree on infinitely many inputs. With small modifications, the construction works also for finite state transducers producing outputs. Within a class of finitely differing languages, the hyper-minimized automaton is not necessarily unique. There may exist several non-isomorphic machines using the minimum number of states, each accepting a separate language finitely-different from the original one. We will show that there are large structural similarities among all these smallest automata.

We propose a novel approach for coping with alternating quantification as the main source of nonelementary complexity of deciding WS1S formulae. Our approach is applicable within the state-of-the-art automata-based WS1S decision procedure implemented, e.g. in MONA. The way in which the standard decision procedure processes quantifiers involves determinization, with its worst case exponential complexity, for every quantifier alternation in the prefix of a formula. Our algorithm avoids building the deterministic automata---instead, it constructs only those of their states needed for (dis)proving validity of the formula. It uses a symbolic representation of the states, which have a deeply nested structure stemming from the repeated implicit subset construction, and prunes the search space by a nested subsumption relation, a generalization of the one used by the so-called antichain algorithms for handling nondeterministic automata. We have obtained encouraging experimental results, in some cases outperforming MONA by several orders of magnitude., Comment: Accepted to TACAS'15

We propose a novel approach for coping with alternating quantification as the main source of nonelementary complexity of deciding WS1S formulae. Our approach is applicable within the state-of-the-art automata-based WS1S decision procedure implemented, e.g. in MONA. The way in which the standard decision procedure processes quantifiers involves determinization, with its worst case exponential complexity, for every quantifier alternation in the prefix of ai¾?formula. Our algorithm avoids building the deterministic automata--instead, it constructs only those of their states needed for disproving validity of the formula. It uses a symbolic representation of the states, which have a deeply nested structure stemming from the repeated implicit subset construction, and prunes the search space by a nested subsumption relation, a generalization of the one used by the so-called antichain algorithms for handling nondeterministic automata. We have obtained encouraging experimental results, in some cases outperforming MONA by several orders of magnitude.

Hereditarily finite (HF) set theory provides a standard universe of sets, but with no infinite sets. Its utility is demonstrated through a formalisation of the theory of regular languages and finite automata, including the Myhill-Nerode theorem and Brzozowski’s minimisation algorithm. The states of an automaton are HF sets, possibly constructed by product, sum, powerset and similar operations.

We propose to harness Angluin’s \(L^*\) algorithm for learning a deterministic finite automaton that describes the possible scenarios under which a given program error occurs. The alphabet of this automaton is given by the user (for instance, a subset of the function call sites or branches), and hence the automaton describes a user-defined abstraction of those scenarios. More generally, the same technique can be used for visualising the behavior of a program or parts thereof. This can be used, for example, for visually comparing different versions of a program, by presenting an automaton for the behavior in the symmetric difference between them, or for assisting in merging several development branches. We present initial experiments that demonstrate the power of an abstract visual representation of errors and of program segments.

We introduce and study three notions of typeness for automata on infinite words. For an acceptance-condition class γ (that is, γ is weak, Büchi, co-Büchi, Rabin, or Streett), deterministic γ-typeness asks for the existence of an equivalent γ-automaton on the same deterministic structure, nondeterministic γ-typeness asks for the existence of an equivalent γ-automaton on the same structure, and γ-powerset-typeness asks for the existence of an equivalent γ-automaton on the (deterministic) powerset structure – one obtained by applying the subset construction. The notions are helpful in studying the complexity and complication of translations between the various classes of automata. For example, we prove that deterministic Büchi automata are co-Büchi type; it follows that a translation from deterministic Büchi to deterministic co-Büchi automata, when exists, involves no blow up. On the other hand, we prove that nondeterministic Büchi automata are not co-Büchi type; it follows that a translation from a nondeterministic Büchi to nondeterministic co-Büchi automata, when exists, should be more complicated than just redefining the acceptance condition. As a third example, by proving that nondeterministic co-Büchi automata are Büchi-powerset type, we show that a translation of nondeterministic co-Büchi to deterministic Büchi automata, when exists, can be done applying the subset construction. We give a complete picture of typeness for the weak, Büchi, co-Büchi, Rabin, and Streett acceptance conditions, and discuss its usefulness.

We consider control questions for finite automata viewed as input/output systems. In particular, we find estimates of the minimal number of states of an automaton able to control a given automaton. We prove that, on average, feedback closed-loop control automata do not have fewer states than open-loop control automata when the control objective is to steer the controlled automaton to a target state. We compare our approach to other ways of formalizing of formalizing analogous control objectives.

Various string matching problems can be solved by means of a deterministic finite automaton (DFA) or a non-deterministic finite automaton (NFA). In non-oblivious cases, DFAs are often preferred for their run-time efficiency despite larger sizes. In oblivious cases, however, the inevitable computation and communication costs associated with the automaton size are more favorable to NFAs. We propose oblivious protocols for NFA evaluation based on homomorphic encryption and demonstrate that our method can be orders of magnitude faster than DFA-based methods, making it applicable to real-life scenarios, such as privacy-preserving detection of viral infection using genomic data.

This paper continues the discussion of teaching nondeterminism (see [6]) where we presented a didactic approach introducing the notion of nondeterministic automata. Although in this paper we use the same methodology we have to face up to new didactic challenges. Namely, teaching the subset construction requires answers to the question how can CAS be used in teaching the different phases of mathematical problem solving so that we can reach higher cognitive efficiency.

We show that the size of a Las Vegas automaton and the size of a complete, minimal deterministic automaton accepting a regular language are polynomially related. More precisely, we show that if a regular language L is accepted by a Las Vegas automaton having r states such that the probability for a definite answer to occur is at least p , then r ≥ np , where n is the number of the states of the minimal deterministic automaton accepting L . Earlier this result has been obtained in [2] by using a reduction to one-way Las Vegas communication protocols , but here we give a direct proof based on information theory.

Part 2: Regular Contributions; International audience; For each regular language L we describe a family of canonical nondeterministic acceptors (nfas). Their construction follows a uniform recipe: build the minimal dfa for L in a locally finite variety V , and apply an equivalence between the finite V -algebras and a category of finite structured sets and relations. By instantiating this to different varieties we recover three well-studied canonical nfas (the átomaton, the jiromaton and the minimal xor automaton) and obtain a new canonical nfa called the distromaton. We prove that each of these nfas is minimal relative to a suitable measure, and give conditions for state-minimality. Our approach is coalgebraic, exhibiting additional structure and universal properties.

A cover-automaton A of a finite language L⊆Σ ∗ is a finite deterministic automaton (DFA) that accepts all words in L and possibly other words that are longer than any word in L . A minimal deterministic finite cover automaton (DFCA) of a finite language L usually has a smaller size than a minimal DFA that accept L . Thus, cover automata can be used to reduce the size of the representations of finite languages in practice. In this paper, we describe an efficient algorithm that, for a given DFA accepting a finite language, constructs a minimal deterministic finite cover-automaton of the language. We also give algorithms for the boolean operations on deterministic cover automata, i.e., on the finite languages they represent.

The aim of this paper is to investigate how subset construction performs on specific families of automata. A new upper bound on the number of states of the subset-automaton is established in the case of homogeneous automata. The complexity of the two basic steps of subset construction, i.e. the computation of deterministic transitions and the set equality tests, is examined depending on whether the nondeterministic automaton is an unrestricted one, an homogeneous one, a position one or a ZPC-structure, which is an implicit construction for a position automaton. Copyright 2001 Elsevier Science B.V.

We prove that every regular expression of size n can be converted into an equivalent nondeterministic ε-free finite automaton (NFA) with O(n(logn)2) transitions in time O(n2logn). The best previously known conversions result in NFAs of worst-case size Θ(n2). We complement our result by proving an almost matching lower bound. We exhibit a sequence of regular expressions of size O(n) and show the number of transitions required in equivalent NFAs is Ω(nlogn). This also proves there does not exist a linear-size conversion from regular expressions to NFAs.

We introduce a new class of groups with solvable word problem, namely groups specified by a confluent set of short-lex-reducing Knuth–Bendix rules which form a regular language. This simultaneously generalizes short-lex-automatic groups and groups with a finite confluent set of short-lex-reducing rules. We describe a computer program which looks for such a set of rules in an arbitrary finitely presented group. Our main theorem is that our computer program finds the set of rules, if it exists, given enough time and space. (This is an optimistic description of our result — for the more pessimistic details, see the body of the paper.) The set of rules is embodied in a finite state automaton in two variables. A central feature of our program is an operation, which we call welding, used to combine existing rules with new rules as they are found. Welding can be defined on arbitrary finite state automata, and we investigate this operation in abstract, proving that it can be considered as a process which takes as input one regular language and outputs another regular language. In our programs we need to convert several nondeterministic finite state automata to deterministic versions accepting the same language. We show how to improve somewhat on the standard subset construction, due to special features in our case. We axiomatize these special features, in the hope that these improvements can be used in other applications. The Knuth–Bendix process normally spends most of its time in reduction, so its efficiency depends on doing reduction quickly. Standard data structures for doing this can become very large, ultimately limiting the set of presentations of groups which can be so analyzed. We are able to give a method for rapid reduction using our much smaller two variable automaton, encoding the (usually infinite) regular language of rules found so far. Time taken for reduction in a given group is a small constant times the time taken for reduction in the best schemes known (see [5]), which is not too bad since we are reducing with respect to an infinite set of rules, whereas known schemes use a finite set of rules. We hope that the method described here might lead to the computation of automatic structures in groups for which this is currently infeasible. Some proofs have been omitted from this paper in the interests of brevity. Full details are provided in [4].

It is shown that if α is an integer which can be expressed as 2k or 2k+1 for some integer 0⩽k⩽n/2−2, then there exist nondeterministic finite automata with n states whose equivalent deterministic finite automata need exactly 2n−α states.

The paper discusses the problem of determinizing finite-state automata containing large numbers of ε-moves. Experiments with finite-state approximations of natural language grammars often give rise to very large automata with a very large number of ε-moves. The paper identifies and compares a number of subset construction algorithms that treat ε-moves. Experiments have been performed which indicate that the algorithms differ considerably in practice, both with respect to the size of the resulting deterministic automaton, and with respect to practical efficiency. Furthermore, the experiments suggest that the average number of ε-moves per state can be used to predict which algorithm is likely to be the fastest for a given input automaton.

International audience; The main result is a finite-state version of the Kraft-McMillan theorem characterizing the generating sequence of a k-ary regular tree. The proof uses a new contruction called the multiset construction which is a version with multiplicities of the well-known subset construction of automata theory

We survey three applications that use finite automata to specify behaviors of concurrent processes in general, and asynchronous circuits in particular. The applications are: verification of concurrent processes, liveness properties, and delay insensitivity of asynchronous networks. In all three cases, we start with a common model of a nondeterministic finite automaton, and then add certain application-specific features. Typically, the added features involve separating the alphabet or the state set of the automaton into several disjoint subsets. For each application we provide the motivation, describe the type of automaton used, define the most important operations, and state some of the key results. For process verification, we describe a BDD-based tool that implements the respective automata and operations.

We consider the problem of storing a set S⊂Σkas a deterministic finite automaton (DFA). We show that inserting a new string σ∈Σk or deleting a string from the set S represented as a minimized DFA can be done in expected time O(k|Σ|), while preserving the minimality of the DFA. The method can be applied to reduce the memory requirements of model checkers that are based on explicit state enumeration. As an example, we discuss an implementation of the method for the model checker Spin.

Infinite behavior of nondeterministic finite-state automata running over infinite trees or more generally over elements of an arbitrary algebraic structure is characterized by a calculus of fixed point terms interpreted in powerset algebras. These terms involve the least and greatest fixed point operators and disjunction as the only logical operation. A tight correspondence is established between a hierarchy of Rabin indices of automata and a hierarchy induced by alternation of the least and greatest fixed point operators. It is shown that, in the powerset algebra of trees constructed from a set of functional symbols, the fixed point hierarchy is infinite unless all the symbols are unary (i.e. trees are words). It is also shown that an interpretation of a closed fixed point term in any powerset algebra can be factorized through the interpretation of this term in the powerset algebra of trees, from which it is deduced that the question whether a term denotes always ∅ can be answered in polynomial time.

We show how to turn a regular expression R of length r into an O(s) space representation of McNaughton and Yamada's NFA, where s is the number of occurrences of alphabet symbols in R, and s + 1 is the number of NFA states. The standard adjacency list representation of McNaughton and Yamada's NFA takes up 1 + 2s + $s\sp2$ space in the worst case. The adjacency list representation of the NFA produced by Thompson takes up between 2r and 6r space, where r can be arbitrarily larger than s. Given any subset V of states in McNaughton and Yamada's NFA, our representation can be used to compute the set U of states one transition away from the states in V in optimal time O($\vert V\vert + \vert U\vert$). McNaughton and Yamada's NFA requires $\Theta$($\vert V\vert \times \vert U\vert$) time in the worst case. Using Thompson's NFA, the equivalent calculation requires $\Theta$(r) time in the worst case. An implementation of our NFA representation confirms that it takes up an order of magnitude less space than McNaughton and Yamada's machine. An implementation to produce a DFA from our NFA representation by subset construction shows linear and quadratic speedups over subset construction starting from both Thompson's and McNaughton and Yamada's NFA's. It also shows that the DFA produced from our NFA is as much as one order of magnitude smaller than DFA's constructed from the two other NFA's. An UNIX egrep compatible software called cgrep based on our NFA representation is implemented. A benchmark shows that cgrep is dramatically faster than both UNIX egrep and GNU e?grep. Throughout this thesis the importance of syntax is stressed in the design of our algorithms. In particular, we exploit a method of program improvement in which costly repeated calculations can be avoided by establishing and maintaining program invariants. This method of symbolic finite differencing has been used previously by Douglas Smith to derive efficient functional programs.

We show that Safra's determinization ofω-automata with Streett (strong fairness) acceptance condition also gives memoryless winning strategies in infinite games, for the player whose acceptance condition is the complement of the Streett condition. Both determinization and memorylessness are essential parts of known proofs of Rabin's tree automata complementation lemma. Also, from Safra's determinization construction, along with its memoryless winning strategy extension, a single exponential complementation of Streett tree automata follows. A different single exponential construction and proof first appeared in [N. Klarlund (1992), Progress measures, immediate determinacy, and a subset construction for tree automata,in“Proceedings, 7th IEEE Symposium on Logics in Computer Science”].

International audience; We study the number of states of the minimal automaton of the mirror of a rational language recognized by a random deterministic automaton with n states. We prove that, for any d > 0, the probability that this number of states is greater than nd tends to 1 as n tends to infinity. As a consequence, the generic and average complexities of Brzozowski minimization algorithm are super-polynomial for the uniform distribution on deterministic automata.

International audience; A lot of computing tools are often used for analyzing DNA se- quences like trees, automata, dictionaries, every one being re- served for a particular problem. A. Blumer and al. have proposed a more general computing tool : the smaller automaton recogniz- ing the subwords of a text (DAWG). In this paper we propose the concept of "weighted factors au- tomaton" producing every occurrence of any factor. Its transi- tions are labeled by the read letter and weighted by the set of the indices of the factors beginnings. The factors are obtained by concatenating the read letters and the indices of the factors begin- nings are obtained by computing the intersection of the weight- ing sets, when advancing from the initial state to a final state. We think that this automaton can be more easily processed than DAWG and we present a comparison between DAWG and our automaton: the set of the factors beginnings indices and the fac- tors frequency are more easily obtained by our automaton and the restriction of our automaton to the factors of length k maintains the automaton structure, when DAWG cannot be eas- ily restricted. The applications are numerous: By selecting factors of length 1 , we obtain the coding regions, factors of length 3 , we obtain the expression level of some gene. The "weighted factors au- tomaton" allows us to find matches of pattern, to study homol- ogy, FASTA and BLAST algorithms being significantly simplified.

The Rabin index of a regular language of infinite words is the minimum number of accepting pairs used in any deterministic Rabin automaton recognizing this language. We show that the Rabin index of a language given by a Muller automaton withnstates andmaccepting sets is computable in timeO(m2nc) wherecis the cardinality of the alphabet.

We first give a method for simulating, in the case of Buchi, an alternating automaton by a usual nondeterministic one. Then, to make the satisfiability problem of Linear Propositional Temporal Logic (LPTL) use this result, we give a method for translating any formula of this logic into an equivalent Buchi alternating automaton.

We introduce a notion of partial derivative of a regular expression and apply it to finite automaton constructions. The notion is a generalization of the known notion of word derivative due to Brzozowski: partial derivatives are related to non-deterministic finite automata (NFA's) in the same natural way as derivatives are related to deterministic ones (DFA's). We give a constructive definition of partial derivatives and prove several facts, in particular: 1.(1) any derivative of a regular expression r can be represented by a finite set of partial derivatives of r;2.(2) the set of all partial derivatives of r is finite and its cardinality is less than or equal to one plus the number of occurrences of letters from A appearing in r;3.(3) any partial derivative of r is either a regular unit, or a subterm of r, or a concatenation of several such subterms. These theoretical results lead us to a new algorithm for turning regular expressions into relatively small NFA's and allow us to provide certain improvements to Brzozowski's algorithm for constructing DFA's. We also report on a prototype implementation of our NFA construction and present several examples.

In this paper we present two algorithms for building lexicons in Directed Acyclic Word-Graphs (DAWGs). The two algorithms, one for deterministic and the other for non-deterministic DAWGs, can be used instead of the traditional subset construction method. Although the proposed algorithms do not produce the optimal DAWG (i.e., the one with the minimum number of states), they are simple, fast and able to build the DAWG incrementally, as new words are added to the lexicon. Thus, building large lexicons in a DAWG structure becomes an easy task, even for a modest computer.

In order to keep up with the demand for solutions to problems with ever-increasing data sets, both academia and industry have embraced commodity computer clusters with locally attached disks or SANs as an inexpensive alternative to supercomputers. With the advent of tools for parallel disks programming, such as MapReduce, STXXL and Roomy --- that allow the developer to focus on higher-level algorithms --- the programmer productivity for memory-intensive programs has increased many-fold. However, such parallel tools were primarily targeted at iterative programs.We propose a programming model for migrating recursive RAM-based legacy algorithms to parallel disks. Many memory-intensive symbolic algebra algorithms are most easily expressed as recursive algorithms. In this case, the programming challenge is multiplied, since the developer must re-structure such an algorithm with two criteria in mind: converting a naturally recursive algorithm into an iterative algorithm, while simultaneously exposing any potential data parallelism (as needed for parallel disks).This model alleviates the large effort going into the design phase of an external memory algorithm. Research in this area over the past 10 years has focused on per-problem solutions, without providing much insight into the connection between legacy algorithms and out-of-core algorithms. Our method shows how legacy algorithms employing recursion and non-streaming memory access can be more easily translated into efficient parallel disk-based algorithms.We demonstrate the ideas on a largest computation of its kind: the determinization via subset construction and minimization of very large nondeterministic finite set automata (NFA). To our knowledge, this is the largest subset construction reported in the literature. Determinization for large NFA has long been a large computational hurdle in the study of permutation classes defined by token passing networks. The programming model was used to design and implement an efficient NFA determinization algorithm that solves the next stage in analyzing token passing networks representing two stacks in series.

Moore automata represent a model that has many applications. In this paper we define a notion of coherent nondeterministic Moore automaton (NMA) and show that such a model has the same computational power of the classical deterministic Moore automaton. We consider also the problem of constructing the minimal deterministic Moore automaton equivalent to a given NMA. We propose an algorithm that is a variant of Brzozowski’s minimization algorithm in the sense that it is essentially structured as reverse operation and subset construction performed twice. Moreover, we explore more general classes of NMA and analyze the applicability of the algorithm. For some of such classes the algorithm does not return the minimal equivalent deterministic automaton.