Search

In this paper, we propose a canonization method for fuzzy automata, i.e., a determinization method that is able to return a minimal fuzzy deterministic automaton equivalent to the original fuzzy automaton. The canonization method is derived from the well-known Brzozowski's algorithm for ordinary nondeterministic automata. For a given fuzzy automaton A, we prove that the construction M ˆ ( r ( N ( r ( A ) ) ) ) returns a minimal fuzzy deterministic automaton equivalent to A. In that construction, r ( . ) represents the reversal of a fuzzy automaton, N ( . ) is the determinization of a fuzzy automaton based on fuzzy accessible subset construction, and M ˆ ( . ) is the determinization of a fuzzy automaton via factorization of fuzzy states which also includes a simple reduction of a particular case of proportional fuzzy states. The method is accomplished for fuzzy automata with membership values over the Godel structure (also called max-min fuzzy automata). These fuzzy automata are always determinizable and have been proved useful in practical applications.

A translated finite automaton (TFA) results from a translation of a deterministic finite automaton (DFA). A translation is based on a mapping from the alphabet of the DFA to a new alphabet, where each symbol in the original alphabet is substituted with a symbol in the new alphabet. When this substitution generates a nondeterministic automaton, the TFA may need to be determinized into an equivalent DFA. Determinization of TFAs may be useful in a variety of domains, specifically in model-based diagnosis of discrete-event systems, where large TFAs constructed by model-based reasoning are processed to perform knowledge compilation. Since, in computation time, the classical Subset Construction determinization algorithm may be less than optimal when applied to large TFAs, a conservative algorithm is proposed, called Embedded Subset Construction. This alternative algorithm updates the TFA based on the mapping of the alphabet rather than building a new DFA from scratch. This way, in contrast with Subset Construction, which performs an exhaustive processing of the TFA to be determinized, the portion of the TFA that does not require determinization is not processed. Embedded Subset Construction is sound and complete, thereby yielding a DFA that is identical to the DFA generated by Subset Construction. The benefit of using Embedded Subset Construction largely depends on the portion of the TFA that actually requires determinization. Experimental results indicate the viability of Embedded Subset Construction, especially so when large TFAs are affected by small portions of nondeterminism.

Deterministic Finite Automaton (DFA) is widely employed in performing fast regular expression matching for numerous network applications. However, constructing DFA recognizing a set of regular expressions is time-consuming especially when the set is huge. In this paper, an improved approach is introduced to accelerate DFA construction based on the hierarchical merging method. The experiments demonstrate that the improved approach proposed in this paper performs about 1.6 to 3.4 times faster than the original hierarchical merging method, and 120 to 1500 times faster than the classical subset construction algorithm.

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.

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 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.

Network intrusion detection and prevention systems commonly use regular expression (RE) signatures to represent individual security threats. While the corresponding deterministic finite state automata (DFA) for any one RE is typically small, the DFA that corresponds to the entire set of REs is usually too large to be constructed or deployed. To address this issue, a variety of alternative automata implementations that compress the size of the final automaton have been proposed such as extended finite automata (XFA) and delayed input DFA (D2 FA). The resulting final automata are typically much smaller than the corresponding DFA. However, the previously proposed automata construction algorithms do suffer from some drawbacks. First, most employ a "Union then Minimize" framework where the automata for each RE are first joined before minimization occurs. This leads to an expensive nondeterministic finite automata (NFA) to DFA subset construction on a relatively large NFA. Second, most construct the corresponding large DFA as an intermediate step. In some cases, this DFA is so large that the final automaton cannot be constructed even though the final automaton is small enough to be deployed. In this paper, we propose a "Minimize then Union" framework for constructing compact alternative automata focusing on the D2 FA. We show that we can construct an almost optimal final D2 FA with small intermediate parsers. The key to our approach is a space-and time-efficient routine for merging two compact D2 FA into a compact D2 FA. In our experiments, our algorithm runs on average 155 times faster and uses 1500 times less memory than previous algorithms. For example, we are able to construct a D2 FA with over 80 000 000 states using only 1 GB of main memory in only 77 min.

Deterministic finite automatons (DFAs) and nondeterministic finite automatons (NFAs) are two typical automatons used in the network intrusion detection system. Although they both perform regular expression matching, they have quite different performance and memory usage properties. DFAs provide fast and deterministic matching performance but suffer from the well-known state explosion problem. NFAs are compact, but their matching performance is unpredictable and with no worst case guarantee. In this paper, we propose a new automaton representation of regular expressions, called tunable finite automaton (TFA), to deal with the DFAs' state explosion problem and the NFAs' unpredictable performance problem. Different from a DFA, which has only one active state, a TFA allows multiple concurrent active states. Thus, the total number of states required by the TFA to track the matching status is much smaller than that required by the DFA. Different from an NFA, a TFA guarantees that the number of concurrent active states is bounded by a bound factor b that can be tuned during the construction of the TFA according to the needs of the application for speed and storage. Simulation results based on regular expression rule sets from Snort and Bro show that, with only two concurrent active states, a TFA can achieve significant reductions in the number of states and memory usage, e.g., a 98% reduction in the number of states and a 95% reduction in memory space.

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.

It is proved that for each nondeterministic ordinal automaton there exists a deterministic ordinal automaton which is equivalent to the original one for all countable ordinals. An upper bound for the number of states of the deterministic automaton is double exponential in the number of states of the nondeterministic automaton.

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.

We present schemes of deterministic finite automata such that, for every nontrivial automaton A resulting from the scheme with n states, the state complexity of the mirror image of the language L(A) equals 2n. The construction leads to cases, where the increase in complexity is maximal in the transition from nondeterministic devices to deterministic ones. We also discuss the crucial importance of the size of the alphabet and present some open problems.

In an earlier paper, the author used derivatives to construct a deterministic automaton recognizing the language defined by an ω-regular expression. The construction was related to a determinization method invented by Safra. This paper describes a new construction, inspired by Piterman's improvement to Safra's method. It produces an automaton with fewer states. In addition, the presentation and proofs are simplified by going via a nondeterministic automaton having derivatives as states.

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.

A number α, in the range from n to 2n, is magic for n with respect to a given alphabet size s, if there is no minimal nondeterministic finite automaton of n states and s input symbols whose equivalent minimal deterministic finite automaton has α states. We show that in the case of a ternary alphabet, there are no magic numbers. For all n and α satisfying n ⩽ α ⩽ 2n, we define an n-state nondeterministic finite automaton with a three-letter input alphabet that requires exactly α deterministic states.

This paper introduces a compiler technology based approach to model and simulate finite automata for pedagogical purposes. The compiler technology helps to define a language to formally model finite automata and to develop a toolkit to simulate them efficiently. The language is called Finite Automaton Description Language (FADL) and the toolkit is based on it. A fast single-pass compiler is used to compile a finite automaton defined in FADL. Then an interpreter is used to simulate the working of the compiled finite automaton for any input string. The nondeterminism of a Nondeterministic Finite Automaton (NFA) is simulated using backtracking. A tool to view the transition diagram of the finite automaton is provided. A Deterministic Finite Automaton (DFA) can be additionally compiled using an optimizing compiler that also minimizes the number of states. Tools for converting an NFA to a DFA and for converting a DFA to a Turing machine are also provided. A preliminary testing of the toolkit has been performed in which the participating students observed that the toolkit is an interesting teaching tool and it helped them to acquire a better perception about finite automata. © 2010 Wiley Periodicals, Inc. Comput Appl Eng Educ 21: 467–474, 2013

In this paper we consider algorithms which allow one to combine several states of a nondeterministic finite automaton into one state. Along with the algorithms for combining states, we adduce one more algorithm for the equivalent transformation of a non-deterministic finite automaton, namely, an algorithm for adding cycles. Problems under consideration imply the development of robust computer programs.

We present a tight time-hierarchy theorem for nondeterministic cellular automata by using a recursive padding argument. It is shown that, if t2(n) is a time-constructible function and t2(n) grows faster than t1(n + 1), then there exists a language which can be accepted by a t2(n)-time nondeterministic cellular automaton but not by any t1(n)-time nondeterministic cellular automaton.

The automaton programming technology is a modern Russian development, which is actively studied and supported by a number of Russian research groups. In the automaton approach to the program design and construction, the program is divided into two—systemindependent and system-dependent—parts. The former part implements logic of the program and is given by a system of the interacting Moore‐Mealy automata. The design of each automaton consists in the creation of a link scheme describing its interface and a transition graph determining its behavior by a verbal description of the desired automaton (declaration of purposes). Given these two documents, a program module corresponding to the automaton can formally and isomorphically be constructed (after which its system-dependent part can be implemented). The automaton programming does not depend on

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.

ProofChecker is a graphical program based on the notion of formal correctness proofs that allows students, both sighted and visually impaired, to draw a deterministic finite automaton (DFA) and determine whether or not it correctly recognizes a given language. Sighted students use the mouse and graphical controls to draw and manipulate the DFA. Keyboard shortcuts, together with the use of a screen reader to voice the accessible descriptions provided by the program, allow visually impaired students to do the same. Because the states of a DFA partition thelanguage over its alphabet into equivalence classes, each state has a language associated with it. Conditions that describe the language of each state are entered by the student in the form of conditional expressions with function calls and/or regular expressions. A brute-force approach is then used to check that each state's condition correctly describes all of the strings in its language and that none of the strings in a state's language meet the condition for another state. Feedback is provided that either confirms that the DFA correctly meets thegiven conditions or alerts the student to a mismatch between the conditions and the DFA. A student's DFA can be saved in an XML file and submitted for grading. An automated checking tool, known as ProofGrader, can be used to compare a student's DFA with the correct DFA for a given language, thus greatly speeding up the grading of student assignments.

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.

Recently there have been increasing research interests on regular expression matching for its widely application in network systems to recognize predefined signatures in suspicious network traffic. Deterministic Finite Automaton (DFA) is the basic data structure for regular expression matching. Though DFA satisfies the need of real-time processing of network traffic in on-line systems, the construction of DFA is very time-consuming that prevents it from being applied on large sets of signature. In this article, we propose two approaches to parallelize the traditional sequential subset construction algorithm, which is used to convert a non-deterministic finite automaton (NFA) to an equivalent DFA, in order to accelerate DFA construction. The first proposed algorithm PRW is based on fine-grained locks on shared data structures to ensure multiple worker threads construct a DFA in parallel safely. The second proposed algorithm ARW splits the read and write accesses on shared data structures, and distributes the read operations and write operations to the multi-thread stage and the single-thread stage respectively. Experiment demonstrates the efficiency of our algorithms on real signatures of open source systems, and the speed-up ratio of PRW and ARW is up to 1.72 and 2.71 respectively with 4 worker threads.

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.

We present a tableau-based algorithm for obtaining a Buchi automaton from a formula in Dynamic Linear Time Temporal Logic (DLTL), a logic which extends LTL by indexing the until operator with regular programs. The construction of the states of the automaton is similar to the standard construction for LTL, but a different technique must be used to verify the fulfillment of until formulas. The resulting automaton is a Buchi automaton rather than a generalized one. The construction can be done on-the-fly, while checking for the emptiness of the automaton. We also extend the construction to the Product Version of DLTL.

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.

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.

In this paper the concept of substitution property (SP) partition for a finite fuzzy automaton is formulated, and the quotient automaton with respect to an SP partition is defined. The state minimization problem for such automata by using the method of quotient machines is solved.

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.

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.

There are three classical algorithms to compute a finite automaton from a regular expression. The Brzozowski algorithm yields a deterministic automaton, the Glushkov algorithm a nondeterministic one, and the general step by step method generally yields a NFA with e-transitions. Berry and Sethi have adapted Brzozowski's algorithm to compute the Glushkov automaton of an expression. We describe a variant of the step by step construction which associates standard and trim automata to regular languages. We show that the automaton constructed by the variant and the Glushkov automaton (computed by Berry-Sethi algorithm) are isomorphic.

The algorithmic approach to the design of fault-detection experiments for testing of control devices requires a mathematical model that describes the behavior of the tested device and its reference model. A finite automaton usually provides a suitable mathematical model. The classical problem assumes that the reference model and the tested device behave as a deterministic f'mite automaton (in what follows, we use the term "automaton" for a deterministic f'mite automaton). The class of faults is limited to faults that do not increase the number of automaton states. It is also assumed that the experimenter has direct access to the inputs and outputs of the device being tested. The construction of multiple fault-detection experiments assumes the existence of an input symbol that allows the model automaton to return from any state to some fixed (initial) state. This special symbol remains a reset symbol under all faults [1]. Recent studies use a nondeterministic automaton (nd-automaton) as a reference model for testing. In particular, an ndautomaton is used to construct test cases that check computer network protocols for conformity [2-4]. It has been shown [5] that if the output of the device being tested is observable only on the output of another device, then a fault,detection experiment also can be constructed using a nondeterministic model. The construction of a fault-detection experiment usually focuses mainly on the design of input sequences. The set of admissible output responses is identified with the entire set of model output sequences. In this article we analyze the possibility of reducing the length of the fault-detection experiment by reducing the set of admissible output responses. The article is organized as follows. Section 1 introduces the main def'mitions and notation. Section 2 describes the possibility of reducing the admissible set of output sequences in a fault-detection experiment. Section 3 provides necessary and sufficient conditions for the realization of a nondeterministic automaton by a deterministic automaton. We examine the conditions that permit passing from the nd-automaton P to an nd-automaton P,~ with fewer states and fewer output responses. The set of automata realizing P is identical with the set of automata realizing P~.. We can thus construct a fault~etection experiment for the nd-automaton P based on the nd-automaton P~.. This possibility is illustrated in Section 4.

We propose a practical technique to compile pattern-matching of prioritised overlapping patterns in equational languages to an minimal deterministic left-to-right matching automaton. First, we present a method to construct a tree matching automaton for such patterns. The automaton obtained allows pattern-matching to be performed without any backtracking. Although this automaton is efficient since it avoids symbol re-examination, it can only achieve this at the cost of increased space requirements. Such space requirements could be minimised by using a dag automaton that shares all the isomorphic subautomata which are duplicated in a tree automaton. We design an efficient method to identify such subautomata and avoid their construction while generating the dag automaton. This is achieved without constructing the tree automaton first.

In this paper, Nondeterministic Buchi Automata (NBA) are equivalently transformed as a new kind of deterministic omega automata, Deterministic Partitioned Automata (DPA). Different from the existing automata, at most three different transitions may occur between two states of a DPA. This leads to a determinization construction of NBA with smaller state complexity but larger transition complexity. Compared with the existing determinization constructions of NBA, the new one is intuitive and easily implementable since it is completely based on subset construction. In addition, we have proved that both nondeterministic and deterministic partitioned automata share the same expressive power with NBA.

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.

For a finite automaton, regardless whether it is deterministic or nondeterministic, Brzozowski's minimization algorithm computes the equivalent minimal deterministic finite automaton by applying reversal and power-set construction twice. Although this is an exponential algorithm because of the power-set construction, it performs well in experimental studies compared to efficient O(nlogn) minimization algorithms. Here we show how to slightly enhance Brzozowski's minimization algorithm by some sort of reachability information so that it can be applied to the following automata models: deterministic cover automata, almost equivalent deterministic finite state machines, and k-similar automata.

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.

Modeling the morphological structure of natural languages in terms of a nondeterministic finite-state automaton is shown to be inadequate in its handling of some common natural language phenomena. We show that a two-tape nondeterministic automaton is capable of handling these phenomena. The modeling is improved by the specification of a new type of automaton, the preset two-head automaton, which we argue is equivalent in expressive power to a linear context-free grammar. We discuss the operation of a parser which implements the improved model.

The present article is a continuation of a series of studies on functional synthesis of automata from their logical specifications. A specification language L based on the logic of one-place predicates interpreted on the set of integers has been described. A specification S in this language defines the class K(S) of equivalent nondeterministic automata. If S is treated as a specification of deterministic automata, then the class of all automata satisfying the specification S is identical with the class of all determinizations of any automaton from K(S). The problem of functional synthesis of a deterministic automaton specified in the language L involves constructing a procedural representation of the automaton (i.e., a representation in terms of states and transition and output functions) that satisfies the original specification. It thus includes the construction of one or several determinizations of an automaton from the class K(S). The last problem can be solved either on the procedural level (i.e., the level of the automaton graph) by constructing a procedural representation of an automation from K(S) or on the logical level (i.e., the level of formulas in the language L). In this article, we propose a solution of the problem based on the methodology ofmore » verification design of automaton. An essential feature of this methodology is that all transformations of the automaton being designed (except the construction of a procedural representation of the automaton) are carried out on the level of specification language formulas. This permits using logic methods to verify the correctness of the applied by the designer in the process of design. The problem is accordingly formulated as follows: given the specification S, constructed a specification S such that K(S{sup *}) is a class of equivalent deterministic automata that are determinizations of automata from K(S).« less

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.

A problem in the control of automata on infinite strings is defined and analyzed. The key to the investigation is the development of a fixpoint characterization of the "controllability subset" of a deterministic Rabin automaton, the set of states from which the automaton can be controlled to the satisfaction of its own acceptance condition. The fixpoint representation allows straightforward computation of the controllability subset and the construction of a suitable state-feedback control for the automaton. The results have applications to control synthesis, automaton synthesis, and decision procedures for logical satisfiability; in particular, they represent a direct, efficient and natural solution to Church's problem, the construction of winning strategies for two-player zero-sum $\omega$-regular games of perfect information, and the emptiness problem for automata on infinite trees.

We present a new incremental algorithm for minimising deterministic finite automata. It runs in quadratic time for any practical application and may be halted at any point, returning a partially minimised automaton. Hence, the algorithm may be applied to a given automaton at the same time as it is processing a string for acceptance. We also include some experimental comparative results.

We solve the open problems of translating, when possible, all common classes of nondeterministic word automata to deterministic and nondeterministic co-Buchi word automata. The handled classes include Buchi, parity, Rabin, Streett and Muller automata. The translations follow a unified approach and are all asymptotically tight. The problem of translating Buchi automata to equivalent co-Buchi automata was solved in [2], leaving open the problems of translating automata with richer acceptance conditions. For these classes, one cannot easily extend or use the construction in [2]. In particular, going via an intermediate Buchi automaton is not optimal and might involve a blow-up exponentially higher than the known lower bound. Other known translations are also not optimal and involve a doubly exponential blow-up. We describe direct, simple, and asymptotically tight constructions, involving a 2Θ(n) blow-up. The constructions are variants of the subset construction, and allow for symbolic implementations. Beyond the theoretical importance of the results, the new constructions have various applications, among which is an improved algorithm for translating, when possible, LTL formulas to deterministic Buchi word automata.

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. In this paper we propose an algorithm that is a variant of Brzozowski's algorithm in the sense that it is essentially structured as reverse operation and subset construction performed twice.

In this paper, we propose a regular expression matching circuit based on a decomposed automaton. To implement a regular expression matching circuit, first, we convert regular expressions into a non-deterministic finite automaton (NFA). Then, to reduce the number of states, we convert the NFA into a modular non-deterministic finite automaton with unbounded string transition (MNFAU). Next, to realize it by a feasible amount of hardware, we decompose the MNFAU into the deterministic finite automaton (DFA) and the 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.

Using the notion of progress measures, we discuss verification methods for proving that a program satisfies a property specified by an automaton having finite nondeterminism. Such automata can express any safety property. Previous methods, which can be derived from the method presented here, either rely on transforming the program or are not complete. In contrast, our ND progress measures describe a homomorphism from the unaltered program to a canonical specification automaton and constitute a complete verification method. The canonical specification automaton is obtained from the classical subset construction and a new subset construction, called historization.

Coalgebra is an abstract framework for the uniform study of different kinds of dynamical systems. An endofunctor $F$ determines both the type of systems ($F$-coalgebras) and a notion of behavioral equivalence ($\sim_F$) amongst them. Many types of transition systems and their equivalences can be captured by a functor $F$. For example, for deterministic automata the derived equivalence is language equivalence, while for non-deterministic automata it is ordinary bisimilarity. The powerset construction is a standard method for converting a nondeterministic automaton into an equivalent deterministic one as far as language is concerned. In this paper, we lift the powerset construction on automata to the more general framework of coalgebras with structured state spaces. Examples of applications include partial Mealy machines, (structured) Moore automata, and Rabin probabilistic automata.

Coalgebra is an abstract framework for the uniform study of different kinds of dynamical systems. An endofunctor $F$ determines both the type of systems ($F$-coalgebras) and a notion of behavioral equivalence ($\sim_F$) amongst them. Many types of transition systems and their equivalences can be captured by a functor $F$. For example, for deterministic automata the derived equivalence is language equivalence, while for non-deterministic automata it is ordinary bisimilarity. The powerset construction is a standard method for converting a nondeterministic automaton into an equivalent deterministic one as far as language is concerned. In this paper, we lift the powerset construction on automata to the more general framework of coalgebras with structured state spaces. Examples of applications include partial Mealy machines, (structured) Moore automata, and Rabin probabilistic automata.