Jorge Almeida (Centro de Matemática da Universidade do Porto)
Factoriality and the Pin-Reutenauer procedure
Separating two regular languages by a regular language of a given type can be viewed as a topological separation problem in the associated profinite completion of the free semigroup on the underlying alphabet. For algorithmic considerations, it is better to work in an intermediate free algebra that is sufficiently rich to capture non-emptiness of the intersection of the closures of two regular languages. For this purpose, we consider "implicit signatures" on finite semigroups determined by sets of pseudonatural numbers. It turns out that, under relatively mild hypotheses on a pseudovariety V of semigroups, a finitely generated free algebra for the largest such signature is closed under taking factors within the free pro-V semigroup. Using similar techniques, we show that the natural analog of the Pin-Reutenauer descriptive procedure for the closure of a regular language in a free group holds for the pseudovariety of all finite semigroups. It follows that the Pin-Reutenauer procedure holds for a pseudovariety of semigroups with respect to the signature consisting of multiplication and pseudo-inversion if and only if the pseudovariety is full with respect to this signature.
(Joint work with J. C. Costa and M. Zeitoun.)
Separating two regular languages by a regular language of a given type can be viewed as a topological separation problem in the associated profinite completion of the free semigroup on the underlying alphabet. For algorithmic considerations, it is better to work in an intermediate free algebra that is sufficiently rich to capture non-emptiness of the intersection of the closures of two regular languages. For this purpose, we consider "implicit signatures" on finite semigroups determined by sets of pseudonatural numbers. It turns out that, under relatively mild hypotheses on a pseudovariety V of semigroups, a finitely generated free algebra for the largest such signature is closed under taking factors within the free pro-V semigroup. Using similar techniques, we show that the natural analog of the Pin-Reutenauer descriptive procedure for the closure of a regular language in a free group holds for the pseudovariety of all finite semigroups. It follows that the Pin-Reutenauer procedure holds for a pseudovariety of semigroups with respect to the signature consisting of multiplication and pseudo-inversion if and only if the pseudovariety is full with respect to this signature.
(Joint work with J. C. Costa and M. Zeitoun.)
Ivone Amorim (Centro de Matemática da Universidade do Porto)
Counting non-equivalent linear finite transducers
In the 80's and 90's a family of public key cryptosystems based on finite transducers were proposed, the so called FAPKCs. To generate a pair of keys in these systems, it is necessary to randomly produce a linear finite transducer (LFT) with an adequate kind of injectivity. As far as we know, no study was previously conducted to address the problem of counting non-equivalent LFTs to evaluate the effective strength of these systems.
In this talk we describe a canonical form for LFTs so that every LFT is equivalent to exactly one canonical transducer, which can then be used to generate all the equivalent LFTs of a given size. This allows to calculate the size of each equivalence class on the set of the LFTs with the same size. From this we derive a recurrence relation that gives the number of non-equivalent LFTs of a given size.
In the 80's and 90's a family of public key cryptosystems based on finite transducers were proposed, the so called FAPKCs. To generate a pair of keys in these systems, it is necessary to randomly produce a linear finite transducer (LFT) with an adequate kind of injectivity. As far as we know, no study was previously conducted to address the problem of counting non-equivalent LFTs to evaluate the effective strength of these systems.
In this talk we describe a canonical form for LFTs so that every LFT is equivalent to exactly one canonical transducer, which can then be used to generate all the equivalent LFTs of a given size. This allows to calculate the size of each equivalence class on the set of the LFTs with the same size. From this we derive a recurrence relation that gives the number of non-equivalent LFTs of a given size.
Manuel Delgado (Centro de Matemática da Universidade do Porto)
Some questions on numerical semigroups
Let \(S\) be a numerical semigroup, i.e. a co-finite submonoid of the non-negative integers, under addition.
For an introduction on numerical semigroups, see a [book] by Rosales and García-Sánchez.
An integer $x$ is said to be the Frobenius number of \(S\) (respectively, a pseudo-Frobenius number of \(S\)) if \(x\not\in S\) and \(x+s\in S\), for all positive integer \(s\) (respectively, for all \(s\in S\)). We denote by \(F(S)\) the Frobenius number of \(S\) and by \(PF(S)\) the set of pseudo-Frobenius numbers of \(S\).
Given a positive integer \(f\), there exists a numerical semigroup \(S\) such that \(F(S)=f\). One example of such a semigroup is the semigroup \(\{0,f+1,\to\}\) containing \(0\) and all the integers greater than \(f\).
There exist fast algorithms to compute all the numerical semigroups with a given Frobenius number.
Let \(PF = \{g_1,g_2,\ldots,g_{n-1}, g_n\}\) be a set of positive integers. Some questions arise naturally.
1- Find conditions on the set \(PF\) that ensure the existence of a numerical semigroup \(S\) such that \(PF(S)=PF\).
2- Compute all the numerical semigroups that have \(PF\) as its set of pseudo-Frobenius numbers.
This kind of questions have been addressed by A. Robles-Pérez and J.C. Rosales for numerical semigroups of type 2 and are part of ongoing work with P. A. García-Sánchez and A. Robles-Pérez.
We will illustrate the use of the package [numericalsgps] to get some insight on how to handle these and some other natural questions on numerical semigroups.
[book] J. C. Rosales and P. A. García-Sánchez, "Numerical Semigroups", Developments in Maths. 20, Springer (2010).
[numericalsgps] M. Delgado, P. A. García-Sánchez and J. Morais, "numericalsgps": a GAP package to compute with numerical semigroups. Version number 0.980 (Released 17/06/2013)
Let \(S\) be a numerical semigroup, i.e. a co-finite submonoid of the non-negative integers, under addition.
For an introduction on numerical semigroups, see a [book] by Rosales and García-Sánchez.
An integer $x$ is said to be the Frobenius number of \(S\) (respectively, a pseudo-Frobenius number of \(S\)) if \(x\not\in S\) and \(x+s\in S\), for all positive integer \(s\) (respectively, for all \(s\in S\)). We denote by \(F(S)\) the Frobenius number of \(S\) and by \(PF(S)\) the set of pseudo-Frobenius numbers of \(S\).
Given a positive integer \(f\), there exists a numerical semigroup \(S\) such that \(F(S)=f\). One example of such a semigroup is the semigroup \(\{0,f+1,\to\}\) containing \(0\) and all the integers greater than \(f\).
There exist fast algorithms to compute all the numerical semigroups with a given Frobenius number.
Let \(PF = \{g_1,g_2,\ldots,g_{n-1}, g_n\}\) be a set of positive integers. Some questions arise naturally.
1- Find conditions on the set \(PF\) that ensure the existence of a numerical semigroup \(S\) such that \(PF(S)=PF\).
2- Compute all the numerical semigroups that have \(PF\) as its set of pseudo-Frobenius numbers.
This kind of questions have been addressed by A. Robles-Pérez and J.C. Rosales for numerical semigroups of type 2 and are part of ongoing work with P. A. García-Sánchez and A. Robles-Pérez.
We will illustrate the use of the package [numericalsgps] to get some insight on how to handle these and some other natural questions on numerical semigroups.
[book] J. C. Rosales and P. A. García-Sánchez, "Numerical Semigroups", Developments in Maths. 20, Springer (2010).
[numericalsgps] M. Delgado, P. A. García-Sánchez and J. Morais, "numericalsgps": a GAP package to compute with numerical semigroups. Version number 0.980 (Released 17/06/2013)
Markus Holzer (Institut für Informatik Universität Gießen)
Some Aspects on Biautomata
Biautomata were recently introduced in [KlPo12] as a generalization of ordinary deterministic finite automata. Simply speaking, a biautomaton is a device consisting of a deterministic finite control, a read-only input tape, and two reading heads, one reading the input from left to right, and the other head reading the input from right to left. Similar two-head finite automata models were introduced, e.g., in [CDJM13a,Lo07,Ro67]. An input word is accepted by a biautomaton, if there is an accepting computation starting the heads on the two ends of the word meeting somewhere in an accepting state. Although the choice of reading a symbol by either head is nondeterministic, a deterministic outcome of the computation is enforced by two properties: (i) The heads read input symbols independently, i.e., if one head reads a symbol and the other reads another, the resulting state does not depend on the order in which the heads read these single letters. (ii) If in a state of the finite control one head accepts a symbol, then this letter is accepted in this state by the other head as well. Later we call the former property the $\diamond$-property and the latter one the \(F\)-property.
We summarize some results on biautomata: (i) In [KlPo12] it was shown that biautomata share a lot of properties with ordinary deterministic finite automata. For instance, there is a unique (up to isomorphism) minimal deterministic biautomaton for every regular language, which obeys a nice description in terms of two-sided derivatives or quotients-cf. Brzozowski's construction for ordinary minimal deterministic finite automata [Br64]. (ii) Simple structural characterizations based on biautomata for language families such as the piecewise testable or prefix-suffix testable languages were given in [KlPo12]. Moreover, further characterizations of commutative and circular shift closed regular languages were obtained in [HoJa13c]. (iii) Recently in [JiKl12] also descriptional complexity issues for biautomata were addressed and in [HoJa13a] biautomata were generalized to deal with nondeterminism. The role of the \(\diamond\)- and the \(F\)-property for descriptional complexity issues is briefly discussed in [HoJa13a]. (iv) Further investigations concern computational aspects of biautomata. Starting with the complexity of minimization algorithms [HoJa13c] up to the question, on the computational complexity of variants of equivalence problems on biautomata [HoJa14] were recently considered. Here it is worth mentioning that he most elegant minimization algorithm, that is, that of Brzozowski [Br62], which minimizes an ordinary finite automaton \(A\), regardless whether it is deterministic or nondeterministic, by applying the reversal and power-set construction atwice in sequence, also works for biautomata. On the other hand biautomata can also be significantly different to ordinary finite automata as, e.g., shown in [HoJa14], where it was proven that computing a hyper-minimal biautomata is computational intractable, namely the problem is NP-complete. Here an automaton is hyper-minimal if it admits no smaller almost equivalent automaton of same type, where two automata are almost equivalent if the symmetric difference of their languages is finite. This task is polynomial time solvable in case of ordinary deterministic finite automata [HoMa10]. Some of the presented results were obtained together with co-author Sebastian Jakobi.
[Br62]
J. A. Brzozowski. Canonical regular expressions and minimal state graphs for definite events. In Mathematical Theory of Automata, volume 12 of MRI Symposia Series], pages 529--561. Polytechnic Press, NY, 1962.
[Br64]
J. A. Brzozowski. Derivatives of regular expressions. J. ACM, 11:481--494, 1964.
[CDJM13a]
J.-M. Champarnaud, J.-P. Dubernard, H. Jeanne, and L. Mignot. Two-sided derivatives for regular expressions and for hairpin expressions. In A.-H.dediu, C. Martín-Vide, and B. Truthe, editors, Proceedings of the $7$th International Conference on Language and Automata Theory and Applications, number 7810 in LNCS, pages 202--213, Bilbao, Spain 2013. Springer.
[HoJa13c]
M. Holzer and S. Jakobi. Minimization and characterizations for biautomata. In S. Bensch, F. Drewes, R. Freund, and F. Otto, editors, Proceedings of the 5th International Workshop on Non-Classical Models of Automata and Applications, number 294 in books$@$ocg.at, pages 179--193, Umea, Sweden, 2013. Österreichische Computer Gesellschaft.
[HoJa13a]
M. Holzer and S. Jakobi. Nondeterministic biautomata and their descriptional complexity. In H. Jürgensen and R. Reis, editors, Proceedings of the 15th International Workshop on Descriptional Complexity of Formal Systems, number 8031 in LNCS, pages 112--123, London, Ontario, Canada, 2013. Springer.
[HoJa14]
M. Holzer and S. Jakobi.
On the complexity of some computational problems on biautomata, 2014. Manuscript in preparation.
[HoMa10]
M. Holzer and A. Maletti. An \(n\log n\) algorithm for hyper-minimizing a (minimized) deterministic automaton. Theoret. Comput. Sci., 411(38--39):3404--3413, 2010.
[JiKl12]
G. Jiráková and O. Klíma. Descriptional complexity of biautomata. In M. Kutrib, N. Moreira, and R. Reis, editors, Proceedings of the 14th International Workshop Descriptional Complexity of Formal Systems, number 7386 in LNCS, pages 196--208, Braga, Portugal, 2012. Springer.
[KlPo12]
O. Klíma and L. Polák. On biautomata. RAIRO--Informatique théorique et Applications / Theoretical Informatics and Applications, 46(4):573--592, 2012.
[Lo07]
R. Loukanova.
Linear context free languages. In C. B. Jones, Z. Liu, and J. Woodcock, editors, Proceedings of the 4th International Colloquium Theoretical Aspects of Computing, number 4711 in LNCS, pages 351--365, Macau, China, 2007. Springer.
[Ro67]
A. L. Rosenberg. A machine realization of the linear context-free languages. Inform. Control, 10:175--188, 1967.
Biautomata were recently introduced in [KlPo12] as a generalization of ordinary deterministic finite automata. Simply speaking, a biautomaton is a device consisting of a deterministic finite control, a read-only input tape, and two reading heads, one reading the input from left to right, and the other head reading the input from right to left. Similar two-head finite automata models were introduced, e.g., in [CDJM13a,Lo07,Ro67]. An input word is accepted by a biautomaton, if there is an accepting computation starting the heads on the two ends of the word meeting somewhere in an accepting state. Although the choice of reading a symbol by either head is nondeterministic, a deterministic outcome of the computation is enforced by two properties: (i) The heads read input symbols independently, i.e., if one head reads a symbol and the other reads another, the resulting state does not depend on the order in which the heads read these single letters. (ii) If in a state of the finite control one head accepts a symbol, then this letter is accepted in this state by the other head as well. Later we call the former property the $\diamond$-property and the latter one the \(F\)-property.
We summarize some results on biautomata: (i) In [KlPo12] it was shown that biautomata share a lot of properties with ordinary deterministic finite automata. For instance, there is a unique (up to isomorphism) minimal deterministic biautomaton for every regular language, which obeys a nice description in terms of two-sided derivatives or quotients-cf. Brzozowski's construction for ordinary minimal deterministic finite automata [Br64]. (ii) Simple structural characterizations based on biautomata for language families such as the piecewise testable or prefix-suffix testable languages were given in [KlPo12]. Moreover, further characterizations of commutative and circular shift closed regular languages were obtained in [HoJa13c]. (iii) Recently in [JiKl12] also descriptional complexity issues for biautomata were addressed and in [HoJa13a] biautomata were generalized to deal with nondeterminism. The role of the \(\diamond\)- and the \(F\)-property for descriptional complexity issues is briefly discussed in [HoJa13a]. (iv) Further investigations concern computational aspects of biautomata. Starting with the complexity of minimization algorithms [HoJa13c] up to the question, on the computational complexity of variants of equivalence problems on biautomata [HoJa14] were recently considered. Here it is worth mentioning that he most elegant minimization algorithm, that is, that of Brzozowski [Br62], which minimizes an ordinary finite automaton \(A\), regardless whether it is deterministic or nondeterministic, by applying the reversal and power-set construction atwice in sequence, also works for biautomata. On the other hand biautomata can also be significantly different to ordinary finite automata as, e.g., shown in [HoJa14], where it was proven that computing a hyper-minimal biautomata is computational intractable, namely the problem is NP-complete. Here an automaton is hyper-minimal if it admits no smaller almost equivalent automaton of same type, where two automata are almost equivalent if the symmetric difference of their languages is finite. This task is polynomial time solvable in case of ordinary deterministic finite automata [HoMa10]. Some of the presented results were obtained together with co-author Sebastian Jakobi.
[Br62]
J. A. Brzozowski. Canonical regular expressions and minimal state graphs for definite events. In Mathematical Theory of Automata, volume 12 of MRI Symposia Series], pages 529--561. Polytechnic Press, NY, 1962.
[Br64]
J. A. Brzozowski. Derivatives of regular expressions. J. ACM, 11:481--494, 1964.
[CDJM13a]
J.-M. Champarnaud, J.-P. Dubernard, H. Jeanne, and L. Mignot. Two-sided derivatives for regular expressions and for hairpin expressions. In A.-H.dediu, C. Martín-Vide, and B. Truthe, editors, Proceedings of the $7$th International Conference on Language and Automata Theory and Applications, number 7810 in LNCS, pages 202--213, Bilbao, Spain 2013. Springer.
[HoJa13c]
M. Holzer and S. Jakobi. Minimization and characterizations for biautomata. In S. Bensch, F. Drewes, R. Freund, and F. Otto, editors, Proceedings of the 5th International Workshop on Non-Classical Models of Automata and Applications, number 294 in books$@$ocg.at, pages 179--193, Umea, Sweden, 2013. Österreichische Computer Gesellschaft.
[HoJa13a]
M. Holzer and S. Jakobi. Nondeterministic biautomata and their descriptional complexity. In H. Jürgensen and R. Reis, editors, Proceedings of the 15th International Workshop on Descriptional Complexity of Formal Systems, number 8031 in LNCS, pages 112--123, London, Ontario, Canada, 2013. Springer.
[HoJa14]
M. Holzer and S. Jakobi.
On the complexity of some computational problems on biautomata, 2014. Manuscript in preparation.
[HoMa10]
M. Holzer and A. Maletti. An \(n\log n\) algorithm for hyper-minimizing a (minimized) deterministic automaton. Theoret. Comput. Sci., 411(38--39):3404--3413, 2010.
[JiKl12]
G. Jiráková and O. Klíma. Descriptional complexity of biautomata. In M. Kutrib, N. Moreira, and R. Reis, editors, Proceedings of the 14th International Workshop Descriptional Complexity of Formal Systems, number 7386 in LNCS, pages 196--208, Braga, Portugal, 2012. Springer.
[KlPo12]
O. Klíma and L. Polák. On biautomata. RAIRO--Informatique théorique et Applications / Theoretical Informatics and Applications, 46(4):573--592, 2012.
[Lo07]
R. Loukanova.
Linear context free languages. In C. B. Jones, Z. Liu, and J. Woodcock, editors, Proceedings of the 4th International Colloquium Theoretical Aspects of Computing, number 4711 in LNCS, pages 351--365, Macau, China, 2007. Springer.
[Ro67]
A. L. Rosenberg. A machine realization of the linear context-free languages. Inform. Control, 10:175--188, 1967.
Martin Kutrib (Institut für Informatik Universität Gießen)
Complexity of Cellular Automata Computations
The advantages of homogeneous arrays of interacting processing elements are simplicity and uniformity. It turned out that a large array of not very powerful elements operating in parallel can be programmed to be very powerful. One type of system is of particular interest: cellular automata whose homogeneously interconnected finite automata (the cells) work synchronously at discrete time steps obeying one common transition function. Cellular automata have extensively been investigated from different points of view. Here we consider them as massively parallel computing model and address some of the main aspects of their complexity. The survey covers the hierarchy of cellular automata classes, their relations to classical computational complexity, reversibility issues, and decidability questions. The later have close connections to the descriptional complexity of cellular automata. Some open problems are addressed as well.
The advantages of homogeneous arrays of interacting processing elements are simplicity and uniformity. It turned out that a large array of not very powerful elements operating in parallel can be programmed to be very powerful. One type of system is of particular interest: cellular automata whose homogeneously interconnected finite automata (the cells) work synchronously at discrete time steps obeying one common transition function. Cellular automata have extensively been investigated from different points of view. Here we consider them as massively parallel computing model and address some of the main aspects of their complexity. The survey covers the hierarchy of cellular automata classes, their relations to classical computational complexity, reversibility issues, and decidability questions. The later have close connections to the descriptional complexity of cellular automata. Some open problems are addressed as well.
Eva Maia (Centro de Matemática da Universidade do Porto)
Pursuing the bisimilarity of Position Automata
Minimization of nondeterministic finite automata (NFA) is a hard problem (PSPACE-complete). Bisimulations are then an attractive alternative for reducingg the size of NFAs, as even bisimilarity (the largest bisimulation) is almost linear using the Paige and Tarjan algorithm.
NFAs obtained from REs can have the number of states linear with respect to (w.r.t) the size of the REs. Conversion methods from REs to equivalent NFAs can produce NFAs without or with transitions labelled with the empty word (\(\epsilon\)-NFA). The standard conversion without \(\epsilon\)-transitions is the position automaton. Other conversions such as partial derivative (PD) automata [1,2], follow automata [3], or the construction in [4], were proved to be quotients of the position automata (by some bisimulations).
Some experimental results in [5] suggested that for REs in (normalized) star normal form (snf) the position bisimilarity almost coincide with the PD automata.
Our goal is to have a better characterization of the PD automata and of the bisimularity of the position automata. In this talk, we will consider this problem for some families of regular expressions.
[1] Antimirov, V. M.: Partial derivatives of regular expressions and finite automaton constructions. Theoret. Comput. Sci., 155(2):291–319, 1996.
[2] Mirkin, B. G.: An algorithm for constructing a base in a language of regular expres- sions. Engineering Cybernetics, 5:51—57, 1966.
[3] Ilie L., Yu S.: Follow automata. Inf. Comput., 186(1):140–162, 2003.
[4] Garcia, P., López, D., Ruiz, J., Alvarez, G.I.: From regular expressions to smaller NFAs. Theor. Comput. Sci. 412(41), 5802–5807 (2011)
[5] Gouveia H., Moreira N., Reis R.: Small nfas from regular expressions: Some experimental results. In Fernando Ferreira, Hélia Guerra, Elvira Mayordomo, and João Rasga, editors, Proceedings of 6th Conference on Computability in Europe (CIE 2010), pages 194-203, Ponta Delgada, Azores, Portugal, June 2010. CMATI.
Minimization of nondeterministic finite automata (NFA) is a hard problem (PSPACE-complete). Bisimulations are then an attractive alternative for reducingg the size of NFAs, as even bisimilarity (the largest bisimulation) is almost linear using the Paige and Tarjan algorithm.
NFAs obtained from REs can have the number of states linear with respect to (w.r.t) the size of the REs. Conversion methods from REs to equivalent NFAs can produce NFAs without or with transitions labelled with the empty word (\(\epsilon\)-NFA). The standard conversion without \(\epsilon\)-transitions is the position automaton. Other conversions such as partial derivative (PD) automata [1,2], follow automata [3], or the construction in [4], were proved to be quotients of the position automata (by some bisimulations).
Some experimental results in [5] suggested that for REs in (normalized) star normal form (snf) the position bisimilarity almost coincide with the PD automata.
Our goal is to have a better characterization of the PD automata and of the bisimularity of the position automata. In this talk, we will consider this problem for some families of regular expressions.
[1] Antimirov, V. M.: Partial derivatives of regular expressions and finite automaton constructions. Theoret. Comput. Sci., 155(2):291–319, 1996.
[2] Mirkin, B. G.: An algorithm for constructing a base in a language of regular expres- sions. Engineering Cybernetics, 5:51—57, 1966.
[3] Ilie L., Yu S.: Follow automata. Inf. Comput., 186(1):140–162, 2003.
[4] Garcia, P., López, D., Ruiz, J., Alvarez, G.I.: From regular expressions to smaller NFAs. Theor. Comput. Sci. 412(41), 5802–5807 (2011)
[5] Gouveia H., Moreira N., Reis R.: Small nfas from regular expressions: Some experimental results. In Fernando Ferreira, Hélia Guerra, Elvira Mayordomo, and João Rasga, editors, Proceedings of 6th Conference on Computability in Europe (CIE 2010), pages 194-203, Ponta Delgada, Azores, Portugal, June 2010. CMATI.
Nelma Moreira (Centro de Matemática da Universidade do Porto)
Automata for KAT expressions
Kleene algebra with tests (KAT) is an equational system that extends Kleene algebra with Boolean tests and that is specially suited to capture and verify properties of simple imperative programs. The standard language-theoretic models for KAT are regular sets of guarded strings, which are words \(w\) where symbols \(p\) from an alphabet \(\Sigma\), alternate with atoms \(\alpha\in At\) which are boolean assignments to (boolean) variables. Automata for KAT expressions as introduced by Kozen [1,2], work over alphabets \(At\times \Sigma\), thus leading to an explicit exponential blow-up (on the size of a KAT expression). Silva [3] introduced an automata model that extends Glushkov's construction for regular expressions. In this automata, transitions are labeled with KAT expressions of the form \(bp\), where \(b\) is a boolean expression and \(p\) an alphabetic symbol. We extended 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 [4]. Classical methods of determinization and equivalence of DFAs can be generalized to this automata and applied to decide KAT expressions equivalence avoiding the explicit use of all possible assignments to the boolean variables.
[1] Kozen, D.: Automata on guarded strings and applications. Matématica Contemporânea 24, 117–139 (2003)
[2] Kozen,D.:On the coalgebraic theory of Kleene algebra with tests.Tech.Rep.http: //hdl.handle.net/1813/10173, Cornell University (05 2008)
[3] Silva, A.: Position automata for Kleene algebra with tests. Sci. Ann. Comp. Sci. 22(2), 367–394 (2012)
[4] Broda, S., Machiavelo, A., Moreira, N., Reis, R.: On the average size of Glushkov and equation automata for KAT expressions. In: 19th International Symposium on Fundamentals of Computation Theory. pp. 72–83. No. 8070 in LNCS, Springer (2013)
Kleene algebra with tests (KAT) is an equational system that extends Kleene algebra with Boolean tests and that is specially suited to capture and verify properties of simple imperative programs. The standard language-theoretic models for KAT are regular sets of guarded strings, which are words \(w\) where symbols \(p\) from an alphabet \(\Sigma\), alternate with atoms \(\alpha\in At\) which are boolean assignments to (boolean) variables. Automata for KAT expressions as introduced by Kozen [1,2], work over alphabets \(At\times \Sigma\), thus leading to an explicit exponential blow-up (on the size of a KAT expression). Silva [3] introduced an automata model that extends Glushkov's construction for regular expressions. In this automata, transitions are labeled with KAT expressions of the form \(bp\), where \(b\) is a boolean expression and \(p\) an alphabetic symbol. We extended 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 [4]. Classical methods of determinization and equivalence of DFAs can be generalized to this automata and applied to decide KAT expressions equivalence avoiding the explicit use of all possible assignments to the boolean variables.
[1] Kozen, D.: Automata on guarded strings and applications. Matématica Contemporânea 24, 117–139 (2003)
[2] Kozen,D.:On the coalgebraic theory of Kleene algebra with tests.Tech.Rep.http: //hdl.handle.net/1813/10173, Cornell University (05 2008)
[3] Silva, A.: Position automata for Kleene algebra with tests. Sci. Ann. Comp. Sci. 22(2), 367–394 (2012)
[4] Broda, S., Machiavelo, A., Moreira, N., Reis, R.: On the average size of Glushkov and equation automata for KAT expressions. In: 19th International Symposium on Fundamentals of Computation Theory. pp. 72–83. No. 8070 in LNCS, Springer (2013)
David Pereira (CISTER, ISEP/IPP)
Formalization and Certified Equivalence of Regular Expressions and KAT Expressions in Coq
Proof assistants are powerful tools specially designed to formalise and verify mathematical developments and properties of computer programs. Results like the proofs of the Four Color and of the Feit-Thomson theorems, the certified compiler CompCert, and the certified micro-kernel SeL4 show that proof assistants can indeed be used in practice to solve/check important mathematical problems, or in the production of certified software. In this talk, we will focus on the Coq proof assistant and on how we can use it to formalize and verify properties of regular expressions, KAT expression, and their partial derivatives. We will give particular focus to the several steps required for implementing a certified decision procedure for regular expression equivalence, in a way that is computationally efficient, and from which we can extract correct functional programming code. Finally, we will show how we can use all the formalisation effort to prove the equivalence and the partial correctness of simple imperative computer programs.
Proof assistants are powerful tools specially designed to formalise and verify mathematical developments and properties of computer programs. Results like the proofs of the Four Color and of the Feit-Thomson theorems, the certified compiler CompCert, and the certified micro-kernel SeL4 show that proof assistants can indeed be used in practice to solve/check important mathematical problems, or in the production of certified software. In this talk, we will focus on the Coq proof assistant and on how we can use it to formalize and verify properties of regular expressions, KAT expression, and their partial derivatives. We will give particular focus to the several steps required for implementing a certified decision procedure for regular expression equivalence, in a way that is computationally efficient, and from which we can extract correct functional programming code. Finally, we will show how we can use all the formalisation effort to prove the equivalence and the partial correctness of simple imperative computer programs.
Giovanni Pighizzini ( Università degli Studi di Milano)
Parikh Equivalence and Descriptional Complexity
It is well-known that the conversion of nondeterministic finite automata into equivalent deterministic finite automata requires an exponential number of states. In all examples witnessing such a state gap, input alphabets with at least two letters and proof arguments strongly relying on the structure of words are used.
What happens if we do not care of the order of symbols in the words, i.e., if we are interested only in obtaining deterministic automata accepting sets of words which are equal, after permuting
the symbols, to the words accepted by the given nondeterministic automata?
This question is related to the well-known notions of Parikh image and Parikh equivalence. We answer the question by proving that for each nondeterministic automaton with n states,
there exists a Parikh equivalent deterministic automaton with \(e^{O(\sqrt{n \cdot \ln n})}\) states. In contrast and quite surprisingly, if all the words accepted by the given automaton contain at least two different letters, then a Parikh equivalent one-way deterministic automaton with a polynomial number of states can be found.
We also consider context-free grammars. We prove that for each grammar in Chomsky normal form with h variables there exists a Parikh equivalent deterministic automata with \(2^{O(h^2)}\) states. All the bounds are tight.
Reference:
G.J. Lavado, G. Pighizzini, and S. Seki.
Converting nondeterministic automata and context-free grammars into Parikh equivalent one-way and two-way deterministic automata. Information and Computation, 228: 1-15 (2013)
It is well-known that the conversion of nondeterministic finite automata into equivalent deterministic finite automata requires an exponential number of states. In all examples witnessing such a state gap, input alphabets with at least two letters and proof arguments strongly relying on the structure of words are used.
What happens if we do not care of the order of symbols in the words, i.e., if we are interested only in obtaining deterministic automata accepting sets of words which are equal, after permuting
the symbols, to the words accepted by the given nondeterministic automata?
This question is related to the well-known notions of Parikh image and Parikh equivalence. We answer the question by proving that for each nondeterministic automaton with n states,
there exists a Parikh equivalent deterministic automaton with \(e^{O(\sqrt{n \cdot \ln n})}\) states. In contrast and quite surprisingly, if all the words accepted by the given automaton contain at least two different letters, then a Parikh equivalent one-way deterministic automaton with a polynomial number of states can be found.
We also consider context-free grammars. We prove that for each grammar in Chomsky normal form with h variables there exists a Parikh equivalent deterministic automata with \(2^{O(h^2)}\) states. All the bounds are tight.
Reference:
G.J. Lavado, G. Pighizzini, and S. Seki.
Converting nondeterministic automata and context-free grammars into Parikh equivalent one-way and two-way deterministic automata. Information and Computation, 228: 1-15 (2013)
Emanuele Rodaro (Centro de Matemática da Universidade do Porto)
A descriptional complexity approach to Cěrny conjecture
We introduce the notion of reset left regular decomposition of an ideal regular language, and we prove that the category formed by these decompositions with the adequate set of morphisms is equivalent to the category of strongly connected synchronizing automata. We show that each ideal regular language has at least one reset left regular decomposition. Using these facts we introduce the notion of reset decomposition complexity of an ideal and reformulate Cěrny's conjecture in terms of lower bounds of this complexity index.
We introduce the notion of reset left regular decomposition of an ideal regular language, and we prove that the category formed by these decompositions with the adequate set of morphisms is equivalent to the category of strongly connected synchronizing automata. We show that each ideal regular language has at least one reset left regular decomposition. Using these facts we introduce the notion of reset decomposition complexity of an ideal and reformulate Cěrny's conjecture in terms of lower bounds of this complexity index.