The quotient complexity of a regular language L is the number of left quotients of L, which is the same as the state complexity of L. Suppose that L and L' are binary regular languages with quotient complexities m and n, and that the transition semigroups of the minimal deterministic automata accepting L and L' are the symmetric groups S_m and S_n of degrees m and n, respectively. Denote by o any binary boolean operation that is not a constant and not a function of one argument only. For m,n >= 2 with (m,n) not in (2,2),(3,4),(4,3),(4,4) we prove that the quotient complexity of LoL' is mn if and only either (a) m is not equal to n or (b) m=n and the bases (ordered pairs of generators) of S_m and S_n are not conjugate. For (m,n)in (2,2),(3,4),(4,3),(4,4) we give examples to show that this need not hold. In proving these results we generalize the notion of uniform minimality to direct products of automata. We also establish a non-trivial connection between complexity of boolean operations and group theory.

Keywords: boolean operation, quotient complexity, regular language, state complexity, symmetric group, transition semigroup

Keywords: transition complexity, automata theory, finite languages, descriptional complexity

Kleene algebra with tests (kat) is an equational system that extends Kleene algebra, the algebra of regular expressions, and that is specially suited to capture and verify properties of simple imperative programs. In this paper we study two constructions of automata from KAT expressions: the Glushkov automaton, and a new construction based on the notion of prebase (equation automata. Contrary to other automata constructions from KAT expressions, these two constructions enjoy the same descriptional complexity behaviour as their conterparts for regular expressions, both in the worst-case as well as in the average-case. In particular, our main result is to show that, asymptotically and on average the number of transitions of the nfa_Pos is linear in the size of the kat expression.

We introduce the notion of reset left regular decomposition of an ideal regular language and we prove that there is a one-to-one correspondence between these decompositions and strongly connected synchronizing automata. We show that each ideal regular language has at least a reset left regular decomposition. As a consequence each ideal regular language is the set of synchronizing words of some strongly connected synchronizing automaton. Furthermore, this one-to-one correspondence allows us to formulate Cerny's conjecture in a pure language theoretic framework.

The state complexity of basic operations on finite languages (considering complete DFAs) has been extensively studied in the literature. In this paper we study the incomplete (deterministic) state and transition complexity on finite languages of boolean operations, concatenation, star, and reversal. For all operations we give tight upper bounds for both descriptional measures. We correct the published state complexity of concatenation for complete DFAs and provide a tight upper bound for the case when the right automaton is larger than the left one. For all binary operations the tightness is proved using family languages with a variable alphabet size. In general the operational complexities depend not only on the complexities of the operands but also on other refined measures.

Y. Gao et al. studied for the first time the transition complexity of Boolean operations on regular languages based on not necessarily complete DFAs. For the intersection and the complementation, tight bounds were presented, but for the union operation the upper and lower bounds differ by a factor of two. In this paper we continue this study by giving tight upper bounds for the concatenation, the Kleene star and the reversal operations. We also give a new tight upper bound for the transition complexity of the union, which refutes the conjecture presented by Y. Gao et al..

In this report we describe the formalisation of a simple imperative language with concurrent/parallel and atomic execution statements within the Coq theorem prover. Our formalisation includes the specification of a simple imperative programming language with statements for parallel and atomic execution of code, an underlying small-step structural semantics and a proof system that is sound with respect to such semantics. With this formalisation we give a first step towards the certified verification of shared- variable concurrent/parallel programs under the context of Cliff Jones? Rely-Guarantee reasoning and in the logic of Coq.

Kleene algebra with tests (KAT) is an equational system for program verification, which is the combination of Boolean algebra (BA) and Kleene algebra (KA), the algebra of regular expressions. In particular, KAT subsumes the propositional fragment of Hoare logic (PHL) which is a formal system for the specification and verification of programs, and that is currently the base of most tools for checking program correctness. Both the equational theory of KAT and the encoding of PHL in KAT are known to be decidable. In this paper we present a new decision procedure for the equivalence of two KAT expressions based on the notion of partial derivatives. We also introduce the notion of derivative modulo particular sets of equations. With this we extend the previous procedure for deciding PHL. Some experimental results are also presented.

Nowadays, an increasing attention is being given to the study of the descriptional complexity on the average case. Although the underlying theory for such a study seems intimidating, one can obtain interesting results in this area without too much effort. In this gentle introduction we take the reader on a journey through the basic analytical tools of that theory, giving some illustrative examples using regular expressions. We finalize with some new asymptotic average case results for several ε-NFA constructions, presented in a unified framework.

This work presents a mechanically verified implementation of an algorithm for deciding regular expression (in-)equivalence within the COQ proof assistant. This algorithm decides regular expression equivalence through an iterated process of testing the equivalence of their partial derivatives and also does not construct the underlying automata. Our implementation has a refutation step that improves the general efficiency of the decision procedure by enforcing the in-equivalence of regular expressions at early stages of computation. Recent theoretical and experimental research provide evidence that this method is, on average, more efficient than the classical methods based in automata. We present some performance tests and comparisons with similar approaches.

In this paper, the relation between the Glushkov automaton (nfaPos) and the partial derivative automaton (nfaPD) of a given regular expression, in terms of transition complexity, is studied. The average transition complexity of nfaPOS was proved by Nicaud to be linear in the size of the corresponding expression. This result was obtained using an upper bound of the number of transitions of nfaPOS. Here we present a new quadratic construction of nfaPOS that leads to a more elegant and straightforward implementation, and that allows the exact counting of the number of transitions. Based on that, a better estimation of the average size is presented. Asymptotically, and as the alphabet size grows, the number of transitions per state is on average 2. Broda et al. computed an upper bound for the ratio of the number of states of nfaPD to the number of states of nfaPOS, which is about (1)/(2) for large alphabet sizes. Here we show how to obtain an upper bound for the number of transitions in nfaPD, which we then use to get an average case approximation. In conclusion, assymptotically, and for large alphabets, the size of nfaPD is half the size of the nfaPOS. This is corroborated by some experiments, even for small alphabets and small regular expressions.

Linear finite transducers underlie a series of schemes for Public Key Criptography (PKC) proposed in the 90s of the last century. The uninspiring and arid language then used, condemned these works to oblivion. Although some of these schemes were, after, shown to be insecure, the promise of a new system of PKC relying in different complexity assumptions is still quite exciting. The algorithms there used depend heavily on the results of invertibility of linear transducers. In this paper we introduce the notion of post-initial linear transducer, which is an extension of the notion of linear finite transducer with memory, and for which the previous fundamental results on invertibility still hold. Using this notion, we give a necessary and sufficient condition for left invertibility with fixed delay of finite transducers, as well as a new explicit method to obtain a left inverse.

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.

In this paper we present a computer assisted proof of the correctness of a partial derivative automata construction from a regular expression within the Coq proof assistant. This proof is part of a formalization of Kleene algebra and regular languages in Coq towards their usage in program certification.

In this paper, the relation between the Glushkov automaton Nfapos and the partial derivative automaton (Nfapd) of a given regular expression, in terms of transition complexity, is studied. The average transition complexity of Nfapos was proved by Nicaud to be linear in the size of the corresponding expression. This result was obtained using an upper bound of the number of transitions of NFApos. Here we present a new quadratic construction of NFApos that leads to a more elegant and straightforward implementation, and that allows the exact counting of the number of transitions. Based on that, a better estimation of the average size is presented. Asymptotically, and as the alphabet size grows, the number of transitions per state is on average 2. Broda et al. computed an upper bound for the ratio of the number of states of NFApd to the number of states of NFApos, which is about 1/2 for large alphabet sizes. Here we show how to obtain an upper bound for the number of transitions in NFApd, which we then use to get an average case approximation. Some experimental results are presented that illustrate the quality of our estimate.

In this paper we investigate from a statistical point of view the expected compression ratio between the size of a minimal Deterministic Finite Cover Automaton (DFCA) and the size of the minimal corresponding Determinitic Finite Automaton (DFA). Using sound statistical methods, we extend the experimental study done in [16], thus obtaining a much better picture of the compression power of DFCAs. We compute the expected ratio for the family of all finite languages, but also for various subfamilies of finite languages, such as prefix, suffix-free languages prefix and suffix closed languages, or (un)balanced languages. We also give an example of a family for which the expected compression ratio is very high.

Keywords: cover automata, automata theory, compression

The partial derivative automaton Apd is usually smaller than other nondeterministic finite automata constructed from a regular expression, and it can be seen as a quotient of the Glushkov automaton (Apos). By estimating the number of regular expressions that have epsilon as a partial derivative, we compute a lower bound of the average number of mergings of states in Apos and describe its asymptotic behaviour. This depends on the alphabet size, k, and for growing k's its limit approaches half the number of states in Apos. The lower bound corresponds to consider the Apd automaton for the marked version of the re, i.e. where all its letters are made different. Experimental results suggest that the average number of states of this automaton, and of the APd automaton for the unmarked re, are very close to each other.

The partial derivative automaton (NFA_Pd) is usually smaller than other non-deterministic finite automata constructed from a regular expression, and it can be seen as a quotient of the Glushkov automaton (NFA_Pos). By estimating the number of regular expressions that have epsilon as a partial derivative, we compute a lower bound of the average number of mergings of states in NFA_Pos and describe its asymptotic behaviour. This depends on the alphabet size, k, and its limit, as k goes to infinity, is 1/2. The lower bound corresponds exactly to consider the NFA_Pd automaton for the marked version of the RE, i.e. where all its letters are made different. Experimental results suggest that the average number of states of this automaton, and of the NFA_Pos automaton for the unmarked RE, are very close to each other.

Recently, the problem of obtaining a short regular expression equivalent to a given finite automaton has been intensively investigated. Algorithms for converting finite automata to regular expressions have an exponential blow-up in the worst-case. To overcome this, simple heuristic methods have been proposed. In this paper we analyse some of the heuris- tics presented in the literature and propose new ones. We also present some experimental comparative results based on uniform random gener- ated deterministic finite automata.

Regular expressions (RES), because of their succinctness and clear syntax, are the common choice to represent regular languages. However, efficient pattern matching or word recognition depend on the size of the equivalent nondeterministic finite automata (NFA). We present the implementation of several algorithms for constructing small epsilon-free NFAs from RES within the FAdo system, and a comparison of regular expression measures and NFA sizes based on experimental results obtained from uniform random generated RES. For this analysis, nonredundant RES and reduced RES in star normal form were considered.

GUItar is a graphical environment for graph visualization, editing, and interaction, that specially focuses in finite automata dia- grams. The application incorporates mechanisms to facilitate the editing of these graphs. It also provides a style manager that allows the cre- ation of rich state and arc styles to be used in the drawing of its ob- jects. This style manager allows the system to cope with complex styles, broaden the application scope to graphical representations of other com- putational models like transducers or Turing machines. GUItar also has a foreign function call (FFC) mechanism for the easy integration of exter- nal modules and libraries like automata symbolic manipulators or graph drawing libraries. For automatic graph drawing we are developing FA- goo, a package that seeks to provide tools capable of finding pleasant graph drawings. FAgoo implements graph drawing algorithms that find embeddings which the user, with minimal manual changes, can adjust to its aesthetically taste. Both GUItar and FAgoo are on going projects licensed under GPL.

The minimal deterministic finite automaton is generally used to determine regular languages equality. Using Brzozowski's notion of derivative, Antimirov and Mosses proposed a rewrite system for deciding regular expressions equivalence of which Almeida et al. presented an improved variant. Hopcroft and Karp proposed an almost linear algorithm for testing the equivalence of two deterministic finite automata that avoids minimisation. In this paper we improve this algorithm's best-case running time, present an extension to non-deterministic finite automata, and establish a relationship with the one proposed in Almeida et al., for which we also exhibit an exponential lower bound. We also present some experimental comparative results.

GUItar is a visualization software tool for various types of automata (standard, weighted, pushdown, transducers, Turing machines, etc.). It provides interactive manipulation of diagrams, comprehensive graphic style creation, multiple export/import filters, and a generic “foreign function calls” (ffc) interface with external systems. In this paper we describe GUItar's XML framework and show how it allows for extensibility, modularity and interoperability.