Search

To specify properties of open systems with interval based temporal logics, Alternating Projection Temporal Logic (APTL) is proposed by introducing Concurrent Game Structures (CGS) to Propositional Projection Temporal Logic (PPTL). Further, examples are given to show how properties of open systems can be specified by APTL formulas. Moreover, to establish the automata based model theory for the new proposed logic, Generalized alternating Buchi automata over Concurrent Game structures (GBCGs) are defined, and a transformation from APTL formulas to GBCGs is presented. In addition, a decision procedure for checking the satisfiability of APTL formulas, and a model checking approach for APTL with Concurrent Game Structures (CGSs) being models are presented.

There exist undoubtedly strong links between the Burnside problem and the class of automaton groups. Indeed, many interesting examples of infinite Burnside groups are automaton groups, in particular for any prime p , there exist an infinite Burnise p -group generated by a Mealy automaton. Moreover the simplest known example of an infinite Burnside group arises in this class. However there is no known example of such a group generated by a reversible Mealy automaton. In this paper we prove that, in fact, no connected reversible Mealy automaton of prime size can generate an infinite Burnside group. In addition we explain how our method can be applied for some Mealy automata of non prime size.

A poly-slender context-free language is a context-free language whose number of words of length n is polynomially bounded. Its structure has been thoroughly characterized by Ilie, Rozenberg and Salomaa. Thanks to this characterization, we show that every poly-slender context-free language is recognizable by a trellis automaton, if the languages of words with as many a as b and at most a constant number of alternations between a and b are recognizable by trellis automata. Then we construct a family of trellis automata that recognizes such languages.

We provide an algorithm for learning an unknown regular set of infinite words, using membership and equivalence queries. Three variations of the algorithm learn three different canonical representations of omega regular languages, using the notion of families of dfas. One is of size similar to L $, a dfa representation recently learned using L* [7]. The second is based on the syntactic forc, introduced in [14]. The third is introduced herein.We show that the second can be exponentially smaller than the first, and the third is at most as large as the first two, with up to a quadratic saving with respect to the second.

This paper proposes a Canonical Form (CF) for chop formulas of Propositional Projection Temporal Logic (PPTL). Based on CF, an improved algorithm for constructing Labeled Normal Form Graph (LNFG) of a PPTL formula is presented. This improvement leads to a better decision procedure for PPTL with infinite models. In addition, a transformation from LNFGs to Generalized Buchi Automata (GBA) and then Buchi Automata (BA) is formalized. Thus, a SPIN based model checking approach is generalized for PPTL. To illustrate how these algorithms work, several examples are given.

International audience; We propose a new approach for minimizing alternating Büchi automata (ABA). The approach is based on the so called \emph{mediated equivalence} on states of ABA, which is the maximal equivalence contained in the so called \emph{mediated preorder}. Two states $p$ and $q$ can be related by the mediated preorder if there is a~\emph{mediator} (mediating state) which forward simulates $p$ and backward simulates $q$. Under some further conditions, letting a computation on some word jump from $q$ to $p$ (due to they get collapsed) preserves the language as the automaton can anyway already accept the word without jumps by runs through the mediator. We further show how the mediated equivalence can be computed efficiently. Finally, we show that, compared to the standard forward simulation equivalence, the mediated equivalence can yield much more significant reductions when applied within the process of complementing Büchi automata where ABA are used as an intermediate model.

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

To determine the structure of an automaton A, we define the layers of A, which form a poset. We show that for any finite poset P there exists an automaton whose poset of layers is isomorphic to P. All subautomata of an automaton A are characterized by the layers of A, and they form a Ps-type upper semilattice. Conversely, for any Ps-type upper semilattice L there exists an automaton whose upper semilattice of subautomata is isomorphic to L. Among the classes of automata, we consider the class of single bottom automata, and we provide the composition of a single loop automaton and a strongly connected automaton together with its automorphism group.

In the paper, we deal with the notion of an automaton over a changing alphabet, which generalizes the concept of a Mealy-type automaton. We modify the methods based on the idea of a dual automaton and its action used by B. Steinberg et al. (2011) and M. Vorobets and Ya. Vorobets (2007, 2010) [16–18] and adapt them to automata over a changing alphabet. We show that this modification provides some naturally defined automaton representations of a free nonabelian group by a 2-state automaton over a changing alphabet.

The suffix automaton (resp. factor automaton) of a finite word w is the minimal deterministic automaton recognizing the set of suffixes (resp. factors) of w. We study the relationships between the structure of the suffix and factor automata and classical combinatorial parameters related to the special factors of w. We derive formulae for the number of states of these automata. We also characterize the languages LSA and LFA of words having respectively suffix automaton and factor automaton with the minimal possible number of states.

This paper investigates the expressiveness of Propositional Projection Temporal Logic with Star (PPTL*). To this end, Büchi automata and ω-regular expressions are first extended as Stutter Büchi Automata (SBA) and Extended Regular Expressions (ERE) to include both finite and infinite strings. Further, by equivalent transformations among PPTL* formulas, SBAs and EREs, PPTL* is proved to represent exactly the full regular language. Moreover, some fragments of PPTL* are characterized, and finally, PPTL* and its fragments are classified into five different language classes.

A regular expression with n occurrences of symbol can be converted into an equivalent automaton with (n+1) states, the so-called Glushkov automaton of the expression. Conversely, it is possible to decide whether a given (n+1)-state automaton is a Glushkov one and, if so, to convert it back to an equivalent regular expression of width n. Our goal is to extend the class of automata for which such a linear retranslation is possible. We define new regular operators, called multi-tilde-bars, allowing us to simultaneously apply a multi-tilde operator and a multi-bar one to a list of expressions. The main results are that a multi-tilde-bar expression of width n can be converted into an (n+1)-state position-like automaton and that any acyclic n-state automaton can be turned into an extended expression of width O(n).

Suffix automata and factor automata are efficient data structures for representing the full index of a set of strings. They are minimal deterministic automata representing the set of all suffixes or substrings of a set of strings. This paper presents a novel analysis of the size of the suffix automaton or factor automaton of a set of strings. It shows that the suffix automaton or factor automaton of a set of strings U has at most 2Q-2 states, where Q is the number of nodes of a prefix-tree representing the strings in U. This bound significantly improves over [email protected][email protected]?-1, the bound given by Blumer et al. [A. Blumer, J. Blumer, D. Haussler, R.M. McConnell, A. Ehrenfeucht, Complete inverted files for efficient text retrieval and analysis, Journal of the ACM 34 (1987) 578-589], where @[email protected]? is the sum of the lengths of all strings in U. More generally, we give novel and general bounds for the size of the suffix or factor automaton of an automaton as a function of the size of the original automaton and the maximal length of a suffix shared by the strings it accepts. We also describe in detail a linear-time algorithm for constructing the suffix automaton S or factor automaton F of U in time O(|S|). Our algorithm applies in fact to any input suffix-unique automaton and strictly generalizes the standard on-line construction of a suffix automaton for a single input string. Our algorithm can also be used straightforwardly to generate the suffix oracle or factor oracle of a set of strings, which has been shown to have various useful properties in string-matching. Our analysis suggests that the use of factor automata of automata can be practical for large-scale applications, a fact that is further supported by the results of our experiments applying factor automata to a music identification task with more than 15,000 songs.

We present a new class of automata which strictly contains the class of aperiodic automata and shares with the latter certain synchronization properties. In particular, every strongly connected automaton in this new class is synchronizing and has a reset word of length [(n(n+1)/6] where n is the number of states of the automaton. © Springer-Verlag Berlin Heidelberg 2007. Supported by the Russian Foundation for Basic Research, grant 05-01-00540. The paper has been completed during the author’s stay at the University of Turku under the Finnish Mathematical Society International Visitors Program 2006–2007 ‘‘Algorithmic and Discrete Mathematics’’.

This article studies the expressive power of finite-state automata recognizing sets of real numbers encoded positionally. It is known that the sets that are definable in the first-order additive theory of real and integer variables 〈R,Z,+,1. In this article, we prove the reciprocal property, i.e., a subset of R that is recognizable by weak deterministic automata in every base r>1 is necessarily definable in 〈R,Z,+

Regular expressions and their extensions have become a major component of industry-oriented specification languages such as IEEE PSL [IEEE Standard for Property Specification Language (PSL). IEEE Std 1850™-2005]. The model checking procedure of regular expression based formulas, involves constructing an automaton which runs in parallel with the model.In this paper we re-examine the automata construction. We propose an algorithm that allows an intermediate representation mixing both regular expressions and automata. This representation can be thought of as plugging an automaton inside a regular expression, to replace an existing sub-expression. In order to be verified, the intermediate representation is then translated into another automaton, resulting in a set of automata running in parallel. A key feature of this algorithm is that the plug-in automaton is independent of the regular expression from which it originated, and thus can be used in several different properties.We demonstrate the usefulness of our method by providing a set of applications. We show how the use of our method allows modularity and flexibility of the automata construction, and can increase expressiveness when seres are mixed with ctl. We give two applications for which it significantly reduces the size of the automata built for formulas, thus reducing the overall run time of the model checking procedure.

We approximate context-free, or more general, languages using finite automata. The degree of approximation is measured, roughly speaking, by counting the number of incorrect answers an automaton gives on inputs of length m and observing how these values behave for large m. More restrictive variants are obtained by requiring that the automaton never accepts words outside the language or that it accepts all words in the language. A further distinction is whether a given (context-free) language has a regular approximation which is optimal under the measure of approximation degree or an approximation which is arbitrarily close to optimal. We study closure and decision properties of the approximation measure.

The two determinization procedures of Safra and Muller–Schupp for Büchi automata are compared, based on an implementation in a program called OmegaDet.

State-of-the-art algorithms for on-the-fly automata-theoretic LTL model checking make use of nested depth-first search to look for accepting cycles in the product of the system and the Büchi automaton. Here, we present two new single depth-first search algorithms that accomplish the same task. The first is based on Tarjan's algorithm for detecting strongly connected components, while the second is a combination of the first and Couvreur's algorithm for finding acceptance cycles in the product of a system and a generalized Büchi automaton. Both new algorithms report an accepting cycle immediately after all transitions in the cycle have been investigated. We show their correctness, describe efficient implementations and discuss how they interact with some other model checking techniques, such as bitstate hashing. The algorithms are compared to the nested search algorithms in experiments on both random and actual state spaces, using random and real formulas. Our measurements indicate that our algorithms investigate at most as many states as the old ones. In the case of a violation of the correctness property, the algorithms often explore significantly fewer states.

We investigate the complexity of basic decidable cases of the commutation problem for languages: testing the equality XY=YX for two languages X and Y. We show that it varies from co-NEXPTIME complete through PSPACE complete and co-NP complete to deterministic polynomial time, when Y is an explicitly given finite language and X is given by a CF grammar generating a finite language, a nondeterministic finite automaton (or a regular expression), an acyclic nondeterministic finite automaton or an explicitly given finite language, respectively. Interestingly in most cases the complexity status does not change if instead of explicitly given finite Y we consider general Y of the same type as X. For deterministic finite automata the problem remains open, due to the asymmetry of the catenation.

Quotienting by simulation equivalences is a well-established technique for reducing the size of nondeterministic Büchi automata. We adapt this technique to alternating Büchi automata. To this end we suggest two new quotients, namely minimax and semi-elective quotients, prove that they preserve the recognized languages, and show that computing them is not more difficult than computing quotients for nondeterministic Büchi automata. Our approach is game-theoretic; the proofs rely on a specifically tailored join operation for strategies in simulation games which is interesting in its own right. We explain the merits of our quotienting procedures with respect to converting alternating Büchi automata into nondeterministic ones.

We generalize a result of Daróczy and Kátai, on the characterization of univoque numbers with respect to a non-integer base (Publ. Math. Debrecen 46(3–4) (1995) 385) by relaxing the digit alphabet to a generic set of real numbers. We apply the result to derive the construction of a Büchi automaton accepting all and only the greedy sequences for a given base and digit set. In the appendix, we prove a more general version of the fact that the expansion of an element x∈Q(q) is ultimately periodic, if q is a Pisot number.

This paper focuses on the realizability problem of a framework for modeling and specifying the global behaviors of reactive electronic services (e-services). In this framework, Web accessible programs (peers) communicate by asynchronous message passing, and a virtual global watcher silently listens to the network. The global behavior is characterized by a “conversation”, which is the infinite sequence of messages observed by the watcher. We show that given a Büchi automaton specifying the desired set of conversations, called a “conversation protocol”, it is possible to realize the protocol using a set of finite state peers if three realizability conditions are satisfied. In particular, the synthesized peers will conform to the protocol by generating only those conversations specified by the protocol. Our results enable a top-down verification strategy where (1) A conversation protocol is specified by a realizable Büchi automaton, (2) The properties of the protocol are verified on the Büchi automaton specification, and (3) The peer implementations are synthesized from the protocol via projection.

Bideterministic automata are deterministic automata with the property of their reversal automata also being deterministic. It has been known that a bideterministic automaton is the minimal deterministic automaton accepting its language. This paper shows that any bideterministic automaton is the unique minimal automaton among all (including nondeterministic) automata accepting the same language. We also present a more general result that shows that under certain conditions a minimal deterministic automaton accepting some language or the reversal of the minimal deterministic automaton of the reversal language is a minimal automaton representation of the language. These conditions can be checked in polynomial time.

In this paper, we introduce a special class of Büchi automata called unambiguous. In these automata, any infinite word labels exactly one path going infinitely often through final states. The word is recognized by the automaton if this path starts in an initial state. The main result of the paper is that any rational set of infinite words is recognized by such an automaton. We give two proofs of this result. We also provide several related results.

Let E be a regular expression. Our aim is to establish a theoretical relation between two well-known automata recognizing the language of E, namely the position automaton PE constructed by Glushkov or McNaughton and Yamada, and the equation automaton EE constructed by Mirkin or Antimirov. We define the notion of c-derivative (for canonical derivative) of a regular expression E and show that if E is linear then two Brzozowski's derivatives of E are aci-similar if and only if the corresponding c-derivatives are identical. It allows us to represent the Berry–Sethi's set of continuations of a position by a unique c-derivative, called the c-continuation of the position. Hence the definition of CE, the c-continuation automaton of E, whose states are pairs made of a position of E and of the associated c-continuation. If states are viewed as positions, CE is isomorphic to PE. On the other hand, a partial derivative, as defined by Antimirov, is a class of c-derivatives for some equivalence relation, thus CE reduces to EE. Finally CE makes it possible to go from PE to EE, while this cannot be achieved directly (from the state graphs). These theoretical results lead to an O(|E|2) space and time algorithm to compute the equation automaton, where |E| is the size of the expression. This is the complexity of the most efficient constructions yielding the position automaton, while the size of the equation automaton is not greater and generally much smaller than the size of the position automaton.

We investigate properties of locally finite languages introduced by Ressayre (J. Symbolic Logic 53 (4) (1988) 1009–1026). These languages are defined by locally finite sentences and generalize languages recognized by automata or defined by monadic second-order sentences. We give many examples, showing that numerous context free languages are locally finite. Then we study closure properties of the family LOC of locally finite languages, and show that most undecidability results that hold for context free languages may be extended to locally finite languages. In a second part, we consider an extension of these languages to infinite and transfinite length words. We prove that each α-language which is recognized by a Büchi automaton (where α is an ordinal and ω⩽α

A locally testable language L is a language with the property that for some nonnegative integer k , called the order or the level of local testability, whether or not a word u is in the language L depends on (1) the prefix and suffix of the word u of length k−1 and (2) the set of intermediate substrings of length k of the word u . For given k the language is called k -testable. A finite deterministic automaton is called k -testable if the automaton accepts a k -testable language. In this paper, algorithms to verify 2-testability of order O (n 3 ) , 3-testability of order O (n 4 ) and j -testability for j>3 of order O (n j+1 ) are presented. An O (n n+2 ) time algorithm of finding the precise order of local testability is described. The time complexity of the algorithms improves on the previously known algorithms. We give necessary and sufficient conditions for an automaton to be k -testable in terms of the length of paths of related graphs. Some estimates of the upper and of the lower bound on the order of local testability follow.

A distance automaton is a finite nondeterministic automaton with a distance function which assigns zero or one to each atomic transition and assigns a nonnegative integer to each accepted word by the plus-min principle. In this paper, we prove that the distances of all accepted words of a distance automaton is bounded by some constant if and only if they are bounded by 2 4m 3 +m log (m+2)+m , where m is the number of states of the automaton.

Glushkov's algorithm computes a nondeterministic finite automaton without e -transitions and with n+1 states from a regular expression having n occurrences of letters. The aim of this paper is to give a set of necessary and sufficient conditions characterizing this automaton. Our characterization theorem is formulated in terms of directed graphs. Moreover these conditions allow us to produce an algorithm of conversion of a Glushkov automaton into a regular expression of small size.

For a Muller automaton only a subset of its states is needed to decide whether a run is accepting or not. The set I of the infinitely often visited states can be replaced by the intersection I∩W with a fixed set W of states, provided W is large enough to distinguish between accepting and non-accepting loops in the automaton. We call such a subset W a separating set. Whereas the idea was previously introduced by McNaughton (Ann. Pure Appl. Logic 65 (1993) 149–184), the algorithmic construction of the smallest separating sets is not treated in the literature. In this paper we show that the problem whether in a Muller automaton a separating set of a given size exists is NP-complete. As a step towards an efficient computation of a separating set of minimal size we present an algorithm in the second part of the paper, based on an analysis of the loop structure of the given automaton.

This paper deals with finite-memory automata, introduced in Kaminski and Francez (Theoret. Comput. Sci. 134 (1994) 329–363). With a restricted memory structure that consists of a finite number of registers, a finite-memory automaton can store arbitrary input symbols. Thus, the language accepted by a finite-memory automaton is defined over a potentially infinite alphabet. The following decision problems are studied for a general finite-memory automata A as well as for deterministic ones: the membership problem, i.e., given an A and a string w , to decide whether w is accepted by A , and the non-emptiness problem, i.e., given an A , to decide whether the language accepted by A is non-empty. The membership problem is P-complete, provided a given automaton is deterministic, and each of the other problems is NP-complete. Thus, we conclude that the decision problems considered are intractable.

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.

A generalized automaton (GA) is a finite automaton where the single transitions are defined on words rather than on single letters. Generalized automata were considered by Hashiguchi (1991), who proved that the problem of calculating the size of a minimal GA is decidable.We define the model of deterministic generalized automaton (DGA) and study the problem of its minimization. A DGA has the restriction that, for each state, the sets of words corresponding to the transitions of that state are prefix sets. We solve the problem of calculating the number of states of a minimal DGA for a given language, by giving a procedure that effectively constructs a minimal DGA starting from the minimal equivalent (conventional) deterministic automaton.

A reset word takes all states of a finite automaton to a single state. In this paper, it is shown that the length of the shortest reset word for a solvable automaton with n states is at most n − 1 and this bound is reachable.

Direct embeddings of the full branching-time CTL ∗ and its extension ECTL ∗ into the modal μ-calculus are presented. The embeddings use tableaux as intermediate representations of formulas, and use extremal fixed points to characterise those paths through tableaux that satisfy an admissibility criterion, guaranteeing eventualities to be eventually satisfied. The version of ECTL ∗ considered replaces the entire linear-time fragment of CTL ∗ by Buchi automata on infinite strings. As a consequence the embedding of ECTL ∗ turns out to be computable in linear time, while the embedding of CTL ∗ is doubly exponential in the worst case.

A two-dimensional nondeterministic on-line tessellation acceptor (2-NOTA) is a special type of real-time two-dimensional nondeterministic cellular automaton in which data flows from the upper-left corner to the lower-right corner. A two-dimensional alternating finite automaton (2-AFA) is an alternating finite automaton with a two-dimensional rectangular input whose input head can move in all four directions on the input. In this paper, we show that 2-NOTAs and 2-AFAs are incomparable. This answers in the negative an open question posed by Ito (this journal, 1989). Closure properties of the classes of languages (i.e., sets of two-dimensional patterns) accepted by two-way, three-way, and four-way two-dimensional alternating finite automata and two-dimensional alternating finite automata with only universal states (2-UFAs) are also obtained which answer several open questions posed by Inoue and Takanami (1988).

It is well known that congruential tree languages are the same as recognizable tree languages. In this paper we construct, in O( n log n ) time, for a given ground term equation system E and given ground trees p 1 ,…, p k , a deterministic tree automaton A recognizing the congruential tree language [p1] ↔ ∗ E ∪…∪[pk] ↔ ∗ E , where n is the number of occurrences of symbols in E and p 1 ,…, p k .

We study relations over ω-words using a representation by tree languages. An ω-word over an alphabet with k letters is considered as a path through the k-ary tree, an n-tuple of ω-words as an n-tuple of paths (coded by an appropriate valuation of the k-ary tree using values in {0,1}n), and a relation over ω-words as a tree language. In the first part of the paper we give a logical characterization of the “Rabin-recognizable relations” (whose associated tree languages are recognized by Rabin tree automata) in terms of “weak chain logic”, a restriction of monadic second-order logic over trees. In the second part of the paper an extended logic is considered, obtained by adjoining the “equal-level predicate” over trees. We describe the class of relations over ω-words which (in the tree language representation) are definable in this logic, and show that the theory of the k-ary tree in this logic is decidable. It covers tree properties which are not expressible in the monadic second-order logic SkS.

Given a finite alphabet Σ, we give a simple characterization of those Gδ subsets of Σω which are deterministic ω-regular (i.e. accepted by Büchi automata) over Σ and then characterize the ω-regular languages in terms of these (rational) Gδ sets. Our characterization yields a hierarchy of ω-regular languages similar to the classical difference hierarchy of Hausdorff and Kuratowski for Δ03 sets (i.e. the class of sets which are both Fσδ and Gδσ). We then prove that the Hausdorff-Kuratowski difference hierarchy of Δ03 when restricted to ω-regular languages coincides with our hierarchy. We obtain this by showing that if an ω-regular language K can be separated from another ω-regular language L by the union of alternate differences of a decreasing sequence of Gδ sets of length n, then there is a decreasing sequence (of length n) of rational Gδ sets such that the union of alternate differences separates K from L. Our results not only generalize a result of Landweber (1969), but also yield an effective procedure for determining the complexity of a given Muller automaton. We also show that our hierarchy does not collapse, thus, giving a fine classification of ω-regular languages and of Muller automata.

A distance function on a finite automaton M is defined by assigning to each transition a distance of nonnegative integer value. M is said to be limited in distance if there is a nonnegative integer k such that, for each accepted string w in the language of M, there is an accepting path p for w on which the sum of distances is bounded by k. The limitedness theorem [6,9] on finite automata with distance functions states that it is decidable if an arbitrary finite automaton with a distance function is limited in distance. In this paper, we give an algebraic proof of the theorem and derive from it an exponential-time decision algorithm. In addition, we prove that the decision problem is PSPACE-hard.

The problem of complementing Büchi automata arises when developing decision procedures for temporal logics of programs. Unfortunately, previously known constructions for complementing Büchi automata involve a doubly exponential blow-up in the size of the automaton. We present a construction that involves only an exponential blow-up. We use this construction to prove a polynomial space upper bound for the propositional temporal logic of regular events and to prove a complexity hierarchy result for quantified propositional temporal logic.

A finite automaton with multiplication (FAM) is a finite automaton with a register which is capable of holding any positive rational number. The register can be multiplied by any of a fixed number of rationals and can be tested for value 1. Closure properties and decision problems for various types of FAM's (e.g. two-way, one-way, nondeterministic, deterministic) are investigated. In particular, it is shown that the languages recognized by two-way deterministic FAM's are of tape complexity log n and time complexity n 3 . Some decision problems related to vector addition systems are also studied.

Given a finite automaton, its infinite behavior is defined by Buchi (1962), Eilenberg (1974) and McNaughton (1966) as the set of all infinite sequences of letters which label paths passing infinitely many times through a given subset of states. Two finite automata are said to be equivalent when their infinite behaviors are equal. In this paper we give a necessary and sufficient condition of equivalence, which uses considerations over finite behaviors only. An algorithm for the general case (deterministic or not) is given; its time and space complexity is better than any other existent method.

The class of all state-independent automata is characterized as a subclass of all semigroup automata (automata generated by semigroups). A state-independent automaton is identified as an automaton over a finite semigroup that is stationary on the right. Associated results are included.

Given a Buchi automaton with n states, we propose an elementary construction of a Buchi automaton with O(16 n 2 ) states which recognizes the complement of the ω-language recognized by the first one.

To every input string of a two-way automaton one associates a quadruple of partial functions (or relations) between the states. This quadruple describes the behavior of the automaton on that input, and can also be used to formulate acceptance, or notions like the crossing sequence. Formulas are given that show how two such quadruples are combined (“multiplied”) as their corresponding input strings are concatenated.

We prove that every FTR-language R (factorial, transitive, rational) admits a minimal irreducible deterministic automaton. This automaton can be computed in three different ways. First, it admits an intrinsic definition depending only on the syntactic monoid of the language R . Secondly, it is a quotient for a simple equivalence relation of every irreducible deterministic automaton recognizing R . Thirdly, it is a subautomaton of the classical minimal deterministic automaton associated with R , computable with a simple algorithm.