Publications
[152] 
Stavros Konstantinidis, Casey Meijer, Nelma Moreira, and Rogério Reis.
Symbolic manipulation of code properties.
Journal of Automata, Languages and Combinatorics,
23(13):243269, 2018.
[ DOI 
.pdf ]
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.

[151] 
Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis.
Position automata for semiextended expressions.
Journal of Automata, Languages and Combinatorics,
23(13):3965, 2018.
[ DOI 
.pdf ]
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 (semiextended). 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.

[150] 
Sabine Broda, António Machiavelo Nelma Moreira, and Rogério Reis.
Automata for regular expressions with shuffle.
Information and Computation, 259:162173, 2018.
[ DOI 
.pdf ]
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

[149] 
Rafaela Bastos, Sabine Broda, António Machiavelo, Nelma Moreira, and
Rogério Reis.
On the state complexity of partial derivative automata for
semiextended expressions.
Journal of Automata, Languages and Combinatorics,
22(13):528, 2017.
[ DOI 
.pdf ]
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 semiextended) 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 worstcase 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 averagestate 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 semiextended regular expressions with only one occurrence of intersection at the top level. In this case, the worstcase state complexity of the partial derivative automaton is quadratic on the size of the expression, but we obtained an upperbound that is, asymptotically and on average, O(n^(3/2)).

[148] 
Sabine Broda, Markus Holzer, Eva Maia, Nelma Moreira, and Rogério Reis.
On the mother of all automata: The position automaton.
In Émilie Charlier, Julien Leroy, and Michel Rigo, editors,
21st DLT 2017, volume 10396 of LNCS, pages 134146. Springer,
2017.
[ DOI 
.pdf ]
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.

[147]  Stavros Konstantinidis, Nelma Moreira, Rogério Reis, and Jeffrey Shallit, editors. The Role of Theory in Computer Science: Essays Dedicated to Janusz Brzozowski. World Scientific, 2017. ISBN 9789813148192. [ http ] 
[146] 
Yuan Gao, Nelma Moreira, Rogério Reis, and Sheng Yu.
A survey on operational state complexity.
Journal of Automata, Languages and Combinatorics,
21(4):251310, 2017.
[ DOI 
.pdf ]
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.

[145] 
Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis.
On the average complexity of strong star normal form.
In Cezar Câmpeanu and Giovanni Pighizzini, editors,
Description Complexity of Formal Systems (DCFS 2017), volume 10316 of
LNCS, pages 7788. Springer, 2017.
[ DOI 
.pdf ]
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 εfollow automaton and the ratio of these expressions to standard regular expressions.

[144] 
Nelma Moreira, Giovanni Pighizzini, and Rogério Reis.
Optimal state reductions of automata with partially specified
behaviors.
Theoretical Computer Science, 658:235245, January 2017.
[ DOI 
.pdf ]
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 NPcomplete and PSPACEhard in the nondeterministic case. The restriction to the unary case is also considered. Keywords: Finite automata; Nondeterminism; Don't care automata; Descriptional complexity 
[143] 
Cezar Câmpeanu, Nelma Moreira, and Rogério Reis.
Distinguishability operations and closures.
Fundamenta Informaticae, 148(34):243266, 2016.
[ DOI 
.pdf ]
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 twosided quotients of a language L. Keywords: Distinguishability, regular languages 
[142] 
Marcus Vinícius Midena Ramos, José Carlos Bacelar Almeida, Nelma
Moreira, and Ruy José Guerra Barretto de Queiroz.
Formalization of the pumping lemma for contextfree languages.
J. Formalized Reasoning, 9(2):5368, 2016.
[ DOI 
http ]
Contextfree 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 contextfree languages, and is used to show the existence of non contextfree languages. This paper presents a formalization, using the Coq proof assistant, of the Pumping Lemma for contextfree languages.

[141] 
Cezar Câmpeanu, Nelma Moreira, and Rogério Reis.
On the dissimilarity operation on finite languages.
In Henning Bordihn, Rudolf Freund, Benedek Nagy, and György Vaszil,
editors, Eighth Workshop on NonClassical Models of Automata and
Applications (NCMA 2016), volume 321, pages 105120. Österreichische
Computer Gesellschaft, 2016.
[ .pdf ]
The distinguishability language of a regular language L is the set of words distinguishing between pairs of words under the MyhillNerode 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 MyhillNerode 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 ldissimilarity, 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.

[140] 
Stavros Konstantinidis, Nelma Moreira, and Rogério Reis.
Generating error control codes with automata and transducers.
In Henning Bordihn, Rudolf Freund, Benedek Nagy, and György Vaszil,
editors, Eighth Workshop on NonClassical Models of Automata and
Applications (NCMA 2016), volume 321, pages 211226. Österreichische
Computer Gesellschaft, 2016.
[ .pdf ]
We introduce the concept of an fmaximal errordetecting 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 errordetecting. Our motivation for this is that constructing a maximal errordetecting 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 errordetecting, or errorcorrecting, 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 errordetecting 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.

[139] 
Miguel Ferreira, Nelma Moreira, and Rogério Reis.
Automata Serialization for Manipulation and Drawing.
In Marjan Mernik, José Paulo Leal, and Hugo Gonçalo
Oliveira, editors, 5th Symposium on Languages, Applications and
Technologies (SLATE'16), volume 51 of OpenAccess Series in Informatics
(OASIcs), pages 17, Dagstuhl, Germany, 2016. Schloss
DagstuhlLeibnizZentrum fuer Informatik.
[ DOI 
http ]
GUItar is a GPLlicensed, crossplatform, 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.

[138] 
Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis.
Position automaton construction for regular expressions with
intersection.
In Srecko Brlek and Christophe Reutenauer, editors, Developments
in Language Theory  20th International Conference, DLT 2016,
Montréal, Canada, July 2528, 2016, Proceedings, volume 9840, pages
5163, 2016.
[ DOI 
.pdf ]
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.

[137] 
Marcus Ramos, Ruy De Queiroz, Nelma Moreira, and José Bacelar Almeida.
On the formalization of some results of contextfree language theory.
In Jouko A. Väänänen, Åsa Hirvonen, and Ruy J.
G. B. de Queiroz, editors, Workshop on Logic, Language, Information and
Computation (WoLLIC 2016), volume 9803 of LNCS, pages 338357.
Springer, 2016.
[ DOI ]
This work describes a formalization effort, using the Coq proof assistant, of fundamental results related to the classical theory of contextfree 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 contextfree gram mars and the Pumping Lemma for contextfree languages. The result is an important set of libraries covering the main results of contextfree language theory, with more than 500 lemmas and theorems fully proved and checked. This is probably the most comprehensive formalization of the classical contextfree 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 contextfree languages.

[136] 
Stavros Konstantinidis, Casey Meijer, Nelma Moreira, and Rogério Reis.
Implementation of code properties via transducers.
In Implementation and Application of Automata, 21th
International Conference (CIAA 2016), 2016.
[ DOI 
.pdf ]
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.

[135] 
Rafaela Bastos, Sabine Broda, António Machiavelo, Nelma Moreira, and
Rogério Reis.
On the state complexity of partial derivative automata for regular
expressions with intersection.
In Proceedings of the 18th Int. Workshop on Descriptional
Complexity of Formal Systems (DCFS16), volume 9777 of LNCS, pages
4559. Springer, 2016.
[ DOI 
.pdf ]
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 semiextended) 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 worstcase 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 averagestate complexity, which is significantly smaller than the one for the worst case.

[134] 
Stavros Konstantinidis, Nelma Moreira, and Rogério Reis.
Channels with synchronization/substitution errors and computation of
error control codes.
Preprint, 2016.
[ http ]
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 errordetecting, 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.

[133] 
Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis.
Average size of automata constructions from regular expressions.
Bulletin of the European Association for Theoretical Computer
Science, 116:167192, June 2015.
[ http ]
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.

[132] 
Marcus V. M. Ramos, Ruy J. G. B. de Queiroz, Nelma Moreira, and José
Carlos Bacelar Almeida.
Formalization of contextfree language theory.
Preprint, 2015.
[ http ]
Contextfree 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 contextfree 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 contextfree grammars.

[131] 
Marcus V. M. Ramos, Ruy J. G. B. de Queiroz, Nelma Moreira, and José
Carlos Bacelar Almeida.
Formalization of the pumping lemma for contextfree languages.
Preprint, 2015.
[ http ]
Contextfree 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 contextfree languages, and is used to show the existence of non contextfree languages. This paper presents a formalization, using the Coq proof assistant, of the Pumping Lemma for contextfree languages.

[130]  Rudolf Freund, Markus Holzer, Nelma Moreira, and Rogério Reis, editors. Seventh Workshop on NonClassical Models of Automata and Applications (NCMA 2015). Österreichische Computer Gesellschaft, 2015. ISBN 9783903035072. 
[129] 
Eva Maia, Nelma Moreira, and Rogério Reis.
Incomplete transition complexity on finite and infinite regular
languages.
Information and Computation, 244:122, 2015.
[ DOI 
http ]
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 worstcase complexity is seldom reached.

[128] 
Sabine Broda, Sílvia Cavadas, Miguel Ferreira, and Nelma Moreira.
Deciding synchronous kleene algebra with derivatives.
In Frank Drewes, editor, Implementation and Application of
Automata, 20th International Conference (CIAA 2015), volume 9223 of
LNCS, pages 4962. SpringerVerlag, 2015.
[ DOI 
.pdf ]
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 epsilonNFA 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.

[127] 
Stavros Konstantinidis, Casey Meijer, Nelma Moreira, and Rogério Reis.
Symbolic manipulation of code properties.
Preprint, 2015.
[ http ]
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.

[126] 
Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis.
Partial derivative automaton for regular expressions with shuffle.
In Jeffrey Shallit and Alexander Okhotin, editors, Proceedings
of the 17th Int. Workshop on Descriptional Complexity of Formal Systems
(DCFS15), number 9118 in LNCS, pages 2132. Springer, 2015.
[ DOI 
http ]
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}.

[125] 
Nelma Moreira, Giovanni Pighizzini, and Rogério Reis.
Universal disjunctive concatenation and star.
In Jeffrey Shallit and Alexander Okhotin, editors, Proceedings
of the 17th Int. Workshop on Descriptional Complexity of Formal Systems
(DCFS15), number 9118 in LNCS, pages 197208. Springer, 2015.
[ DOI 
http ]
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.

[124] 
Eva Maia, Nelma Moreira, and Rogério Reis.
Prefix and rightpartial derivative automata.
In Mariya Soskova and Victor Mitrana, editors, Computability in
Europe (CiE 2015), number 9136 in LNCS, pages 258267. Springer, 2015.
[ DOI 
.pdf ]
Recently, Yamamoto presented a new method for the conversion from regular expressions (REs) to nondeterministic 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 leftinvariant equivalence relation. We define and characterise the rightpartial derivative automaton. Finally, we study the average size of all these constructions both experimentally and from an analytic combinatorics point of view.

[123] 
Nelma Moreira, Giovanni Pighizzini, and Rogério Reis.
Optimal state reductions of automata with partially specified
behaviors.
In 41st SOFSEM  the International Conference on Current Trends
in Theory and Practice of Computer Science, number 8939 in LNCS, pages
339351. Springer, 2015.
[ DOI 
http ]
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 NPcomplete.

[122] 
Nelma Moreira, David Pereira, and Sim ao Melo de Sousa.
Deciding Kleene algebra terms (in)equivalence in Coq.
Journal of Logical and Algebraic Methods in Programming,
84(3):377401, 2015.
[ DOI ]
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.

[121]  Sabine Broda, Sílvia Cavadas, and Nelma Moreira. Kleene algebra completeness. Technical Report DCC201407, DCCFC & CMUP, Universidade do Porto, July 2014. [ .pdf ] 
[120]  Sabine Broda, Sílvia Cavadas, and Nelma Moreira. Derivative based methods for deciding ska and skat. Technical Report DCC201410, DCCFC & CMUP, Universidade do Porto, May 2014. [ .pdf ] 
[119] 
Cezar Câmpeanu, Nelma Moreira, and Rogério Reis.
The distinguishability operation on regular languages.
In Suna Bensch, Rudolf Freund, and Friedrich Otto, editors,
NonClassical Models of Automata and Applications (NCMA 2014), pages
85100. Oesterreichische Computer Gesellschaft, 2014.
[ .pdf ]
In this paper we study the language of the words that, for a given language L, distinguish between pairs of different leftquotients 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.

[118] 
Eva Maia, Nelma Moreira, and Rogério Reis.
Partial derivative and position bisimilarity automata.
In Markus Holzer and Martin Kutrib, editors, Implementation and
Application of Automata, 19th International Conference (CIAA 2014), volume
8587 of LNCS, pages 264277. SpringerVerlag, 2014.
[ DOI 
.pdf ]
Minimization of nondeterministic finite automata (NFA) is a hard problem (PSPACEcomplete). 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.

[117] 
Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis.
On the Equivalence of Automata for KATexpressions.
In Arnold Beckmann, Erzsébet CsuhajVarjú, and Klaus Meer,
editors, Language, Life, Limits  10th Conference on Computability in
Europe, CiE 2014, Budapest, Hungary, June 2327, 2014. Proceedings, volume
8493 of LNCS, pages 7383. SpringerVerlag, 2014.
[ DOI 
.pdf ]
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.

[116]  Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis. Automata for KAT Expressions. Technical Report DCC201401, DCCFC, Universidade do Porto, January 2014. [ .pdf ] 
[115] 
Jason Bell, Janusz Brzozowski, Nelma Moreira, and Rogério Reis.
Symmetric groups and quotient complexity of boolean operations.
In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias
Koutsoupias, editors, Automata, Languages, and Programming  41st
International Colloquium, ICALP 2014, Copenhagen, Denmark, July 811, 2014,
Proceedings, Part II, volume 8573 of Lecture Notes on Computer
Science, pages 112, 2014.
[ DOI 
.pdf ]
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 nontrivial connection between complexity of boolean operations and group theory.

[114] 
Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis.
A hitchhiker's guide to descriptional complexity through analytic
combinatorics.
Theoretical Computer Science, 528(0):85  100, 2014.
[ DOI 
http ]
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 averagecase 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.

[113] 
Marco Almeida, Nelma Moreira, and Rogério Reis.
Incremental dfa minimisation.
RAIRO  Theoretical Informatics and Applications,
48(2):173186, 2014.
[ DOI 
http ]
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.

[112]  Rafaela Bastos, Nelma Moreira, and Rogério Reis. Manipulation of extended regular expressions with derivatives. Technical Report DCC201311, DCCFC, Universidade do Porto, September 2013. [ .pdf ] 
[111]  Nelma Moreira and Rogério Reis. Preface. Special Issue  Implementation and Application of Automata (CIAA 2012). International Journal of Fundations of Computer Science, 24(06):689690, September 2013. [ DOI ] 
[110]  Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis. Glushkov and Equation Automata for KAT Expressions. Technical Report DCC201307, DCCFC, Universidade do Porto, July 2013. [ .pdf ] 
[109]  Davide Nabais, Nelma Moreira, and Rogério Reis. Desco: a knowledge based system for descriptional complexity of formal languages. Technical Report DCC201312, DCCFC Universidade do Porto, July 2013. [ .pdf ] 
[108]  Ricardo Almeida, Sabine Broda, and Nelma Moreira. Kat and Hoare logic with derivatives. Technical Report DCC201304, DCC  FC & CMUP, Universidade do Porto, February 2013. [ .pdf ] 
[107]  Yuan Gao, Nelma Moreira, Rogério Reis, and Sheng Yu. A survey on state complexity. (Submitted), 2013. [ http ] 
[106] 
Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis.
On the average size of Glushkov and equation automata for KAT
expressions.
In 19th International Symposium on Fundamentals of Computation
Theory, number 8070 in LNCS, pages 7283. SpringerVerlag, 2013.
[ DOI 
.pdf ]
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 worstcase as well as in the averagecase. 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.

[105]  Eva Maia, Nelma Moreira, and Rogério Reis. The operational incomplete transition complexity on finite languages. Technical Report DCC201302, DCC  FC & CMUP, Universidade do Porto, January 2013. [ .pdf ] 
[104] 
Eva Maia, Nelma Moreira, and Rogério Reis.
Incomplete transition complexity of basic operations on finite
languages.
In Stavros Konstantinidis, editor, Implementation and
Application of Automata, 18th International Conference (CIAA 2013), number
7982 in LNCS, pages 349356. SpringerVerlag, 2013.
[ DOI 
.pdf ]
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.

[103] 
Eva Maia, Nelma Moreira, and Rogério Reis.
Incomplete transition complexity of some basic operations.
In Peter van Emde Boas, Frans C.A. Groen, Giuseppe F. Italiano, Jerzy
Nawrocki, and Harald Sack, editors, SOFSEM 2013: Theory and Practice of
Computer Science, number 7741 in Lecture Notes on Computer Science, pages
319330. SpringerVerlag, 2013.
MR3074101.
[ DOI 
.pdf ]
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..

[102] 
Nelma Moreira, David Pereira, and Sim ao Melo de Sousa.
On the mechanisation of relyguarantee in Coq.
Technical Report DCC201303, DCC  FC & LIACC, Universidade do
Porto, January 2013.
[ .pdf ]
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 smallstep 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? RelyGuarantee reasoning and in the logic of Coq.

[101]  Nelma Moreira, Davide Nabais, and Rogério Reis. Desco: a web based information system for descriptional complexity results. Technical Report DCC201303, DCCFC, Universidade do Porto, 2013. [ .pdf ] 
[100]  Marco Almeida, Nelma Moreira, and Rogério Reis. Finite automata minimization algorithms. In Jiacun Wang, editor, Handbook of Finite State Based Models and Applications, Discrete Mathematics and Its Applications, pages 145170. Chapman and Hall/CRC Press, November 2012. MR3014621. [ http ] 
[99] 
Ricardo Almeida, Sabine Broda, and Nelma Moreira.
Deciding KAT and Hoare logic with derivatives.
In 3rd International Symposium on Games, Automata, Logics, and
Formal Verification, Proceedings, volume 96, page 127?140, Napoli, Italy,
September 2012. Electronic Proceedings in Theoretical Computer Science.
[ DOI 
.pdf ]
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.

[98]  Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis. An introduction to descriptional complexity of regular languages through analytic combinatorics. Technical Report DCC201205, DCC  FC, Universidade do Porto, July 2012. [ .pdf ] 
[97]  Nelma Moreira and Rogério Reis, editors. Implementation and Application of Automata, 17th International Conference (CIAA 2012), volume 7381 of LNCS, Porto, Portugal, July 2012. Springer. ISBN 9783642316050. MR3059553. [ DOI  http ] 
[96]  Martin Kutrib, Nelma Moreira, and Rogério Reis, editors. Descriptional Complexity of Formal Systems, 14th International Workshop (DCFS 2012), volume 7386 of LNCS, Braga, Portugal, July 2012. Springer. ISBN 9783642316227. MR3087301. [ DOI  http ] 
[95]  Nelma Moreira, David Pereira, and Sim ao Melo de Sousa. Mechanization of an algorithm for deciding KAT terms equivalence. Technical Report DCC201204, DCCFC, Universidade do Porto, May 2012. [ .pdf ] 
[94]  Eva Maia, Nelma Moreira, and Rogério Reis. On the incomplete transition complexity of some basic operations on regular languages. Technical Report DCC201202, DCCFC, Universidade do Porto, April 2012. [ .pdf ] 
[93]  Rizó Isrof, Nelma Moreira, and Rogério Reis. GUITAR: Graphical User Interface Tool for Automata Representation. In Actas do IJUP. Universidade do Porto, 2012. [ .pdf ] 
[92]  Jürgen Dassow, Martin Kutrib, Nelma Moreira, and Rogério Reis. Preface. Selected papers of DCFS 2012. Journal of Automata, Languages and Combinatorics, 17(24):5960, 2012. [ .html ] 
[91] 
David Pereira Nelma Moreira and Sim ao Melo de Sousa.
Deciding regular expressions (in)equivalence in Coq.
In T. G. Griffin and W. Kahl, editors, 13th International
Conference on Relational and Algebraic Methods in Computer Science (RAMiCS
13). Proceedings, volume 7560 of Lecture Notes on Computer Science,
pages 98113. SpringerVerlag, 2012.
MR3040160.
[ DOI 
.pdf ]
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 inequivalence 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.

[90] 
Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis.
On the average size of Glushkov and partial derivative automata.
International Journal of Foundations of Computer Science,
23(5):969984, 2012.
MR2983363.
[ DOI 
.pdf ]
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.

[89]  Yuan Gao, Nelma Moreira, Rogério Reis, and Sheng Yu. A review on state complexity of individual operations. Technical Report dcc201108, DCC  FC, Universidade do Porto,, December 2011. [ .pdf ] 
[88]  Marco Almeida, Nelma Moreira, and Rogério Reis. Incremental dfa minimisation. In Michael Domaratzki and Kai Salomaa, editors, Proceedings of the 15th International Conference on Implementation and Application of Automata (CIAA 2010), number 6482 in Lecture Notes on Computer Science, pages 3948, Winnipeg, MA, Canada, August 2011. SpringerVerlag. MR2776275. [ DOI  .pdf ] 
[87] 
José Bacelar Almeida, Nelma Moreira, David Pereira, and Sim ao Melo de
Sousa.
Partial derivative automata formalized in Coq.
In Michael Domaratzki and Kai Salomaa, editors, Proceedings of
the 15th International Conference on Implementation and Application of
Automata (CIAA 2010), number 6482 in Lecture Notes on Computer Science,
pages 5968, Winnipeg, MA, Canada, August 2011. SpringerVerlag.
MR2776277.
[ DOI 
.pdf ]
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.

[86] 
Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis.
The average transition complexity of Glushkov and partial
derivative automata.
In G. Mauri and A. Leporati, editors, Developments in Language
Theory, 15th International Conference, DLT 2011, Milano, Italy, July 2011.
Proceedings, volume 6795 of Lecture Notes on Computer Science, pages
93104, Milano, Italy, July 2011. SpringerVerlag.
MR2862718.
[ DOI 
.pdf ]
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.

[85] 
Cezar Câmpeanu, Nelma Moreira, and Rogério Reis.
Expected compression ratio for dfca: experimental average case.
Technical Report DCC201107, DCCFC, Universidade do Porto, January
2011.
[ .pdf ]
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, suffixfree 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 
[84]  Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis. Study of the average size of Glushkov and partial derivative automata. Technical Report DCC201103, DCCFC, Universidade do Porto, 2011. [ .pdf ] 
[83] 
Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis.
On the average state complexity of partial derivative automata: an
analytic combinatorics approach.
International Journal of Foundations of Computer Science,
22(7):15931606, 2011.
MR2865339.
[ DOI 
.pdf ]
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.

[82] 
Eva Maia, Nelma Moreira, and Rogério Reis.
A static type inference for Python.
In Proc. of DYLA'11, 5th Workshop on Dynamic Languages and
Applications, colocated with 49th Intl Conf on Objects, Models, Components
and Patterns (TOOLS 2011) July 1, 2011, Zürich, Switzerland, 2011.
[ .pdf ]
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.

[81]  Nelma Moreira, David Pereira, and Sim ao Melo de Sousa. Deciding regular expressions (in)equivalence in coq. Technical Report DCC201106, DCCFC, Universidade do Porto, 2011. 
[80]  Nelma Moreira, Davide Nabais, and Rogério Reis. DesCo: a web based information system for descriptional complexity results. Technical Report DCC201110, DCCFC, Universidade do Porto, 2011. [ .pdf ] 
[79] 
André Almeida, Nelma Moreira, and Rogério Reis.
GUItar and FAgoo: Graphical interface for automata visualization,
editing, and interaction.
In Luís S. Barbosa and Miguel P. Correia, editors, Inforum,
Simpósio de Informática, pages 317328, Braga,Portugal, September
2010.
Also at
http://inforum.org.pt/INForum2010/papers/computacaografica/Paper038.pdf.
[ .pdf ]
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.

[78]  Eva Maia, Nelma Moreira, and Rogério Reis. Inferência de tipos em Python. In Luís S. Barbosa and Miguel P. Correia, editors, Inforum, Simpósio de Informática, pages 515518, Braga,Portugal, September 2010. Also at http://inforum.org.pt/INForum2010/papers/especificacaoverificacaoetestesistemascriticos/Paper040.pdf. [ .pdf ] 
[77]  André Almeida, Nelma Moreira, and Rogério Reis. GUItar and FAgoo: Graphical interface for automata visualization, editing, and interaction. In Luís S. Barbosa and Miguel P. Correia, editors, Inforum, Simpósio de Informática, pages 317328, Braga, Portugal, September 2010. 
[76] 
Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis.
On the average number of states of partial derivative automata.
In Yuan Gao, Hanlin Lu, Shinnosuke Seki, and Sheng Yu, editors,
Developments in Language Theory, 14th International Conference, DLT 2010,
London, ON, Canada, August 1720, 2010. Proceedings, volume 6224 of
Lecture Notes on Computer Science, pages 112123, London, ON, Canada,
August 2010. SpringerVerlag.
MR2725637.
[ DOI 
.pdf ]
The partial derivative automaton (NFA_Pd) 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 (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.

[75] 
Nelma Moreira, Davide Nabais, and Rogério Reis.
State elimination ordering strategies: Some experimental results.
In I. MacQuillan, G. Pighizzini, and B. Trost, editors, Proc. of
11th Workshop on Descriptional Complexity of Formal Systems (DCFS10), pages
169180, Saskatoon, Saskatchewan,Canada, August 2010.
[ DOI 
.pdf ]
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 blowup in the worstcase. 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.

[74] 
Hugo Gouveia, Nelma Moreira, and Rogério Reis.
Small nfas from regular expressions: Some experimental results.
In Fernando Ferreira, Hélia Guerra, Elvira Mayordomo, and Jo ao
Rasga, editors, Proceedings of 6th Conference on Computability in Europe
(CIE 2010), pages 194203, Ponta Delgada, Azores, Portugal, June 2010.
CMATI.
Also at ArXiv: http://arxiv.org/abs/1009.3599.
[ .pdf ]
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 epsilonfree 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.

[73] 
Marco Almeida, Nelma Moreira, and Rogério Reis.
Testing equivalence of regular languages.
Journal of Automata, Languages and Combinatorics,
15(1/2):725, 2010.
[ .pdf ]
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 bestcase running time, present an extension to nondeterministic 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.

[72] 
José Alves, Nelma Moreira, and Rogério Reis.
XML description for automata manipulations.
In Alberto Sim oes, Daniela Cruz, and José Carlos Ramalho,
editors, Actas XATA 2010, XML: aplicações e tecnologias
associadas, pages 7788, ESEIG, Vila do Conde, 2010.
Also in http://hdl.handle.net/1822/10637.
[ .pdf ]
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.

[71]  Sabine Broda, António Machiavelo, Nelma Moreira, and Rogério Reis. On the average size of pd automata: an analytic combinatorics approach. Technical Report DCC201004, DCCFC, Universidade do Porto, 2010. [ .html ] 
[70]  André Carvalho, Nuno Silva, Sim ao Melo de Sousa, and Nelma Moreira. A tool for automatic model extraction of Ada/SPARK programs. Technical Report DCC201005, DCCFC, Universidade do Porto, 2010. [ .html ] 
[69]  Marco Almeida, Nelma Moreira, and Rogério Reis. Antimirov and Mosses' rewrite system revisited. International Journal of Foundations of Computer Science, 20(4):669684, August 2009. MR2555761. [ DOI  .pdf ] 
[68] 
André Almeida, Marco Almeida, José Alves, Nelma Moreira, and Rogério
Reis.
Fado and guitar: tools for automata manipulation and visualization.
In S. Maneth, editor, CIAA 2009: Fourteenth International
Conference on Implementation and Application of Automata, volume 5642 of
Lecture Notes on Computer Science, pages 6574, Sydney, Australia,
July 2009. SpringerVerlag.
[ DOI 
.pdf ]
FAdo is an ongoing project which aims to provide a set of tools for symbolic manipulation of formal languages. To allow highlevel 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.

[67]  Marco Almeida, Nelma Moreira, and Rogério Reis. Testing equivalence of regular languages. In Workshop on Descriptional Complexity of Formal Systems (DCFS09), Magdeburg, Germany, July 2009. Also in Electronic Proceedings in Theoretical Computer Science (eptcs 3) http://www.eptcs.org. [ DOI  .pdf ] 
[66]  Marco Almeida, Nelma Moreira, and Rogério Reis. Testing equivalence of regular languages. Technical Report DCC200901, DCCFC&LIACC, Universidade do Porto, 2009. [ .html ] 
[65] 
Nelma Moreira and Rogério Reis.
Seriesparallel automata and short regular expressions.
Fundamenta Informaticae, 91(34):611629, 2009.
[ DOI 
.pdf ]
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 seriesparallel 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.

[64]  Nelma Moreira, David Pereira, and Sim ao Melo de Sousa. On the Mechanization of Kleene Algebra in Coq. Technical Report Dcc200903, DCCFC&LIACC, Universidade do Porto, 2009. [ .html ] 
[63] 
Nelma Moreira and Rogério Reis.
Seriesparallel automata and short regular expressions.
Fundamenta Informaticae, 91(34):611629, 2009.
MR2518215.
[ DOI 
.pdf ]
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 seriesparallel 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.

[62] 
David Pereira and Nelma Moreira.
KAT and PHL in COQ.
Computer Science and Information Systems, 05(02), December
2008.
ISSN: 18200214.
[ .pdf ]
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 (sourcelevel) ProofCarryingCode (PCC).

[61] 
Marco Almeida, Nelma Moreira, and Rogério Reis.
Exact generation of minimal acyclic deterministic finite automata.
International Journal of Foundations of Computer Science,
19(4):751765, August 2008.
MR2437812.
[ DOI 
.pdf ]
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.

[60] 
Marco Almeida, Nelma Moreira, and Rogério Reis.
Antimirov and Mosses's rewrite system revisited.
In O. Ibarra and B. Ravikumar, editors, CIAA 2008: Thirteenth
International Conference on Implementation and Application of Automata,
Lecture Notes on Computer Science, pages 4656, San Francisco, CA, USA, July
2008. SpringerVerlag.
MR2504697.
[ DOI 
.pdf ]
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.

[59] 
André Almeida, José Alves, Nelma Moreira, and Rogério Reis.
Cgm: A contextfree grammar manipulator.
In Corta 08, Bragança, Portugal, July 2008.
[ .pdf ]
We present an interactive graphical environment for the manipulation of contextfree languages. The graphical environment allows the editing of a contextfree 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.

[58] 
Marco Almeida, Nelma Moreira, and Rogério Reis.
Exact generation of acyclic deterministic finite automata.
In Workshop on Descriptional Complexity of Formal Systems
(DCFS08), Charlottetown, Canada, July 2008.
[ .pdf ]
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..

[57]  David Pereira and Nelma Moreira. KAT and PHL in COQ. In Corta 08, Bragança, Portugal, July 2008. [ .pdf ] 
[56]  Marco Almeida, Nelma Moreira, and Rogério Reis. On the performance of automata minimization algorithms. In Arnold Beckmann, Costas Dimitracopoulos, and Benedikt Löwe, editors, CiE 2008: Abstracts and extended abstracts of unpublished papers., 2008. [ .pdf ] 
[55]  Silvestre Lacerda, Norberto Lopes, Nelma Moreira, and Rogério Reis. A toolkit for an oral history digital archive. In José Carlos Ramalho and Jo ao Correia Lopes, editors, Actas XATA 2008, XML: aplicações e tecnologias associadas, pages 4051, Universidade de Évora, 2008. [ .pdf ] 
[54] 
David Pereira, Eugénio Oliveira, and Nelma Moreira.
Formal modelling of emotions in bdi agents.
In F. Sadri and K. Satoh, editors, Eighth Workshop on
Computational Logic in MultiAgent Systems (CLIMAVIII), number 5056 in
LNAI, pages 6281, Porto, Portugal, 2008. SpringerVerlag.
[ .pdf ]
EmotionalBDI 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 decisionmaking. The Ebdi logic is a formal system for expressing the concepts of the EmotionalBDI 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 EmotionalBDI agents: fear, anxiety and selfconfidence. We also focus in the computational properties of Ebdi which can lead to its use in automated proof systems.

[53]  Marco Almeida, Nelma Moreira, and Rogério Reis. Testing regular expressions equivalence. Technical Report DCC200707, DCC  FC, Universidade do Porto, October 2007. [ .pdf ] 
[52]  David Pereira, Eugénio Oliveira, and Nelma Moreira. Formal modelling of emotions in bdi agents. In Eighth Workshop on Computational Logic in MultiAgent Systems (CLIMAVIII), Porto, Portugal, September 2007. For a extended version see Technical Report [48]. [ .pdf ] 
[51]  Marco Almeida, Nelma Moreira, and Rogério Reis. Exact generation of minimal acyclic deterministic finite automata. In Workshop on Descriptional Complexity of Formal Systems (DCFS07), pages 5768, High Tatras, Slovakia, July 2007. [ .pdf ] 
[50]  Marco Almeida, Nelma Moreira, and Rogério Reis. On the performance of automata minimization algorithms. Technical Report DCC200703, DCC  FC & LIACC, Universidade do Porto, June 2007. [ .pdf ] 
[49]  Marco Almeida, Nelma Moreira, and Rogério Reis. Exact generation of minimal acyclic deterministic finite automata. Technical Report DCC200705, DCC  FC & LIACC, Universidade do Porto, June 2007. [ .pdf ] 
[48]  David Pereira, Eugénio Oliveira, and Nelma Moreira. Formal modelling of emotions in bdi agents. Technical Report DCC200704, DCC  FC & LIACC, Universidade do Porto, June 2007. [ .pdf ] 
[47]  Silvestre Lacerda, Norberto Lopes, Nelma Moreira, and Rogério Reis. Ferramentas para a construção de arquivos digitais de história oral. In Luís Carriço José Carlos Ramalho, João Correia Lopes, editor, Actas XATA 2007, XML: aplicações e tecnologias associadas. Universidade de Lisboa, February 2007. 
[46] 
Marco Almeida, Nelma Moreira, and Rogério Reis.
Enumeration and generation with a string automata representation.
Theoretical Computer Science, 387(2):93102, 2007.
MR2362181.
[ DOI 
.pdf ]
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 initiallyconnected 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 precalculated values. Based on the same table, an optimal coding for ICDFAs is obtained.

[45]  J. Barbosa, J. Caramelo, J. Cunha, A. Ferreira, S. Lacerda, N. Lopes, M. Loff, M. Matias, T. Medina, B. Monteiro, N. Moreira, C. Nogueira, R. Reis, I. Ribeiro, J. Rocha, C. F. Silva, and C. R. Silva. Education and language in memories of labour. Poster in “Investugação Científica na PréGraduação”, Universidade do Porto, 2007. 
[44]  Marco Almeida, Nelma Moreira, and Rogério Reis. Enumeration and generation of initially connected deterministic finite automata. Technical Report DCC200607, DCCFC & LIACC, Universidade do Porto, December 2006. [ .pdf ] 
[43] 
Marco Almeida, Nelma Moreira, and Rogério Reis.
Aspects of enumeration and generation with a string automata
representation.
In H. Leung and G.Pighizzini, editors, Proceedings of the 8th
Int. Workshop on Descriptional Complexity of Formal Systems (DCFS06), number
NMSUCS2006001 in Computer Science Technical Report, pages 5869, Las
Cruces, New Mexico, June 2006. NMSU.
[ .pdf ]
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) initiallyconnected 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 precalculated values. Based on the same table it is also possible to obtain an optimal coding for ICDFA's.

[42] 
Ana Paula Tomás, Nelma Moreira, and Nuno Pereira.
Designing a solver for arithmetic constraints to support education in
mathematics.
In IFIP Conference on Artificial Intelligence Applications &
Innovations (AIAI) 2006. SpringerVerlag, 2006.
IFIP Conference on Artificial Intelligence Applications &
Innovations (AIAI) 2006 , Athens, Greece.
[ .pdf ]
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 stepbystep 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 highschool math textbooks.

[41] 
David Pereira, Eugénio Oliveira, and Nelma Moreira.
Modelling emotional bdi agents.
In Workshop on Formal Approaches to MultiAgent Systems (FAMAS
2006), Riva del Garda, Italy, 2006.
[ .pdf ]
EmotionalBDI agents are agents whose behaviour is guided not only by beliefs, desires and intentions, but also by the role of emotions in reasoning and decisionmaking. In this paper we introduce the logic logic for specifying EmotionalBDI agents in general and a special kind of EmotionalBDI 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.

[40]  David Pereira, Eugénio Oliveira, Nelma Moreira, and Luís Sarmento. Towards an architecture for emotional bdi agents. In Amílcar Cardoso Carlos Bento and Gaël Dias, editors, EPIA05  12th Portuguese Conference on Artificial Intelligence, pages 4046. Universidade da Beira Interior, IEEE, December 2005. ISBN 0780393651. [ .pdf ] 
[39]  David Pereira, Eugénio Oliveira, and Nelma Moreira. Towards an architecture for emotional bdi agents. Technical Report DCC200509, DCC  FC & LIACC, Universidade do Porto, July 2005. [ .pdf ] 
[38]  José João Morais, Nelma Moreira, and Rogério Reis. Acyclic automata with easytofind short regular expressions. In Igor Litovshy Jacques Farré and Sylvain Schmitz, editors, CIAA 2005, Tenth International Conference on Implementation and Application of Automata, volume 3845 of Lecture Notes on Computer Science, pages 349350, SophiaAnthiopolis, France, June 2005. SpringerVerlag. Also in Preproceedings of Tenth International Conference on Implementation and Application of Automata (CIAA05). [ .pdf ] 
[37]  Rogério Reis, Nelma Moreira, and Marco Almeida. On the representation of finite automata. In G. Pighizzini C. Mereghetti, B. Palano and D. Wotschkes, editors, Proceedings of the 7th Int. Workshop on Descriptional Complexity of Formal Systems (DCFS05), pages 269276, Como, Italy, June 2005. For a extended version see Technical Report [35]. [ .pdf ] 
[36]  Ana Paula Tomás, Nelma Moreira, and Nuno Pereira. Designing a symbolic solver for arithmetic constraints for computer assisted learning. Technical Report DCC200506, DCC  FC & LIACC, Universidade do Porto, May 2005. [ .pdf ] 
[35]  Marco Almeida, Nelma Moreira, and Rogério Reis. On the representation of finite automata. Technical Report DCC200504, DCC  FC & LIACC, Universidade do Porto, April 2005. [ .pdf ] 
[34]  José João Morais, Nelma Moreira, and Rogério Reis. Acyclic automata with easytofind short regular expressions. Technical Report DCC200503, ,DCCFC& LIACC, Universidade do Porto, April 2005. [ .pdf ] 
[33]  Nelma Moreira and Rogério Reis. On the density of languages representing finite set partitions. Journal of Integer Sequences, 8(05.2.8), 2005. MR2152288. [ .html ] 
[32]  Nelma Moreira and Rogério Reis. Fado:interactive tools for learning formal computational models. In Encontro Nacional de Visualização Científica, Centro Multimeios de Espinho, 2005. http://envc2005.multimeios.pt. [ .pdf ] 
[31] 
Nelma Moreira and Rogério Reis.
Interactive manipulation of regular objects with FAdo.
In Proceedings of 2005 Innovation and Technology in Computer
Science Education (ITiCSE 2005). ACM, 2005.
Based on Technical Report [25].
[ .pdf ]
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, elearning 
[30] 
Ângela Oliveira and Nelma Moreira.
Gerexa: Plataforma integrada para a organização,
geração e avaliação de exercícios e testes.
In Actas da 3a Conferência Nacional XML: Aplicações e
Tecnologias Associadas. Universidade do Minho, 2005.
[ .pdf ]
Keywords: elearning,XML, integrated knowledge management,automatic assessement 
[29]  Nelma Moreira and Rogério Reis. On the density of languages representing finite set partitions. Technical Report DCC200407, DCCFC& LIACC, Universidade do Porto, August 2004. [ .pdf ] 
[28]  Rogério Reis, Nelma Moreira, and Jo ao Pedro Pedroso. Educated bruteforce to get h(4). Technical Report DCC200404, DCCFC& LIACC, Universidade do Porto, July 2004. [ .pdf ] 
[27] 
Jo ao Pedro Pedroso, Nelma Moreira, and Rogério Reis.
A webbased system for multiagent interactive timetabling.
In ICKEDS 2004, First International Conference on Knowledge
Engineering and Decision Support, Porto,2123 of July, 2004.
[ .pdf ]
We propose a webbased 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 preestablished 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.

[26]  Rogério Reis and Nelma Moreira. Yappy: Yet another LR(1) parser generator for Python. DCCFC & LIACC, Universidade do Porto, Portugal, 2003. http://www.ncc.up.pt/fado/Yappy/. [ .pdf ] 
[25] 
Rogério Reis and Nelma Moreira.
FAdo:tools for finite automata and regular expressions
manipulation.
Technical Report DCC20022, DCCFC& LIACC, Universidade do Porto,
August 2002.
[ .pdf ]
Keywords: Automata theory, Interactive visual tools, elearning 
[24]  Rogério Reis and Nelma Moreira. Apoo: an environment for a first course in assembly language programming. SIGCSE Bulletin (ACM Special Interest Group on Computer Science Education), 33(2), December 2001. Extended version available as Technical Report [19]. 
[23]  Nelma Moreira José Paulo Leal and Pedro Ribeiro. EDIC: Uma abordagem para apresentação de conteúdos pedagógicos na web. Technical Report DCC20015, DCC  FC & LIACC, Universidade do Porto, July 2001. [ .ps.gz ] 
[22]  Nelma Moreira José Paulo Leal and Pedro Ribeiro. Edic: Uma abordagem para apresentação de conteúdos pedagógicos na web. In Proceedings of the International Conference on New Technologies in Science Education (resumos), CINTEC 2001, page 86, Aveiro, 2001. Extended version available as Technical Report [23]. 
[21]  José Paulo Leal and Nelma Moreira. Using matching for automatic assessment in computer science learning environments. In Francisco Restivo and Lígia Ribeiro, editors, WebBased Lerning Environments, pages 7072. Merlin 2000 Project, FEUP Edições, June 2000. Extended version available as Technical Report [20]. 
[20]  José Paulo Leal and Nelma Moreira. Using matching for automatic assessment in computer science learning environments. Technical Report DCC20003, DCC  FC & LIACC, Universidade do Porto, 2000. [ .ps.gz ] 
[19] 
Rogério Reis and Nelma Moreira.
Apoo: an environment for a first course in assembly language
programming.
Technical Report DCC989, DCCFC& LIACC, Universidade do Porto,
1998.
[ .pdf.gz ]
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 
[18]  José Paulo Leal and Nelma Moreira. Automatic grading of programming exercises. Technical Report DCC984, DCC  FC & LIACC, Universidade do Porto, 1998. [ .ps.gz ] 
[17] 
Nelma Moreira.
Resolution of Complex Constraints on Trees and Applications in
Logic Grammars.
PhD thesis, Universidade do Porto, 1997.
(In Portuguese).
[ .ps.gz ]
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 firstorder 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 NPhardness 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 lowlevel implementation of the main features of the complete solvers; A higher order tree descriptions Calculus based on a typed lambdacalculus, 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.

[16] 
Luís Damas and Nelma Moreira.
Constraint categorial grammars.
In Nuno Mamede and Carlos PintoFereira, editors, EPIA 95,
volume 990 of Lecture Notes in Artificial Intelligence.
SpringerVerlag, 1995.
MR1390070.
[ .ps.gz ]
Although unification can be used to implement a weak form of betareduction, several linguistic phenomena are better handled by using some form of lambdacalculus. In this paper we present a higher order feature description calculus based on a typed lambdacalculus. 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.

[15]  Luís Damas, Nelma Moreira, and Giovanni B. Varile. The formal and computational theory of complex constraint solution. In C. Rupp, M. A. Rosner, and R. L. Johnson, editors, Constraints, Language, and Computation, Computation in Cognitive Science, pages 149166. Academic Press, London, 1994. [ .pdf ] 
[14]  Luís Damas, Nelma Moreira, and Giovanni Varile. CLG: Constraint logic grammar. In Rolf Backofen, HansUlrich Krieger, S. Spackman, and Hans Uszkoreit, editors, Report of the EAGLES workshop on implemented formalisms at DFKI, pages 4041. DFKI, Saarbrücken, March 1993. 
[13]  Luís Damas and Nelma Moreira. CC(L)G: constraint categorial grammars. In Rolf Backofen, HansUlrich Krieger, S. Spackman, and Hans Uszkoreit, editors, Report of the EAGLES workshop on implemented formalisms at DFKI, pages 2628. DFKI, Saarbrücken, March 1993. 
[12] 
Luís Damas, Nelma Moreira, and Sabine Broda.
Resolution of constraints in algebras of rational trees.
In Miguel Filgueiras and Luís Damas, editors, Progress in
Artificial Intelligence  6th Portuguese Conference on Artificial
Intelligence (EPIA 93), volume 727 of Lecture Notes in Artificial
Intelligence, pages 6176. SpringerVerlag, 1993.
MR1291450.
[ .pdf ]
This work presents a constraint solver for the domain of rational trees. Since the problem is NPhard 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.

[11] 
Luís Damas and Nelma Moreira.
A quantifier elimination algorithm for a first order logic with
equality.
Technical report, Centro de Informática da Universidade do Porto,
July 1991.
[ .pdf ]
We present an algorithm for decidibility of formulas over the Herbrand Universe with an infinite alphabet, based on rewriting rules and quantifier elimination.

[10]  Luís Damas, Nelma Moreira, and Giovanni B. Varile. The formal and processing models of CLG. In Fifth Conference of the European Chapter of the Association for Computational Linguistics, pages 173178, Berlin, 1991. [ .pdf ] 
[9]  José Paulo Leal, Luís Damas, and Nelma Moreira. A history based interface. In Proceedings of the ICLP preconference Workshop on Logic Programming Environments, Paris, 1991. 
[8]  Miguel Filgueiras, N. Moreira, and A. P. Tomás. General introduction. In Filgueiras et al. [7], pages 13. MR1102026. 
[7]  Miguel Filgueiras, L. Damas, N. Moreira, and A. P. Tomás, editors. Natural Language Processing  EAIA '90 Proceedings. Number 476 in Lecture Notes in Artificial Intelligence. SpringerVerlag, 1991. Reviewed in Math Reviews, 91k:68015; 03B65 68S05. Reviewed in Zentralblatt für Mathematik, 875.00077; 00B25, 6806, 68S05, 68T99. 
[6]  M. Filgueiras, A.P. Tomás, N. Moreira, J.P. Leal, and R.Reis. Natural language and natural menus interfaces. In Preprints of the TC7 IFIP International Conference Modelling the Innovation, Roma, March 1990. Also in M. Carnevale, M. Lucërtini, S. Nicosia (eds.), “Modelling the Innovation: Communications, Automation and Information Systems”, NorthHolland, 1990. 
[5]  Sergio Balari, Luís Damas, Nelma Moreira, and Giovanni B. Varile. CLG(n): Constraint logic grammars. In H.Karlgren, editor, Proceedings of the 13th International Conference on Computational Linguistics (COLING), volume 3, pages 712, Helsinki, 1990. [ .pdf ] 
[4] 
Nelma Moreira.
Semantic analysis of time and tense in natural language: an
implementation.
In J.P Martins and E.M. Morgado, editors, Proceedings of the 4th
Portuguese Conference of Artificial Inteligence, number 390 in LNAI, Berlin,
1989. SpringerVerlag.
[ .pdf ]
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 
[3]  Nelma Moreira. Representação de semântica de referências temporais em linguagem natural. Master's thesis, Universidade do Porto, October 1988. Apresentado à Universidade do Porto no âmbito das Provas de Aptidão Pedagógica e Capacidade Científica. 
[2]  Isabel Labouriau and Nelma Moreira. Third order derivative of degenerate Hopf bifurcation in normal form. Technical report, Grupo de Matemática Aplicada da Faculdade de Ciências da Universidade do Porto, 1986. 
[1]  Isabel Labouriau e Nelma Moreira. Soluções periódicas das equações de Fitzhugh para o impulso nervoso. In Actas do VII Congresso do Grupo de Matemáticos de Expressão Latina, 1985. 
This file was generated by bibtex2html 1.98.