The partial derivative automaton (apd) is an elegant simulation of a regular expression. Although it is, in general, smaller than the position automaton (apos), the algorithms that build apd in quadratic worst-case time first compute apos. Asymptotically, and on average for the uniform distribution, the size of apd is half the size of apos, being both linear on the size of the expression. We address the construction of apd efficiently, on average, avoiding the computation of apos. The expression and the set of its partial derivatives are represented by a directed acyclic graph with shared common subexpressions. We develop an algorithm for building apds from expressions in strong star normal form of size n that runs, on average, in time that asymptotically behaves as n^(3/2)log(n)^(1/4), and space as n^(3/2)/(log(n))^(3/4). Empirical results corroborate its good practical performance.

We revisit the basic concept of quotient of a regular language R by a language L that is not necessarily regular.

We revise the deterministic complexity upper bounds of the quotient operation, and we also address the nondeterministic case. Specifically, the revised deterministic upper bound is shown to be more accurate for all hard streams of regular languages.

When both languages R and L are regular, we give algorithms to construct their

quotient in four ways. If the two languages are given via Nfas, the first algorithm produces an Nfa for the desired quotient.

If the two languages are given via regular expressions, we present an algorithm that produces a regular expression for the quotient both using ordinary derivatives and using partial derivatives. Finally, we consider regular expressions with a quotient operator and define the set of partial derivatives for regular expressions with this operator. Thus, using the partial derivative automaton, one can directly produce an Nfa for the quotient. We have implemented all algorithms and present here experimental results.

n this paper we consider block languages, namely sets of words having the same length, and we propose a new representation for these languages. In particular, given an alphabet of size k and a length l, these languages can be represented by bitmaps of size k^l, in which each bit indicates whether the correspondent word, according to the lexicographical order, belongs to the language (bit equal to 1) or not (bit equal to 0). This representation turns out to be a good tool for the investigation of several properties of block languages, making proofs simpler and reasoning clearer. After showing how to convert bitmaps into minimal deterministic and nondeterministic finite automata, we use this representation as a tool to study the deterministic and nondeterministic state complexity of block languages, as well as the costs of basic operations on block languages, in terms of the sizes of the equivalent finite automata.

In this paper we consider block languages, namely sets of words having the same length, and study the deterministic and nondeterministic state complexity of several operations on these languages. Being a subclass of finite languages, the upper bounds of operational state complexity known for finite languages apply for block languages as well. However, in several cases, smaller values were found. Block languages can be represented as bitmaps, which are a good tool to study their minimal finite automata and their operations, as we illustrate here.

The difference set of two (nondeterministic, in general) transducers is the set of all input words for which the output sets of the two transducers are not equal. When the two transducers realize homomorphisms, their difference set is the complement of the well known equality set of the two morphisms.

However, difference sets result in classes of languages that are different than the classes resulting from equality sets.

We also consider the following word problem: given transducers s, t and input w, tell whether the output sets s(w) and t(w) are different. In general the problem is PSPACE-complete, but it becomes NP-complete when at least one of the given transducers has finite outputs. We also provide a PRAX (polynomial randomized approximation) algorithm for the word problem as well as for the NFA (in)equivalence problem. Our presentation of PRAX algorithms improves the original presentation.

In this paper we consider block languages, namely sets of words having the same length, and we propose a new representation for these languages. In particular, given an alphabet of size k and a length l, a block language can be represented by a bitmap of length k^l, where each bit indicates whether the corresponding word, according to the lexicographical order, belongs, or not, to the language (bit equal to 1 or 0, respectively). This representation turns out to be a good tool for the investigation of several properties of block languages, making proofs simpler and reasoning clearer. First, we show how to convert bitmaps into deterministic and nondeterministic finite automata. We then focus on the size of the machines obtained from the conversion and we prove that their size is minimal. Finally, we give an analysis of the maximum number of states sufficient to accept every block language in the deterministic and nondeterministic case.

Although regular expressions do not correspond univocally to regular languages, it is still worthwhile to study their properties and algorithms. For the average case analysis one often relies on the uniform random generation using a specific grammar for regular expressions, that can represent regular languages with more or less redundancy. Generators that are uniform on the set of expressions are not necessarily uniform on the set of regular languages. Nevertheless, it is not straightforward that asymptotic estimates obtained by considering the whole set of regular expressions are different from those obtained using a more refined set that avoids some large class of equivalent expressions. In this paper we study a set of expressions that avoid a given absorbing pattern. It is shown that, although this set is significantly smaller than the standard one, the asymptotic average estimates for the size of the Glushkov automaton for these expressions does not differ from the standard case. Furthermore, for this set the asymptotic density of epsilon-accepting expressions is also the same as for the set of all standard regular expressions.

We define the notion of location for regular expressions with shuffle by extending the notion of position in standard regular expressions. Locations allow for the definition of the sets Follow, First, and Last with their usual semantics. From these, we construct an automaton for regular expressions with shuffle (apos), which generalises the standard position/Glushkov automaton. The sets mentioned above are also the foundation for other constructions, such as the Follow automaton, and automata based on pointed expressions. As a consequence, all these constructions can be generalised to the shuffle operator. We show that the partial derivative automaton is a right-quotient of apos. We relate apos with another automaton construction based on positions that has been previously studied (apartialpos). The prefix automaton is extended to the shuffle operator and shown not to be a quotient of apos. Locations are also used to define a position automaton for regular expressions with the intersection.

Several notions of synchronisation in concurrent systems can be modelled by regular shuffle operators. In this paper we consider regular expressions extended with three operators corresponding respectively to strong, arbitrary, and weak synchronisation. For these expressions, we define a location based position automaton. Furthermore, we show that the partial derivative automaton is still a quotient of the position automaton.

2D regular expressions represent rational relations over two alphabets Sigma and DElta. In standard 2D expressions (S2D-RE) the basic terms are generators of Sigma*xDelta*, while in generalised 2D expressions (2D-RE) the basic terms are pairs of (ordinary) regular expressions over one alphabet (1D). In this paper we study the average state complexity of partial derivative standard transducers (TPD) for both S2D-RE and 2D-RE. For S2D-RE we obtain the same asymptotic bounds as for partial derivative automata. For 2D-RE, while in the worst case the number of states of TPD can be O(n^2), where n is the size of the expression, asymptotically and on average that value is bounded from above by O(n^(3/2)). We also show that asymptotically and on average the alphabetic size of a 2D-RE is half of its size. All results are obtained in the framework of analytic combinatorics considering generating functions of parametrised combinatorial classes defined implicitly by algebraic curves. In particular, we generalise the methods developed in previous work to a broad class of analytic function

Synchronised shuffle operators allow to specify symbols on which the operands must or can synchronise instead of interleave. Recently, partial derivative and position based automata for regular expressions with synchronised shuffle operators were introduced. In this paper, using the framework of analytic combinatorics, we study the asymptotic average state complexity of partial derivative automata for regular expressions with strongly and arbitrarily synchronised shuffles. The new results extend and improve the ones previously obtained for regular expressions with shuffle and intersection. For intersection, asymptotically the average state complexity of the partial derivative automaton is 3, which significantly improves the known exponential upper-bound.

In coding and information theory, it is desirable to construct maximal codes that can be either variable length codes or error control codes of fixed length. However deciding code maximality boils down to deciding whether a given NFA is universal, and this is a hard problem (including the case of whether the NFA accepts all words of a fixed length). On the other hand, it is acceptable to know whether a code is `approximately' maximal, which then boils down to whether a given NFA is `approximately' universal. Here we introduce the notion of a (1-epsilon)-universal automaton and present polynomial randomized approximation algorithms to test NFA universality and related hard automata problems, for certain natural probability distributions on the set of words. We also conclude that the randomization aspect is necessary, as approximate universality remains hard for any fixed polynomially computable epsilon.

Keywords: NFA universality, approximation, randomized algorithm, PSPACE hard

2D regular expressions represent rational relations over two alphabets Sigma and Delta. In standard 2D expressions (S2D-RE) the basic terms are generators of Sigma^*xDelta^*, while in generalised 2D expressions (2D-RE) the basic terms are pairs of (ordinary) regular expressions over one alphabet (1D). In this paper we study the average state complexity of partial derivative standard transducers (TPD)) for both S2D-RE and 2D-RE. For S2D-RE we obtain the same asymptotic bounds as for partial derivative automata. For 2D-RE, while in the worst case the number of states of TPD can be O(n^2), where n is the size of the expression, asymptotically and on average that value is bounded from above by O(n^3/2). We also show that asymptotically and on average the alphabetic size of a 2D-RE is half of its size. All results are obtained in the framework of analytic combinatorics considering generating functions of parametrised combinatorial classes defined implicitly by algebraic curves. In particular, we generalise the methods developed in previous work to a broad class of analytic functions.

The notions of derivative and partial derivative of regular expressions revealed themselves to be very powerful and have been successfully extended to many other formal language classes and algebraic structures. Although the undisputed elegance of this formalism, its efficient practical use is still a challenging research topic. Here we give a brief historical overview and summarise some of these aspects.

In coding and information theory, it is desirable to construct maximal codes that can be either variable length codes or error control codes of fixed length. However deciding code maximality boils down to deciding whether a given NFA is universal, and this is a hard problem (including the case of whether the NFA accepts all words of a fixed length). On the other hand, it is acceptable to know whether a code is `approximately' maximal, which then boils down to whether a given NFA is `approximately' universal. Here we introduce the notion of a (1-e)-universal automaton and present polynomial randomized approximation algorithms to test NFA universality and related hard automata problems, for certain natural probability distributions on the set of words. We also conclude that the randomization aspect is necessary, as approximate universality remains hard for any fixed polynomially computable e.

There are many different constructions when converting regular expressions to finite automata. In this paper we focus on the prefix automaton APRE introduced by Yamamoto in 2014. We present two different methods for the construction of APRE. First, an inductive one, based on a system of expression equations. A second one using an iterative function for computing the states and transitions. We establish relationships between APRE and other constructions, such as the position automaton, partial derivative automaton and their double reversal (dual) counterparts. We study the average size of these constructions, both experimentally and from an analytic combinatorics point of view. Finally, we extend the construction of the prefix automaton to regular expressions with intersection and show that the relationships with the other automaton constructions also hold for these expressions.

We are interested in regular expressions that represent word relations in an alphabet-invariant way---for example, the set of all word pairs (u,v) where v is a prefix of u independently of what the alphabet is. Current software systems of formal language objects do not have a mechanism to define such objects. Labelled graphs (transducers and automata) with alphabet-invariant and user-defined labels were considered in a recent paper. In this paper we study derivatives of regular expressions over labels (atomic objects) in some set B. These labels can be any strings as long as the strings represent subsets of a certain monoid. We show that the number of partial derivatives of any type B regular expression is linearly bounded, and that one can define partial derivative labelled graphs, whose transition labels can be elements of another label set X as long as X and B refer to the same monoid. We also show how to use derivatives directly to decide whether a given word is in the language of a regular expression over set specs. Set specs and pairing specs are label sets allowing one to express languages and relations over large alphabets in a natural and concise way such that many algorithms work directly on these labels without the need to expand these labels to linear or quadratic size expressions.

We define the notion of location for regular expressions with shuffle by extending the notion of position in standard regular expressions. Locations allow for the definition of the sets Follow, First and Last with their usual semantics. From these, we construct an automaton for regular expressions with shuffle (apos), which generalises the standard position/Glushkov automaton. The sets mentioned above are also the foundation for other constructions, such as the Follow automaton, and automata based on pointed expressions. As a consequence, all these constructions can now be directly generalised to regular expressions with shuffle, as well as their known relationships. We also show that the partial derivative automaton (apd) is a (right) quotient of the new position automaton, apos. In previous work an automaton construction based on positions was studied (adpos), and here we relate apos and adpos. Finally, we extend the construction of the prefix automaton to the shuffle operator and show that it is not a quotient of apos.

Although regular expressions do not correspond univocally to regular languages, it is still worthwhile to study their properties and algorithms. For the average case analysis one often relies on the uniform random generation using a specific grammar for regular expressions, that can represent regular languages with more or less redundancy. Generators that are uniform on the set of expressions are not necessarily uniform on the set of regular languages. Nevertheless, it is not straightforward that asymptotic estimates obtained by considering the whole set of regular expressions are different from those obtained using a more refined set that avoids some large class of equivalent expressions. In this paper we study a set of expressions that avoid a given absorbing pattern. It is shown that, although this set is significantly smaller than the standard one, the asymptotic average estimates for the size of the Glushkov automaton for these expressions does not differ from the standard case.

Partial derivatives are widely used to convert regular expressions to nondeterministic automata. For the word membership problem, it is not strictly necessary to build an automaton. In this paper, we study the size of partial derivatives on the average case. For expressions in strong star normal form, we show that on average and asymptotically the largest partial derivative is at most half the size of the expression. The results are obtained in the framework of analytic combinatorics considering generating functions of parametrised combinatorial classes defined implicitly by algebraic curves. Our average case estimates suggest that a detailed word membership algorithm based directly on partial derivatives should be analysed both theoretically and experimentally.

Although regular expressions do not correspond univocally to regular languages, it is still worthwhile to study their properties and algorithms. For the average case analysis one often relies on the uniform random generation using a specific grammar for regular expressions, that can represent regular languages with more or less redundancy. Generators that are uniform on the set of expressions are not necessarily uniform on the set of regular languages. Nevertheless, it is not straightforward that asymptotic estimates obtained by considering the whole set of regular expressions are different from those obtained using a more refined set that avoids some large class of equivalent expressions. In this paper we study a set of expressions that avoid a given absorbing pattern. It is shown that, although this set is significantly smaller than the standard one, the asymptotic average estimates for the size of the Glushkov automaton for these expressions does not differ from the standard case.

The partial derivative automaton (apd) is an elegant simulation of a regular expression. Although it is, in general, smaller than the position automaton (apos), the algorithms that build apd in quadratic worst-case time, first compute apos. Asymptotically, and on average for the uniform distribution, the size of apd is half the size of apos, being both linear on the size of the expression. We address the construction of apd efficiently, on average, avoiding the computation of apos. The expression and the set of its partial derivatives are represented by a directed acyclic graph with shared common subexpressions. We develop an algorithm for building apd's from expressions in strong star normal form of size n that runs in time O(n^3/2sqrt[4]log(n)) and space O(n^3/2/(log n)^3/4), on average. Empirical results corroborate its good practical performance.

We study the computational power of parsing expression grammars (PEGs). We begin by constructing PEGs with unexpected behaviour, and surprising new examples of languages with PEGs, including the language of palindromes whose length is a power of two, and a binary-counting language. We then propose a new computational model, the scaffolding automaton, and prove that it exactly characterises the computational power of parsing expression grammars (PEGs). Several consequences will follow from this characterisation: (1) we show that PEGs are computationally “universal”, in a certain sense, which implies the existence of a PEG for a P-complete language; (2) we show that there can be no pumping lemma for PEGs; and (3) we show that PEGs are strictly more powerful than online Turing machines which do o(n/(log n)^2) steps of computation per input symbol.

Average-case complexity results provide important information about computational models and methods, as worst-case scenarios usually occur for a negligible amount of cases. The frame- work of analytic combinatorics provides an elegant tool for that analysis, completely avoiding the use of statistical methods, by relating combinatorial objects to algebraic properties of complex analytic generating functions. We have previously used this framework to study the average size of different nondeterministic finite automata simulations of regular expressions. In some cases it was not feasible to obtain explicit expressions for the generating functions involved, and we had to resort to Puiseux expansions. This is particularly important when dealing with families of generating functions indexed by a parameter, e.g. the size of underlying alphabets, and when the corresponding generating functions are obtained by algebraic curves of degree higher than two. In this paper we expound our approach in a tutorial pace, providing sufficient details to make it available to the reader. Corrigendum: In formula (7) a 4 is missing in the denominator; so 4 should be removed from (8). We thank M. Wallner fo hthe correction.

2D regular expressions represent rational relations over two alphabets. In this paper we study the average state complexity of partial derivative standard transducers (tpd) that can be defined for (general) 2D expressions where basic terms are pairs of ordinary regular expressions (1D). While in the worst case the number of states of tpd can be O(n^2), where n is the size of the expression, asymptotically and on average that value is bounded from above by O(n^3/2). Moreover, asymptotically and on average the alphabetic size of a 2D expression is half of the size of that expression. All results are obtained in the framework of analytic combinatorics considering generating functions of parametrised combinatorial classes defined implicitly by algebraic curves. In particular, we generalise the methods developed in previous work to a broad class of analytic functions.

We are interested in regular expressions and transducers that represent word relations in an alphabet-invariant way---for example, the set of all word pairs (u,v) where v is a prefix of u independently of what the alphabet is. Current software systems of formal language objects do not have a mechanism to define such objects. We define transducers in which transition labels involve what we call set specifications, some of which are alphabet invariant. In fact, we give a more broad definition of automata-type objects, called labelled graphs, where each transition label can be any string, as long as that string represents a subset of a certain monoid. Then, the behaviour of the labelled graph is a subset of that monoid. We do the same for regular expressions. We obtain extensions of a few classic algorithmic constructions on ordinary regular expressions and transducers at the broad level of labelled graphs and in such a way that the computational efficiency of the extended constructions is not sacrificed. For transducers with set specs we obtain further algorithms that can be applied to questions about independent regular languages,

as well as a decision question about synchronous transducers.

We contribute new relations to the taxonomy of different

conversions from regular expressions to equivalent finite

automata. In particular, we are interested in

transformations that construct automata such as, the follow

automaton, the partial derivative automaton, the prefix automaton,

the automata based on pointed expressions recently introduced and

studied, and last but not least the position, or Glushkov

automaton (Apos), and their double reversed construction

counterparts. We deepen the understanding of these constructions

and show that with the artefacts used to construct the Glushkov

automaton one is able to capture most of them. As a byproduct we

define a dual version Aposr of the position automaton

which plays a similar role as Apos but now for the reverse

expression. Moreover, it turns out that the prefix

automaton Apre is central to reverse expressions, because

the determinisation of the double reversal of Apre (first

reverse the expression, construct the automaton Apre, and then

reverse the automaton) can be represented as a quotient of any of

the considered deterministic automata that we consider in this

investigation. This shows that although the conversion of

regular expressions and reversal of regular expressions to finite

automata seems quite similar, there are significant differences.

For regular expressions in (strong) star normal form a large set of

efficient algorithms is known, from conversions into finite automata

to characterisations of unambiguity. In this paper we study the

average complexity of this class of expressions using analytic

combinatorics. As it is not always feasible to obtain explicit

expressions for the generating functions involved, here we show how

to get the required information for the asymptotic estimates with an

indirect use of the existence of Puiseux expansions at

singularities. We study, asymptotically and on average, the

alphabetic size, the size of the epsilon-follow automaton and of the position automaton, as well as

the ratio and the size of these expressions to standard regular expressions.

We introduce the concept of an f-maximal error-detecting block code, for some parameter f in (0,1), in order to formalize the situation where a block code is close to maximal with respect to being error-detecting. Our motivation for this is that it is computationally hard to decide whether an error-detecting block code is maximal. We present an output-polynomial time randomized algorithm that takes as input two positive integers N,l and a specification of the errors permitted in some application, and generates an error-detecting, or error-correcting, block code of length l that is fp-maximal, or contains N words with a high likelihood. We model error specifications as (nondeterministic) transducers, which allow one to represent any rational combination of substitution and synchronization errors. We also present some elements of our implementation of various error-detecting properties and their associated methods. Then, we show several tests of the implemented randomized algorithm on various error specifications. A methodological contribution is the presentation of how various desirable error combinations can be expressed formally and processed algorithmically.

We are interested in regular expressions that represent word relations in an alphabet-invariant way—for example, the set of all word pairs u, v where v is a prefix of u independently of what the alphabet is. This is the second part of a recent paper on this topic which focused on labelled graphs (transducers and automata) with alphabet-invariant and user-defined labels. In this paper we study derivatives of regular expressions over labels (atomic objects) in some set B. These labels can be any strings as long as the strings represent subsets of a certain monoid. We show that one can define partial derivative labelled graphs of type B expressions, whose transition labels can be elements of another label set X as long as X and B refer to the same monoid. We also show how to use derivatives directly to decide whether a given word pair is in the relation of a regular expression over pairing specs. Set specs and pairing specs are useful label sets allowing one to express languages and relations over large alphabets in a natural and compact way.

Context-free languages are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma for Context-Free Languages states a property that is valid for all context-free languages, which makes it a tool for showing the existence of non-context-free languages. This paper presents a formalization, extending the previously formalized Lemma, of the fact that several well-known languages are not context-free. Moreover, we build on those results to construct a formal proof of the well-known property that context-free languages are not closed under intersection. All the formalization has been mechanized in the Coq proof assistant.

Descriptional complexity is the study of the conciseness of the various models representing formal languages. The state complexity of a regular language is the size, measured by the number of states of the smallest, either deterministic or nondeterministic, finite automaton that recognises it. Operational state complexity is the study of the state complexity of operations over languages. In this survey, we review the state complexities of individual regularity preserving language operations on regular and some subregular languages. Then we revisit the state complexities of the combination of individual operations. We also review methods of estimation and approximation of state complexity of more complex combined operations

Positions and derivatives are two essential notions in the conversion methods from regular expressions to equivalent finite automata. Partial derivative based methods have recently been extended to regular expressions with intersection (semi-extended). In this paper, we present a position automaton construction for those expressions. This construction generalizes the notion of position, making it compatible with intersection. The resulting automaton is homogeneous and has the partial derivative automaton as a quotient.

The FAdo system is a symbolic manipulator of formal languages objects, implemented in Python. In this work, we extend its capabilities by implementing methods to manipulate transducers and we go one level higher than existing formal language systems and implement methods to manipulate objects representing classes of independent languages (widely known as code properties). Our methods allow users to define their own code properties and combine them between themselves or with fixed properties such as prefix codes, suffix codes, error detecting codes, etc. The satisfaction and maximality decision questions are solvable for any of the definable properties. The new online system LaSer allows to query about code properties and obtain the answer in a batch mode. Our work is founded on independence theory as well as the theory of rational relations and transducers, and contributes with improved algorithms on these objects.

We define the class of forward injective finite automata (FIFA) and study some of their properties. Each FIFA has a unique canonical representation up to isomorphism. Using this representation an enumeration is given and an efficient uniform random generator is presented. We provide a conversion algorithm from a nondeterministic finite automaton or regular expression into an equivalent FIFA. Finally, we present some experimental results comparing the size of FIFA with other automata.

We study the computational power of parsing expression grammars (PEGs). We begin by constructing PEGs with unexpected behaviour, and surprising new examples of languages with PEGs, including the language of palindromes whose length is a power of two, and a binary-counting language. We then propose a new computational model, the scaffolding automaton, and prove that it exactly characterises the computational power of parsing expression grammars (PEGs). Several consequences will follow from this characterisation: (1) we show that PEGs are computationally “universal”, in a certain sense, which implies the existence of a PEG for a P-complete language; (2) we show that there can be no pumping lemma for PEGs; and (3) we show that PEGs are strictly more powerful than online Turing machines which do o(n/(log n)^2) steps of computation per input symbol.

Nondeterministic finite automata with don't care states, namely states which neither accept nor reject, are considered. A characterization of deterministic automata compatible with such a device is obtained. Furthermore, an optimal state bound for the smallest compatible deterministic automata is provided. It is proved that the problem of minimizing deterministic don't care automata is NP-complete and PSPACE-hard in the nondeterministic case. The restriction to the unary case is also considered.

Keywords: Finite automata; Nondeterminism; Don't care automata; Descriptional complexity

For regular expressions in (strong) star normal form a large set of

efficient algorithms is known, from conversions into finite automata

to characterisations of unambiguity. In this paper we study the

average complexity of this class of expressions using analytic

combinatorics. As it is not always feasible to obtain explicit

expressions for the generating functions involved, here we show how

to get the required information for the asymptotic estimates with an

indirect use of the existence of Puiseux expansions at

singularities. We study, asymptotically and on average, the

alphabetic size, the size of the varepsilon-follow automaton and

the ratio of these expressions to standard regular expressions.

Descriptional complexity is

the study of the conciseness of the various models representing formal languages. The state complexity of a regular language is the size, measured by the number of states of the smallest, either deterministic or nondeterministic, finite automaton that recognises it. Operational state complexity is the study of the state complexity of operations over languages.

In this survey, we review the state complexities of individual

regularity preserving language operations on regular and some

subregular languages. Then we revisit the state

complexities of the combination of individual operations. We also review methods of

estimation and approximation of state complexity of more complex

combined operations.

We contribute new relations to the taxonomy of different conversions

from regular expressions to equivalent finite automata. In

particular, we are interested in ordinary transformations that

construct automata such as, the follow automaton, the partial

derivative automaton, the prefix automaton, the automata based on pointed expressions recently introduced and studied, and last but not least the position, or

Glushkov automaton apos, and their double reversed construction

counterparts. We deepen the understanding of these constructions and

show that with the artefacts used to construct the Glushkov automaton one is able to capture most of them. As a byproduct we

define a dual version aposr of the position automaton

which plays a similar role as apos but now for the reverse

expression. It turns out that although the conversion of regular

expressions and reversal of regular expressions to finite automata

seems quite similar, there are significant differences.

Extended regular expressions (with complement and intersection) are used in many applications due to their succinctness. In particular, regular expressions extended with intersection only (also called semi-extended) can already be exponentially smaller than standard regular expressions

or equivalent nondeterministic finite automata.

For practical purposes it is important to study the average behaviour of conversions between these models. In this paper, we focus on the conversion of regular expressions with intersection to nondeterministic finite automata, using partial derivatives and the notion of support. We give a tight upper bound of

2^O(n) for the worst-case number of states of the resulting partial derivative automaton, where n is the size of the expression. Using the framework of analytic combinatorics, we establish an upper bound of (1.056 +o(1))^n for its asymptotic average-state complexity, which is significantly smaller than the one for the worst case. Some experimental results here presented suggest that, on average, the upper bound may not be exponential. Finally, we study the class of semi-extended regular expressions with only one occurrence of intersection at the top level. In this case, the worst-case state complexity of the partial derivative automaton is quadratic on the size of the expression, but we obtained an upper-bound that is, asymptotically and on average, O(n^(3/2)).

We present a randomized algorithm that takes as input two positive

integers N,l and a channel (=specification of the errors permitted), and computes an error-detecting,

or -correcting, block code having up to N codewords of length l.The channel could allow any rational

combination of substitution and synchronization errors.Moreover, if the algorithm finds less than N codewords then those codewords constitute a code that, with high probability, is close to maximal (in a certain precise sense defined here).

We also present some components of an open source Python package in which several code related concepts have been implemented.

A methodological contribution is the presentation of how various error combinations can be expressed formally and processed

algorithmically.

Extended regular expressions (with complement and intersection) are used in many applications due to their succinctness. In particular, regular expressions extended with intersection only (also called semi-extended) can already be exponentially smaller than standard regular expressions

or equivalent nondeterministic finite automata.

For practical purposes it is important to study the average behaviour of conversions between these models. In this paper, we focus on the conversion of regular expressions with intersection to nondeterministic finite automata, using partial derivatives and the notion of support. First, we give a tight upper bound of

2^O(n) for the worst-case number of states of the resulting partial derivative automaton, where n is the size of the expression. Using the framework of analytic combinatorics, we then establish an upper bound of (1.056 +o(1))^n for its asymptotic average-state complexity, which is significantly smaller than the one for the worst case.

The FAdo system is a symbolic manipulator of formal language objects, implemented in Python. In this work, we extend its capabilities by implementing methods to manipulate transducers and we go one level higher than existing formal language systems and implement methods to manipulate objects representing

classes of independent languages (widely known as code properties).

Our methods allow users to define their own code properties and combine them

between themselves or with fixed properties such as prefix codes, suffix codes,

error detecting codes, etc. The satisfaction and maximality decision questions are

solvable for any of the definable properties. The new online system LaSer allows one to query about a code property and obtain the answer in a batch mode.

Our work is founded on independence theory as well as the theory

of rational relations and transducers, and contributes

with improved algorithms on these objects.

This work describes a formalization effort, using the Coq proof assistant, of fundamental results related to the classical theory of context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimi- nation of useless symbols, inaccessible symbols, empty rules and unit rules), the existence of a Chomsky Normal Form for context-free gram- mars and the Pumping Lemma for context-free languages. The result is an important set of libraries covering the main results of context-free language theory, with more than 500 lemmas and theorems fully proved and checked. This is probably the most comprehensive formalization of the classical context-free language theory in the Coq proof assistant done to the present date, and includes the important result that is the formal- ization of the Pumping Lemma for context-free languages.

Positions and derivatives are two essential notions

in the conversion methods from regular expressions

to equivalent finite automata. Partial derivative

based methods have recently been extended to regular

expressions with intersection. In this paper, we

present a position automaton construction for those

expressions. This construction generalizes the

notion of position making it compatible with

intersection. The resulting automaton is homogeneous

and has the partial derivative automaton as its

quotient.

GUItar is a GPL-licensed, cross-platform, graphical

user interface for automata drawing and

manipulation, written in C++ and Qt5. This tool

offers support for styling, automatic layouts,

several format exports and interface with any

foreign finite automata manipulation library that

can parse the serialized XML or JSON produced. In

this paper we describe a new redesign of the GUItar

framework and specially the method used to interface

GUItar with automata manipulation libraries.

We introduce the concept of an f-maximal

error-detecting block code, for some parameter f

between 0 and 1, in order to formalize the situation

where a block code is close to maximal with respect

to being error-detecting. Our motivation for this is

that constructing a maximal error-detecting code is

a computationally hard problem. We present a

randomized algorithm that takes as input two

positive integers N,l, a probability value f,

and a specification of the errors permitted in some

application, and generates an error-detecting, or

error-correcting, block code having up to N

codewords of length l. If the algorithm finds

less than N codewords, then those codewords

constitute a code that is -Maximalf with high

probability. The error specification is modelled as

a (nondeterministic) transducer, which allows one to

model any rational combination of substitution and

synchronization errors. We also present some

elements of our implementation of various

error-detecting properties and their associated

methods. Then, we show several tests of the

implemented randomized algorithm on various error

specifications. A methodological contribution is

the presentation of how various desirable error

combinations can be expressed formally and processed

algorithmically.

The distinguishability language of a regular

language L is the set of words distinguishing

between pairs of words under the Myhill-Nerode

equivalence induced by L, i.e., between pairs of

distinct left quotients of L. The similarity

relation induced by a language L is a similarity

relation inspired by the Myhill-Nerode equivalence

and it was used to obtain compact representation of

automata for a finite language L, i.e.,

deterministic finite cover automata, which are

deterministic finite automata accepting all the

words of L and possibly some other words that are

longer than any word of L. The dissimilarity

language of a finite language L is defined as the

set of words that separate a pair of words which are

not similar w.r.t. to a (finite) language L. In

this paper we extend the study of distinguishability

operation on regular languages to l-dissimilarity,

for linN, and the dissimilarity

operation on finite languages. We examine their

properties, the state complexity, and relations that

can be established between these operations.

Context-free languages are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma is a property that is valid for all context-free languages, and is used to show the existence of non context-free languages. This paper presents a formalization, using the Coq proof assistant, of the Pumping Lemma for context-free languages.

Given a language L, we study the language of words D(L), that distinguish between pairs of different left quotients of L. We characterize this distinguishability operation, show that its iteration has always a fixed point, and we generalize this result to operations derived from closure operators and Boolean operators. For the case of regular languages, we give an upper bound for the state complexity of the distinguishability operation, and prove its tightness. We show that the set of minimal words that can be used to distinguish between different left quotients of a regular language L has at most n -- 1 elements, where n is the state complexity of L, and we also study the properties of its iteration. We generalize the results for the languages of words that distinguish between pairs of different right quotients and two-sided quotients of a language L.

Keywords: Distinguishability, regular languages

Because of their succinctness and clear syntax, regular expressions are the common choice to represent regular languages. Deterministic finite au- tomata are an excellent representation for testing equivalence, containment or membership, as these problems are easily solved for this model. How- ever, minimal deterministic finite automata can be exponentially larger than the associated regular expression, while the corresponding nondeterministic finite automata can be linearly larger. The worst case of both the complexity of the conversion algorithms, and of the size of the resulting automata, are well studied. However, for practical purposes, estimates for the average case can provide much more useful information. In this paper we review recent results on the average size of automata resulting from several constructions and suggest several directions of research. Most results were obtained within the framework of analytic combinatorics.

This paper presents a mechanically verified implementation of an algorithm for deciding the equivalence of Kleene algebra terms within the Coq proof assistant. The algorithm decides equivalence of two given regular expressions through an iterated process of testing the equivalence of their partial derivatives and does not require the construction of the corresponding automata. Recent theoretical and experimental research provides evidence that this method is, on average, more efficient than the classical methods based on automata. We present some performance tests, comparisons with similar approaches, and also introduce a generalization of the algorithm to decide the equivalence of terms of Kleene algebra with tests. The motivation for the work presented in this paper is that of using the libraries developed as trusted frameworks for carrying out certified program verification.

Nondeterministic finite automata with don't care states, namely states which neither accept nor reject, are considered.

A characterization of deterministic automata compatible with such a device is obtained.

Furthermore, an optimal state bound for the smallest compatible deterministic automata is provided.

Finally, it is proved that the problem of minimizing nondeterministic and deterministic don't care automata is NP-complete.

Recently, Yamamoto presented a new method for the conversion from regular expressions (REs) to non-deterministic finite automata (NFA) based on the Thompson ε-NFA (A_T). The A_T automaton has two quotients considered: the suffix automaton A_suf and the prefix automaton, A_pre. Eliminating ε-transitions in A_T, the Glushkov automaton (A_pos) is obtained. Thus, it is easy to see that A_suf and the partial derivative automaton are the same. In this paper, we characterise the A_pre automaton as a solution of a system of left RE equations and express it as a quotient of A_pos by a specific left-invariant equivalence relation. We define and characterise the right-partial derivative automaton. Finally, we study the average size of all these constructions both experimentally and from an analytic combinatorics point of view.

Two language operations that can be expressed by suitable combining complement with

concatenation and star, respectively, are introduced.

The state complexity of those operations on regular languages is investigated.

In the deterministic case, optimal exponential state gaps are proved for both operations.

In the nondeterministic case, for one operation an optimal exponential

gap is also proved, while for the other operation an exponential upper bound is obtained.

We generalize the partial derivative automaton to regular expressions with shuffle and study its size in the worst and in the average case. The number of states of the partial derivative automata is in the worst case at most 2^m, where m is the number of letters in the expression, while asymptotically and on average it is no more than (4/3)^m.

The FAdo system is a symbolic manipulator of formal languages objects, implemented in Python. In this work, we extend its capabilities by implementing methods to manipulate transducers and we go one level higher than existing formal language systems and implement methods to manipulate objects representing classes of independent languages (widely known as code properties). Our methods allow users to define their own code properties and combine them between themselves or with fixed properties such as prefix codes, suffix codes, error detecting codes, etc. The satisfaction and maximality decision questions are solvable for any of the definable properties. The new online system LaSer allows to query about code properties and obtain the answer in a batch mode. Our work is founded on independence theory as well as the theory of rational relations and transducers and contributes with improveded algorithms on these objects.

Synchronous Kleene algebra (ska) is a decidable framework that

combines Kleene algebra (ka) with a synchrony model of concurrency.

Elements of ska can be seen as processes taking place within a

fixed discrete

time frame and that, at each time step, may execute one or more

basic actions or then come to a halt. The synchronous

Kleene algebra with tests (skat) combines ska with a Boolean

algebra. Both algebras were introduced by Prisacariu, who proved the

decidability of the equational theory,

through a Kleene theorem based on the classical Thompson

epsilon-NFA construction. Using the notion of

partial derivatives, we present a new decision

procedure for equivalence between ska terms. The results are extended for skat

considering automata with transitions labeled by Boolean expressions instead of

atoms. This work continous previous research done for ka and kat,

where derivative based methods were used in feasible algorithms

for testing terms equivalence.

The state complexity of basic operations on regular languages considering complete deterministic finite automata (DFA) has been extensively studied in the literature. But, if incomplete DFAs are considered, transition complexity is also an significant measure. In this paper we study the incomplete (deterministic) state and transition complexity of boolean operations, concatenation, star, and reversal for regular languages and finite languages. For all operations we give tight upper bounds for both descriptional measures. For regular languages we give a new tight upper bound for the transition complexity of the union, which refutes the conjecture presented by Y. Gao et al.. For finite languages, we correct the published state complexity of concatenation for complete DFAs and provide a tight upper bound for the case when the right operand is larger than the left one. In general the operational complexities depend not only on the complexities of the operands but also on other refined measures. For both families of languages we present some experimental results to test the behaviour of those operations on the average case, and we conjecture that for many operations and in practical applications the worst-case complexity is seldom reached.

Context-free languages (CFLs) are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma is a property that is valid for all context-free languages, and is used to show the existence of non context-free languages. This paper presents a formalization, using the Coq proof assistant, of the Pumping Lemma for context-free languages.

Context-free language theory is a subject of high importance in computer language processing technology as well as in formal language theory. This paper presents a formalization, using the Coq proof assistant, of fundamental results related to context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimination of useless symbols inaccessible symbols, empty rules and unit rules) and the existence of a Chomsky Normal Form for context-free grammars.

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.

Nowadays, increasing attention is being given to the study of the descrip- tional complexity in 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. Additionally, new asymptotic average-case results for several ε-NFA constructions are presented, in a unified framework. It turns out that, asymptotically, and in the average case, the complexity gap between the several constructions is significantly larger than in the worst case. Furthermore, one of the ε-NFA constructions approaches the corresponding ε-free NFA construction, asymptotically and on average.

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.

Kleene algebra with tests (KAT) is a decidable equational system

for program verification that uses both Kleene and Boolean

algebras. In spite of KAT?s elegance and success in providing theoretical

solutions for several problems, not many efforts have been made towards

obtaining tractable decision procedures that could be used in

practical software verification tools. The main drawback of the

existing methods relies on the explicit use of all possible

assignments to boolean variables.

Recently, Silva introduced an automata model that extends

Glushkov's construction for regular expressions. Broda et al. extended also

Mirkin's equation automata to KAT expressions and studied the

state complexity of both algorithms.

Contrary to other automata

constructions from KAT expressions, these two constructions enjoy the

same descriptional complexity behaviour as their counterparts for

regular expressions, both in the worst case as well as in the

average case.

In this paper, we generalize, for these automata, the

classical methods of subset construction for nondeterministic finite

automata, and the Hopcroft and Karp algorithm for testing deterministic

finite automata equivalence. As a result, we obtain a decision

procedure for KAT equivalence where the extra burden of dealing with

boolean expressions avoids the explicit use of all possible

assignments to the boolean variables. Finally, we specialize the

decision procedure for testing KAT expressions equivalence without

explicitly constructing the automata, by introducing a new notion of

derivative and a new method of constructing the equation automaton.

Minimization of nondeterministic finite automata (NFA) is a hard problem (PSPACE-complete). Bisimulations are then an attrac- tive alternative for reducing the size of NFAs, as even bisimilarity (the largest bisimulation) is almost linear using the Paige and Tarjan algo- rithm. NFAs obtained from REs can have the number of states linear with respect to (w.r.t) the size of the REs and conversion methods from REs to equivalent NFAs can produce NFAs without or with transitions labelled with the empty word (ε-NFA). The standard conversion without ε-transitions is the position automaton, Apos. Other conversions, such as partial derivative (Apd ) automata or follow automata (Af ), were proved to be quotients of the position automata (by some bisimulations). Recent experimental results suggested that for REs in (normalized) star normal form (snf) the position bisimilarity almost coincide with the Apd automaton. Our goal is to have a better characterization of Apd au- tomata and their relation with the bisimilarity of the position automata. In this paper, we consider Apd automata for regular expressions without Kleene star and establish under which conditions it is isomorphic to the bisimilarity of Apos.

In this paper we study the language of the words that, for a given language L, distinguish between pairs of different left-quotients of L. We characterize this distinguishability operation, show that its iteration has always a fixed point, and we generalize this result to operations derived from closure operators and Boolean operators. We give an upper bound for the state complexity of the distinguishability, and prove its tightness. We show that the set of minimal words that can be used to distinguish between different quotients of a language L is n - 1, where n is the state complexity of L. For this operation, we also study the properties of its iteration.

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.

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

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.

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.

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.

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.

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

Dynamic languages, like Python, are attractive

because they guarantee that no correct program is

rejected prematurely. However, this comes at a price

of losing early error detection, and making both

code optimization and certification harder tasks

when compared with static typed languages. Having

the static certification of Python programs as a

goal, we developed a static type inference system

for a subset of Python, known as RPython. Some

dynamic features are absent from RPython,

nevertheless it is powerful enough as a Python

dialect and exhibits most of its main features. Our

type inference system tackles with almost all

language constructions, such as object inheritance

and subtyping, polymorphic and recursive functions,

exceptions, generators, modules, etc., and is itself

written in Python.

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.

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

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.

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.

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.

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

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.

FAdo is an ongoing project which aims to provide a

set of tools for symbolic manipulation of formal

languages. To allow high-level programming with

complex data structures, easy prototyping of

algorithms, and portability (to use in computer grid

systems for example), are its main features. Our

main motivation is the theoretical and experimental

research, but we have also in mind the construction

of a pedagogical tool for teaching automata theory

and formal languages. For the graphical

visualization and interactive manipulation a new

interface application, GUItar, is being developed.

In this paper, we describe the main components of

the FAdo system as well as the basics of the

graphical interface and editor, the export/import

filters and its generic interface with external

systems, such as FAdo.

Computing short regular expressions equivalent to a

given finite automaton is a hard task. In this work

we present a class of acyclic automata for which it

is possible to obtain in time O(n^2logn) an

equivalent regular expression of size O(n). A

characterisation of this class is made using

properties of the underlying digraphs that

correspond to the series-parallel digraphs

class. Using this characterisation we present an

algorithm for the generation of automata of this

class and an enumerative formula for the underlying

digraphs with a given number of vertices.

Computing short regular expressions equivalent to a

given finite automaton is a hard task. In this work

we present a class of acyclic automata for which it

is possible to obtain in time O(n^2logn) an

equivalent regular expression of size O(n). A

characterisation of this class is made using

properties of the underlying digraphs that

correspond to the series-parallel digraphs

class. Using this characterisation we present an

algorithm for the generation of automata of this

class and an enumerative formula for the underlying

digraphs with a given number of vertices.

In this article we describe an implementation of

Kleene algebra with tests (KAT) in the Coq theorem

prover. KAT is an equational system that has been

successfully applied in program verification and, in

particular, it subsumes the propositional Hoare

logic (PHL). We also present an PHL encoding in KAT,

by deriving its deduction rules as theorems of

KAT. Some examples of simple program's formal

correctness are given. This work is part of a study

of the feasibility of using KAT in the automatic

production of certificates in the context of

(source-level) Proof-Carrying-Code (PCC).

We give a canonical representation for minimal

acyclic deterministic finite automata (Madfa) with n

states over an alphabet of k symbols. Using this

normal form, we present a method for the exact

generation of Madfas. This method avoids a rejection

phase that would be needed if a generation algorithm

for a larger class of objects that contains the

Madfas were used. We give upper and lower bounds for

Madfas enumeration and some exact formulas for small

values of n.

We give a canonical representation for trim acyclic

deterministic finite automata (Adfas) with n states

over an alphabet of k symbols. Using this normal

form, we present a backtracking algorithm for the

exact generation of Adfas. This algorithm is a non

trivial adaptation of the algorithm for the exact

generation of minimal acyclic deterministic finite

automata , presented by Almeida et al..

We present an interactive graphical environment for

the manipulation of context-free languages. The

graphical environment allows the editing of a

context-free grammar, the conversion to Chomsky

normal form, word parsing and the (interactive)

construction of parse trees. It is possible to store

positive and negative datasets of words to be tested

by a given grammar. The main goal of this system is

to provide a pedagogical tool for studying grammar

construction and parse trees.

Antimirov and Mosses proposed a rewrite system for

deciding the equivalence of two (extended) regular

expressions. In this paper we present a functional

approach to that method, prove its correctness, and

give some experimental comparative results. Besides

an improved version of AM's algorithm, we present a

version using partial derivatives. Our preliminary

results lead to the conclusion that, indeed, these

methods are feasible and, generally, faster than the

classical methods.

Emotional-BDI agents are BDI agents whose behaviour

is guided not only by beliefs, desires and

intentions, but also by the role of emotions in

reasoning and decision-making. The Ebdi logic is a

formal system for expressing the concepts of the

Emotional-BDI model of agency. In this paper we

present an improved version of the Ebdi logic and

show how it can be used to model the role of three

emotions in Emotional-BDI agents: fear, anxiety and

self-confidence. We also focus in the computational

properties of Ebdi which can lead to its use in

automated proof systems.

The representation of combinatorial objects is

decisive for the feasibility of several enumerative

tasks. In this work, we present a unique string

representation for complete initially-connected

deterministic automata (ICDFAs) with n states over

an alphabet of k symbols. For these strings we give

a regular expression and show how they are adequate

for exact and random generation, allow an

alternative way for enumeration and lead to an upper

bound for the number of ICDFAs. The exact generation

algorithm can be used to partition the set of ICDFAs

in order to parallelize the counting of minimal

automata, and thus of regular languages. A uniform

random generator for ICDFAs is presented that uses a

table of pre-calculated values. Based on the same

table, an optimal coding for ICDFAs is obtained.

In general, the representation of combinatorial

objects is decisive for the feasibility of several

enumerative tasks. In this work, we show how a

(unique) string representation for (complete)

initially-connected deterministic automata (ICDFA's)

with n states over an alphabet of k symbols can be

used for counting, exact enumeration, sampling and

optimal coding, not only the set of ICDFA's but, to

some extent, the set of regular languages. An exact

generation algorithm can be used to partition the

set of ICDFA's in order to parallelize the counting

of minimal automata (and thus of regular languages).

We present also a uniform random generator for

ICDFA's that uses a table of pre-calculated values.

Based on the same table it is also possible to

obtain an optimal coding for ICDFA's.

Emotional-BDI agents are agents whose behaviour is

guided not only by beliefs, desires and intentions,

but also by the role of emotions in reasoning and

decision-making. In this paper we introduce the

logic logic for specifying Emotional-BDI agents in

general and a special kind of Emotional-BDI agent

under the effect of fear. The focus of this work is

in the expressiveness of logic and on using it to

establish some properties which agents under the

effect of an emotion should exhibit.

We present a conditional rewrite system for

arithmetic and membership univariate constraints

over real numbers, designed for computer assisted

learning (CAL) in elementary math. Two fundamental

principles guided the design of the proposed rewrite

rules: cognitive fidelity (emulating steps students

should take) and correctness, aiming that

step-by-step solutions to problems look like ones

carried out by students. In order to gain more

flexibility to modify rules, add new ones and

customize solvers, the rules are written in a

specification language and then compiled to Prolog.

The rewrite system is complete for a relevant subset

of problems found in high-school math textbooks.

Keywords: e-learning,XML, integrated knowledge

management,automatic assessement

FAdo is an ongoing project which aims the

development of an interactive environment for

symbolic manipulation of formal languages. In this

paper we focus in the description of interactive

tools for teaching and assisting research on regular

languages, and in particular finite automata and

regular expressions. Those tools implement most

standard automata operations, conversion between

automata and regular expressions, and word

recognition. We illustrate their use in training and

automatic assessment. Finally we present a graphical

environment for editing and interactive

visualisation.

Keywords: Automata theory, Interactive visual tools,

e-learning

We propose a web-based timetabling system for a

typical situation in universities, where agents

(usually departments or faculties) compete for a set

of resources (class rooms) on a given number of time

slots. Each agent (typically a person, on the

behalf of a department) proposes the placement (room

and time) for events. A dispatching system decides

which event should be scheduled next, based on a

pre-established set of rules, and asks its placement

to the corresponding department. The system also

includes a solver that suggests the placement of an

event to each agent, thus allowing a completely

automated timetable construction. We describe a

prototype being implemented at the Faculty of

Sciences, University of Porto.

Keywords: Automata theory, Interactive visual tools,

e-learning

Teaching the very basic concepts of a computer

architecture, instruction set and operation based on

a real microprocessor is usually an unfruitful task

as the essential notions are obscured by the

specific details of its architecture. A machine

emulator has the benefit of providing a portable

environment that can be run in several platforms and

that can be easily adapted for pedagogical

purposes. Apoo is a virtual machine with a very

simple architecture and instruction set that mimics

almost all the essential features of a modern

microprocessor. The Apooi is an graphical

environment that monitors the state of the machine

during the execution of a program and allows the

writing/editing/execution of programs in assembly

language. The Apoot is a module that aims the

grading of student programs based on a description

of what should be the execution of the program for

specified input data sets. This module was used to

evaluate students programming skills in an

interactive learning/grading system, not only

allowing the detection of errors but trying to give

extra information in order that the student could

understand and correct his/her mistakes more

easily.

Keywords: teaching, assembly language

In recent years, symbolic constraints have raised a

considerable interest in several areas of

computation and particularly in the Computational

Linguistics community. As a matter of fact

constraints over the algebra of rational trees can

significantly contribute to the reduction of the

search space of problems in Natural Language

Processing, while increasing the formalisms

expressive power. In this thesis we developed a

formal and computational framework for constraint

languages over the algebras of finite, rational and

feature trees. Although, the first-order theories of

these algebras are decidable, they are

computationally intractable. Our goal was to design

a formal model and decision procedures to face that

problem, and that have been (successfully) used in

the implementation of several grammar formalisms,

called Constraint Logic Grammars (CLG). The main

contributions of this thesis are: Complete solvers

for complex constraints in the algebras of finite

and rational trees. In order to face the NP-hardness

of the satisfiability problem for complex

constraints, our approach was based in factoring

out, in polynomial time, deterministic information

contained in a complex constraint, simplifying the

remaining formula using that information and

delaying as much as possible the explosion of

disjunctions. We also developed rewrite systems for

detection of common factors in disjuncts and rewrite

systems that use negative information for the

simplification process. We investigated the problem

of eliminating negative constraints and presented a

decision procedure for finite signatures;

Establishment of a relation between the algebra of

rational trees and the algebra of feature trees,

such that the satisfiability problem in one can be

reduced to the satisfiability problem in the other:

A method for the computation of the minimal models

of certain classes of satisfiable constraints. These

characterizations are useful to simplify and to

detect equivalent constraints; A low-level

implementation of the main features of the complete

solvers; A higher order tree descriptions Calculus

based on a typed lambda-calculus, which extended the

previous techniques developed for resolving complex

constraints. The higher order tree descriptions were

used as semantic representations in categorial

grammars for Natural Language.

Although unification can be used to implement a weak

form of beta-reduction, several linguistic phenomena

are better handled by using some form of

lambda-calculus. In this paper we present a higher

order feature description calculus based on a typed

lambda-calculus. We show how the techniques used in

CLG for resolving complex feature constraints can

be efficiently extended. CCLG is a simple

formalism, based on categorial grammars, designed to

test the practical feasibility of such a calculus.

This work presents a constraint solver for the

domain of rational trees. Since the problem is

NP-hard the strategy used by the solver is to reduce

as much as possible, in polynomial time, the size of

the constraints using a rewriting system before

applying a complete algorithm. This rewriting system

works essentially by rewriting constraints using the

information in a partial model. An efficient C

implementation of the rewriting system is described

and an algorithm for factoring complex constraints

is also presented.

We present an algorithm for decidibility of formulas

over the Herbrand Universe with an infinite

alphabet, based on rewriting rules and quantifier

elimination.

In this paper a model for temporal references in

natural language (NL) is studied and a Prolog

implementation of it is presented. This model is

intended to be a common framework for semantic

analysis of verb tenses and temporal adverbial

phrases. The time model choosen was based on time

intervals and temporal relations. The notion of

“proposition type” and temporal concepts of tense,

aspect, duration, location and iteration were

represented as temporal relations between some

special time intervals and temporal quantifiers over

time intervals. The implementation consisted in

extending an existing semantic analyser.

Keywords: Natural Language Understanding