
Researcher, LaBRI CS Lab, Bordeaux University. Professor of Computer Science, Bordeaux University. 
đ§ 
mz@labri.fr 
Research
Main interests

Links

Publications
 All publications
2016
 J. Almeida, J. C. Costa, M. Zeitoun, Reducibility of Pointlike Problems. Semigroup Forum, 2016. doi pdf abstract We show that the pointlike and the idempotent pointlike problems are reducible with respect to natural signatures in the following cases: the pseudovariety of all finite semigroups in which the order of every subgroup is a product of elements of a fixed set Ï of primes; the pseudovariety of all finite semigroups in which every regular Jclass is the product of a rectangular band by a group from a fixed pseudovariety of groups that is reducible for the pointlike problem, respectively graph reducible. Allowing only trivial groups, we obtain Ïreducibility of the pointlike and idempotent pointlike problems, respectively for the pseudovarieties of all finite aperiodic semigroups (A) and of all finite semigroups in which all regular elements are idempotents (DA). bibtex
@article{reducibility:acz:2015, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {Reducibility of Pointlike Problems}, journal = {Semigroup Forum}, year = 2016, doi = {10.1007/s0023301597692}, url = {http://arxiv.org/pdf/1507.03076v1.pdf}, abstract = "We show that the pointlike and the idempotent pointlike problems are reducible with respect to natural signatures in the following cases: the pseudovariety of all finite semigroups in which the order of every subgroup is a product of elements of a fixed set Ï of primes; the pseudovariety of all finite semigroups in which every regular Jclass is the product of a rectangular band by a group from a fixed pseudovariety of groups that is reducible for the pointlike problem, respectively graph reducible. Allowing only trivial groups, we obtain Ïreducibility of the pointlike and idempotent pointlike problems, respectively for the pseudovarieties of all finite aperiodic semigroups (A) and of all finite semigroups in which all regular elements are idempotents (DA).", note = {To appear} }
 T. Pierron, T. Place, M. Zeitoun, Quantifier Alternation for Infinite Words. In 19th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS'16, Springer. 2016. doi pdf abstract We investigate the expressive power of the quantifier alternation hierarchy of firstorder logic over words. This hierarchy includes the classes ÎŁi (sentences having at most i blocks of quantifiers starting with an â) and BÎŁi (Boolean combinations of ÎŁi sentences). So far, this expressive power has been effectively characterized for the lower levels only. Recently, a breakthrough was made over finite words, and decidable characterizations were obtained for BÎŁ2 and ÎŁ3, by relying on a decision problem called separation, and solving it for ÎŁ2. The contribution of this paper is a generalization of these results to the setting of infinite words: we solve separation for ÎŁ2 and ÎŁ3, and obtain decidable characterizations of BÎŁ2 and ÎŁ3 as consequences. bibtex
@inproceedings{ppzinf16, author = {T. Pierron and T. Place and M. Zeitoun}, title = {Quantifier Alternation for Infinite Words}, booktitle = {19th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS'16}, year = 2016, editor = {B. Jacobs and C. LĂ¶ding}, series = {Lect. Notes Comp. Sci.}, volume = 9634, publisher = {Springer}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/PPZFOSSACS16.pdf}, doi = {10.1007/9783662496305_14}, abstract = {We investigate the expressive power of the quantifier alternation hierarchy of firstorder logic over words. This hierarchy includes the classes ÎŁi (sentences having at most i blocks of quantifiers starting with an â) and BÎŁi (Boolean combinations of ÎŁi sentences). So far, this expressive power has been effectively characterized for the lower levels only. Recently, a breakthrough was made over finite words, and decidable characterizations were obtained for BÎŁ2 and ÎŁ3, by relying on a decision problem called separation, and solving it for ÎŁ2. The contribution of this paper is a generalization of these results to the setting of infinite words: we solve separation for ÎŁ2 and ÎŁ3, and obtain decidable characterizations of BÎŁ2 and ÎŁ3 as consequences.} }
 T. Place, M. Zeitoun, Separating Regular Languages with FirstOrder Logic. Logical Methods in Computer Science 12 (1), pp. 1â30, 2016. doi pdf abstract Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem, called separation: given two regular languages of finite words, decide whether there exists a firstorder definable separator. A more general problem was solved in an algebraic framework by Henckell in 1988, although the connection with separation was pointed out only in 1996, by Almeida. The result was then generalized by Henckell, Steinberg and Rhodes in 2010. In this paper, we present a new, selfcontained and elementary proof of it, which actually covers the original result of Henckell. We prove that in order to answer this question, sufficient information can be extracted from semigroups recognizing the input languages, using a fixpoint computation, similar to that originally proposed by Henckell. Given as input a morphism recognizing both languages to be separated, this yields an Exptime algorithm for checking firstorder separability. Moreover, the correctness proof of this algorithm yields a stronger result, namely a description of a possible separator. More precisely, one can compute a bound on the quantifier rank of potential separators, as well as a firstorder formula that describes a separator, if there exists one. Finally, we prove that this technique can be generalized to answer the same question for regular languages of infinite words. bibtex
@Article{PZ:FOSep16, author = {T. Place and M. Zeitoun}, title = {Separating Regular Languages with FirstOrder Logic}, journal = {Logical Methods in Computer Science}, year = 2016, url = {http://arxiv.org/pdf/1402.3277v3}, volume = 12, number = 1, pages = {130}, doi = {10.2168/LMCS12(1:5)2016}, abstract = {Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem, called separation: given two regular languages of finite words, decide whether there exists a firstorder definable separator. A more general problem was solved in an algebraic framework by Henckell in 1988, although the connection with separation was pointed out only in 1996, by Almeida. The result was then generalized by Henckell, Steinberg and Rhodes in 2010. In this paper, we present a new, selfcontained and elementary proof of it, which actually covers the original result of Henckell. We prove that in order to answer this question, sufficient information can be extracted from semigroups recognizing the input languages, using a fixpoint computation, similar to that originally proposed by Henckell. Given as input a morphism recognizing both languages to be separated, this yields an Exptime algorithm for checking firstorder separability. Moreover, the correctness proof of this algorithm yields a stronger result, namely a description of a possible separator. More precisely, one can compute a bound on the quantifier rank of potential separators, as well as a firstorder formula that describes a separator, if there exists one. Finally, we prove that this technique can be generalized to answer the same question for regular languages of infinite words.} }
 J. Almeida, J. C. Costa, M. Zeitoun, Factoriality and the PinReutenauer Procedure. Discrete Mathematics & Theoretical Computer Science 18 (3), pp. 123, 2016. pdf abstract We consider implicit signatures over finite semigroups determined by sets of pseudonatural numbers. We prove that, under relatively simple hypotheses on a pseudovariety V of semigroups, the finitely generated free algebra for the largest such signature is closed under taking factors within the free proV semigroup on the same set of generators. Furthermore, we show that the natural analogue of the PinReutenauer descriptive procedure for the closure of a rational language in the free group with respect to the profinite topology holds for the pseudovariety of all finite semigroups. As an application, we establish that a pseudovariety enjoys this property if and only if it is full. bibtex
@article{factoriality:acz:2016, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {{Factoriality and the PinReutenauer Procedure}}, journal = {Discrete Mathematics & Theoretical Computer Science}, year = 2016, volume = 18, number = 3, pages = {123}, url = {http://dmtcs.episciences.org/1412/pdf}, abstract = "We consider implicit signatures over finite semigroups determined by sets of pseudonatural numbers. We prove that, under relatively simple hypotheses on a pseudovariety V of semigroups, the finitely generated free algebra for the largest such signature is closed under taking factors within the free proV semigroup on the same set of generators. Furthermore, we show that the natural analogue of the PinReutenauer descriptive procedure for the closure of a rational language in the free group with respect to the profinite topology holds for the pseudovariety of all finite semigroups. As an application, we establish that a pseudovariety enjoys this property if and only if it is full.", note = {To appear} }
 T. Place, M. Zeitoun, The Covering Problem: a Unified Approach for Investigating the Expressive Power of Logics. In 41st International Symposium on Mathematical Foundations of Computer Science, MFCS'16, pp. 78:1â78:14, Schloss Dagstuhl  LeibnizZentrum fĂŒr Informatik. 2016. doi pdf abstract An important endeavor in computer science is to precisely understand the expressive power of logical formalisms over discrete structures, such as words. Naturally, âunderstandingâ is not a mathematical notion. Therefore, this investigation requires a concrete objective to capture such a notion. In the literature, the standard choice for this objective is the emph{membership problem}, whose aim is to find a procedure deciding whether an input regular language can be defined in the logic under study. This approach was cemented as the ârightâ one by the seminal work of SchĂŒtzenberger, McNaughton and Papert on firstorder logic and has been in use since then. However, membership questions are hard: for several important fragments, researchers have failed in this endeavor despite decades of investigation. In view of recent results on one of the most famous open questions, namely the quantifier alternation hierarchy of firstorder logic, an explanation may be that membership is too restrictive as a setting. These new results were indeed obtained by considering more general problems than membership, taking advantage of the increased flexibility of the enriched mathematical setting. This opens a promising avenue of research and efforts have been devoted at identifying and solving such problems for natural fragments. However, until now, these problems have been emph{ad hoc}, most fragments relying on a specific one. A unique new problem replacing membership as the right one is still missing. The main contribution of this paper is a suitable candidate to play this role: the Covering Problem. We motivate this problem with three arguments. First, it admits an elementary set theoretic formulation, similar to membership. Second, we are able to reexplain or generalize all known results with this problem. Third, we develop a mathematical framework as well as a methodology tailored to the investigation of this problem. bibtex
@inproceedings{pzcovers:mfcs16, author = {T. Place and M. Zeitoun}, title = {The Covering Problem: a Unified Approach for Investigating the Expressive Power of Logics}, booktitle = {41st International Symposium on Mathematical Foundations of Computer Science, MFCS'16}, year = 2016, editor = {P. Faliszewski and A. Muscholl and R. Niedermeier}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, volume = 58, publisher = {Schloss Dagstuhl  LeibnizZentrum fĂŒr Informatik}, pages = {78:178:14}, doi = {10.4230/LIPIcs.MFCS.2016.78}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/PZMFCS16.pdf}, abstract = {An important endeavor in computer science is to precisely understand the expressive power of logical formalisms over discrete structures, such as words. Naturally, "understanding" is not a mathematical notion. Therefore, this investigation requires a concrete objective to capture such a notion. In the literature, the standard choice for this objective is the emph{membership problem}, whose aim is to find a procedure deciding whether an input regular language can be defined in the logic under study. This approach was cemented as the "right" one by the seminal work of SchĂŒtzenberger, McNaughton and Papert on firstorder logic and has been in use since then. However, membership questions are hard: for several important fragments, researchers have failed in this endeavor despite decades of investigation. In view of recent results on one of the most famous open questions, namely the quantifier alternation hierarchy of firstorder logic, an explanation may be that membership is too restrictive as a setting. These new results were indeed obtained by considering more general problems than membership, taking advantage of the increased flexibility of the enriched mathematical setting. This opens a promising avenue of research and efforts have been devoted at identifying and solving such problems for natural fragments. However, until now, these problems have been emph{ad hoc}, most fragments relying on a specific one. A unique new problem replacing membership as the right one is still missing. The main contribution of this paper is a suitable candidate to play this role: the Covering Problem. We motivate this problem with three arguments. First, it admits an elementary set theoretic formulation, similar to membership. Second, we are able to reexplain or generalize all known results with this problem. Third, we develop a mathematical framework as well as a methodology tailored to the investigation of this problem.} }
2015
 T. Place, M. Zeitoun, The Tale of the Quantifier Alternation Hierarchy of FirstOrder Logic over Words. SIGLOG news 2 (3), pp. 417, ACM. July 2015. pdf abstract In this survey, we present ideas developed until recently in order to understand the expressive power of logical fragments in the quantifier alternation hierarchy of firstorder logic interpreted on finite words. bibtex
@article{PZ:Siglog15, author = {T. Place and M. Zeitoun}, title = {The Tale of the Quantifier Alternation Hierarchy of FirstOrder Logic over Words}, journal = {SIGLOG news}, year = 2015, volume = 2, number = 3, pages = {417}, month = {July}, publisher = {{ACM}}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/QaltSiglog15.pdf}, abstract = {In this survey, we present ideas developed until recently in order to understand the expressive power of logical fragments in the quantifier alternation hierarchy of firstorder logic interpreted on finite words.} }
 J. Almeida, J. C. Costa, M. Zeitoun, McCammondâs normal forms for free aperiodic semigroups revisited. LMS Journal of Computation and Mathematics 18 (1), pp. 130â147, Cambridge University Press. 2015. doi pdf abstract This paper revisits the solution of the word problem for Ïterms interpreted over finite aperiodic semigroups, obtained by J. McCammond. The original proof of correctness of McCammondâs algorithm, based on normal forms for such terms, uses McCammondâs solution of the word problem for certain Burnside semigroups. In this paper, we establish a new, simpler, correctness proof of McCammondâs algorithm, based on properties of certain regular languages associated with the normal forms. This method leads to new applications. bibtex
@article{ACZ14:McCammonNF, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {{McCammondâs normal forms for free aperiodic semigroups revisited}}, journal = {LMS Journal of Computation and Mathematics}, year = 2015, volume = 18, number = 1, pages = {130147}, doi = {10.1112/S1461157014000448}, publisher = {Cambridge University Press}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/ACZMcCammondNF.pdf}, abstract = {This paper revisits the solution of the word problem for Ïterms interpreted over finite aperiodic semigroups, obtained by J. McCammond. The original proof of correctness of McCammondâs algorithm, based on normal forms for such terms, uses McCammondâs solution of the word problem for certain Burnside semigroups. In this paper, we establish a new, simpler, correctness proof of McCammondâs algorithm, based on properties of certain regular languages associated with the normal forms. This method leads to new applications.}}
 W. Czerwinski, W. Martens, L. van Rooijen, M. Zeitoun, A Note on Decidable Separability by Piecewise Testable Languages. In 20th International Symposium on Fundamentals of Computation Theory, FCT'15, pp. 173185, Springer. 2015. doi pdf abstract The separability problem for languages from a class C by languages of a class S asks, for two given word languages I and E from C, whether there exists a language S from S which includes I and excludes E, that is, I â S and S â© E = â . It is known that separability for contextfree languages by any class containing all definite languages (such as regular languages) is undecidable. We show that separability of contextfree languages by piecewise testable languages is decidable. This contrasts the fact that testing if a contextfree language is piecewise testable is undecidable. We generalize this decidability result by showing that, for every full trio (a class of languages that is closed under rather weak operations) which has decidable diagonal problem, separability with respect to piecewise testable languages is decidable. Examples of such classes are the class of languages defined by labeled vector addition systems and the class of languages accepted by higher order pushdown automata of order two. The proof goes through a result which is of independent interest and shows that, for any kind of languages I and E, separability can be decided by testing the existence of common patterns in I and E. bibtex
@inproceedings{CMvRZ:15, author = {W. Czerwinski and W. Martens and L. van Rooijen and M. Zeitoun}, title = {A Note on Decidable Separability by Piecewise Testable Languages}, booktitle = {20th International Symposium on Fundamentals of Computation Theory, FCT'15}, year = 2015, editor = {A. Kosowski and I. Walukiewicz}, volume = 9210, series = {Lect. Notes Comp. Sci.}, pages = {173185}, publisher = {Springer}, doi = {10.1007/9783319221779}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/PTSepFCT15.pdf}, abstract = {The separability problem for languages from a class C by languages of a class S asks, for two given word languages I and E from C, whether there exists a language S from S which includes I and excludes E, that is, I â S and S â© E = â . It is known that separability for contextfree languages by any class containing all definite languages (such as regular languages) is undecidable. We show that separability of contextfree languages by piecewise testable languages is decidable. This contrasts the fact that testing if a contextfree language is piecewise testable is undecidable. We generalize this decidability result by showing that, for every full trio (a class of languages that is closed under rather weak operations) which has decidable diagonal problem, separability with respect to piecewise testable languages is decidable. Examples of such classes are the class of languages defined by labeled vector addition systems and the class of languages accepted by higher order pushdown automata of order two. The proof goes through a result which is of independent interest and shows that, for any kind of languages I and E, separability can be decided by testing the existence of common patterns in I and E.} }
 T. Place, M. Zeitoun, Separation and the Successor Relation. In STACS'15, pp. 662â675, Springer. 2015. doi pdf abstract We investigate two problems for a class C of regular word languages. The Cmembership problem asks for an algorithm to decide whether an input language belongs to C. The Cseparation problem asks for an algorithm that, given as input two regular languages, decides whether there exists a third language in C containing the first language, while being disjoint from the second. These problems are considered as means to obtain a deep understanding of the class C. It is usual for such classes to be defined by logical formalisms. Logics are often built on top of each other, by adding new predicates. A natural construction is to enrich a logic with the successor relation. In this paper, we obtain simple selfcontained proofs of two transfer results: we show that for suitable logically defined classes, the membership, resp. the separation problem for a class enriched with the successor relation reduces to the same problem for the original class. Our reductions work both for languages of finite words and infinite words. The proofs are mostly selfcontained, and only require a basic background on regular languages. This paper therefore gives new, simple proofs of results that were considered as difficult, such as the decidability of the membership problem for the levels 1, 3/2, 2 and 5/2 of the dotdepth hierarchy. bibtex
@inproceedings{PZ:stacs15, author = {T. Place and M. Zeitoun}, title = {Separation and the Successor Relation}, booktitle = {{STACS'15}}, year = {2015}, series = {Lect. Notes Comp. Sci.}, volume = {30}, pages = {662675}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, editor = {Ernst W. Mayr and Nicolas Ollinger}, publisher = {Springer}, URL = {http://drops.dagstuhl.de/opus/volltexte/2015/4949}, URN = {urn:nbn:de:0030drops49499}, doi = {10.4230/LIPIcs.STACS.2015.662}, abstract = {We investigate two problems for a class C of regular word languages. The Cmembership problem asks for an algorithm to decide whether an input language belongs to C. The Cseparation problem asks for an algorithm that, given as input two regular languages, decides whether there exists a third language in C containing the first language, while being disjoint from the second. These problems are considered as means to obtain a deep understanding of the class C. It is usual for such classes to be defined by logical formalisms. Logics are often built on top of each other, by adding new predicates. A natural construction is to enrich a logic with the successor relation. In this paper, we obtain simple selfcontained proofs of two transfer results: we show that for suitable logically defined classes, the membership, resp. the separation problem for a class enriched with the successor relation reduces to the same problem for the original class. Our reductions work both for languages of finite words and infinite words. The proofs are mostly selfcontained, and only require a basic background on regular languages. This paper therefore gives new, simple proofs of results that were considered as difficult, such as the decidability of the membership problem for the levels 1, 3/2, 2 and 5/2 of the dotdepth hierarchy.} }
2014
 B. Bollig, A. Cyriac, P. Gastin, M. Zeitoun, Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking. Journal of Applied Logic 12 (4), pp. 395â416, 2014. doi pdf abstract We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic secondorder logic and that, in addition, allows PDLlike path expressions. This captures, in a unifying framework, a wide range of logics defined for ranked and unranked trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satifiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities. bibtex
@article{BCGZ:TempLogConcRecurs:14, author = {Bollig, B. and Cyriac, A. and Gastin, P. and Zeitoun, M.}, title = {Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking}, journal = {Journal of Applied Logic}, volume = 12, number = 4, pages = 395â416, year = {2014}, doi = {10.1016/j.jal.2014.05.001}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/BCGZjal14.pdf}, abstract = {We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic secondorder logic and that, in addition, allows PDLlike path expressions. This captures, in a unifying framework, a wide range of logics defined for ranked and unranked trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satifiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities.} }
 J. Almeida, J. C. Costa, M. Zeitoun, Closures of Regular Languages for Profinite Topologies. Semigroup Forum 89 (1), pp. 20â40, 2014. doi pdf abstract The PinReutenauer algorithm gives a method, that can be viewed as a descriptive procedure, to compute the closure in the free group of a regular language with respect to the Hall topology. A similar descriptive procedure is shown to hold for the pseudovariety A of aperiodic semigroups, where the closure is taken in the free aperiodic Ïsemigroup. It is inherited by a subpseudovariety of a given pseudovariety if both of them enjoy the property of being full. The pseudovariety A, as well as some of its subpseudovarieties are shown to be full. The interest in such descriptions stems from the fact that, for each of the main pseudovarieties V in our examples, the closures of two regular languages are disjoint if and only if the languages can be separated by a language whose syntactic semigroup lies in V. In the cases of A and of the pseudovariety DA of semigroups in which all regular elements are idempotents, this is a new result. bibtex
@article{ACZ:Closures:14, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {Closures of Regular Languages for Profinite Topologies}, journal = {Semigroup Forum}, year = {2014}, volume = 89, number = 1, pages = {2040}, doi = {10.1007/s0023301495743}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaCostaZeitounxi2013.pdf}, abstract = {The PinReutenauer algorithm gives a method, that can be viewed as a descriptive procedure, to compute the closure in the free group of a regular language with respect to the Hall topology. A similar descriptive procedure is shown to hold for the pseudovariety A of aperiodic semigroups, where the closure is taken in the free aperiodic Ïsemigroup. It is inherited by a subpseudovariety of a given pseudovariety if both of them enjoy the property of being full. The pseudovariety A, as well as some of its subpseudovarieties are shown to be full. The interest in such descriptions stems from the fact that, for each of the main pseudovarieties V in our examples, the closures of two regular languages are disjoint if and only if the languages can be separated by a language whose syntactic semigroup lies in V. In the cases of A and of the pseudovariety DA of semigroups in which all regular elements are idempotents, this is a new result.} }
 J. Almeida, J. C. Costa, M. Zeitoun, Iterated Periodicity over Finite Aperiodic Semigroups. European J. Combinatorics 37, pp. 115149, 2014. doi pdf abstract This paper provides a characterization of pseudowords over the pseudovariety of all finite aperiodic semigroups that can be described from the free generators using only the operations of multiplication and Ïpower. A necessary and sufficient condition for this property to hold turns out to be given by the conjunction of two rather simple finiteness conditions: the nonexistence of infinite antichains of factors and the rationality of the language of McCammond normal forms of Ïterms that define factors of the given pseudoword. The relationship between pseudowords with this property and arbitrary pseudowords is also investigated. bibtex
@article{ACZ:Iterated:14, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {Iterated Periodicity over Finite Aperiodic Semigroups}, journal = {European J. Combinatorics}, volume = {37}, pages = {115149}, year = {2014}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaCostaZeitounAkterms.pdf}, doi = {10.1016/j.ejc.2013.07.011}, abstract = {This paper provides a characterization of pseudowords over the pseudovariety of all finite aperiodic semigroups that can be described from the free generators using only the operations of multiplication and Ïpower. A necessary and sufficient condition for this property to hold turns out to be given by the conjunction of two rather simple finiteness conditions: the nonexistence of infinite antichains of factors and the rationality of the language of McCammond normal forms of Ïterms that define factors of the given pseudoword. The relationship between pseudowords with this property and arbitrary pseudowords is also investigated.}, }
 B. Bollig, P. Gastin, B. Monmege, M. Zeitoun, Pebble Weighted Automata and Weighted Logics. ACM Transactions on Computational Logic 15 (2), pp. 15:1â15:35, 2014. doi pdf abstract We introduce new classes of weighted automata on words. Equipped with pebbles, they go beyond the class of recognizable formal power series: they capture weighted firstorder logic enriched with a quantitative version of transitive closure. In contrast to previous work, this calculus allows for unrestricted use of existential and universal quantifications over positions of the input word. We actually consider both twoway and oneway pebble weighted automata. The latter class constrains the head of the automaton to walk lefttoright, resetting it each time a pebble is dropped. Such automata have already been considered in the Boolean setting, in the context of data words. Our main result states that twoway pebble weighted automata, oneway pebble weighted automata, and our weighted logic are expressively equivalent. We also give new logical characterizations of standard recognizable series. bibtex
@article{BGMZ:PebbleWeighted:14, author = {B. Bollig and P. Gastin and B. Monmege and M. Zeitoun}, title = {Pebble Weighted Automata and Weighted Logics}, journal = {{ACM Transactions on Computational Logic}}, volume = 15, number = 2, pages = {15:115:35}, year = {2014}, doi = {10.1145/2579819}, url = {http://tocl.acm.org/accepted/bolliggastin_pebble.pdf}, abstract = {We introduce new classes of weighted automata on words. Equipped with pebbles, they go beyond the class of recognizable formal power series: they capture weighted firstorder logic enriched with a quantitative version of transitive closure. In contrast to previous work, this calculus allows for unrestricted use of existential and universal quantifications over positions of the input word. We actually consider both twoway and oneway pebble weighted automata. The latter class constrains the head of the automaton to walk lefttoright, resetting it each time a pebble is dropped. Such automata have already been considered in the Boolean setting, in the context of data words. Our main result states that twoway pebble weighted automata, oneway pebble weighted automata, and our weighted logic are expressively equivalent. We also give new logical characterizations of standard recognizable series.}, }
 T. Place, L. van Rooijen, M. Zeitoun, On Separation by Locally Testable and Locally Threshold Testable Languages. Logical Methods in Computer Science 10 (3:24), pp. 1â28, 2014. doi pdf abstract A separator for two languages is a third language containing the first one and disjoint from the second one. We investigate the following decision problem: given two regular input languages, decide whether there exists a locally testable (resp. a locally threshold testable) separator. In both cases, we design a decision procedure based on the occurrence of special patterns in automata accepting the input languages. We prove that the problem is computationally harder than deciding membership. The correctness proof of the algorithm yields a stronger result, namely a description of a possible separator. Finally, we discuss the same problem for contextfree input languages. bibtex
@article{PvRZ:LTT:14, author = {T. Place and L. van Rooijen and M. Zeitoun}, title = {On Separation by Locally Testable and Locally Threshold Testable Languages}, journal = {Logical Methods in Computer Science}, year = {2014}, volume = 10, number = "3:24", pages = "128", url = {http://arxiv.org/pdf/1308.0181}, doi = {10.2168/LMCS10(3:24)2014}, abstract = {A separator for two languages is a third language containing the first one and disjoint from the second one. We investigate the following decision problem: given two regular input languages, decide whether there exists a locally testable (resp. a locally threshold testable) separator. In both cases, we design a decision procedure based on the occurrence of special patterns in automata accepting the input languages. We prove that the problem is computationally harder than deciding membership. The correctness proof of the algorithm yields a stronger result, namely a description of a possible separator. Finally, we discuss the same problem for contextfree input languages.} }
 B. Bollig, P. Gastin, B. Monmege, M. Zeitoun, Logical Characterization of Weighted Pebble Walking Automata. In CSLLICS'14, pp. 19:1â19:10, ACM. 2014. doi pdf abstract Weighted automata are a conservative quantitative extension of finite automata that enjoys applications, e.g., in language processing and speech recognition. Their expressive power, however, appears to be limited, especially when they are applied to more general structures than words, such as graphs. To address this drawback, weighted automata have recently been generalized to weighted pebble walking automata, which proved useful as a tool for the specification and evaluation of quantitative properties over words and nested words. In this paper, we establish the expressive power of weighted pebble walking automata in terms of transitive closure logic, lifting a similar result by Engelfriet and Hoogeboom from the Boolean case to a quantitative setting. This result applies to a general class of graphs that subsumes all the aforementioned classes. bibtex
@inproceedings{BGMZ:lics14, author = {B. Bollig and P. Gastin and B. Monmege and M. Zeitoun}, title = {Logical Characterization of Weighted Pebble Walking Automata}, booktitle = {{CSLLICS'14}}, year = {2014}, doi = {10.1145/2603088.2603118}, pages = {19:119:10}, publisher = {ACM}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/graphsBGMZlics14.pdf}, abstract = {Weighted automata are a conservative quantitative extension of finite automata that enjoys applications, e.g., in language processing and speech recognition. Their expressive power, however, appears to be limited, especially when they are applied to more general structures than words, such as graphs. To address this drawback, weighted automata have recently been generalized to weighted pebble walking automata, which proved useful as a tool for the specification and evaluation of quantitative properties over words and nested words. In this paper, we establish the expressive power of weighted pebble walking automata in terms of transitive closure logic, lifting a similar result by Engelfriet and Hoogeboom from the Boolean case to a quantitative setting. This result applies to a general class of graphs that subsumes all the aforementioned classes.} }
 T. Place, M. Zeitoun, Separating Regular Languages with FirstOrder Logic. In CSLLICS'14, pp. 75:1â75:10, ACM. 2014. doi pdf abstract Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular input languages of finite words, decide whether there exists a firstorder definable separator. We prove that in order to answer this question, sufficient information can be extracted from semigroups recognizing the input languages, using a fixpoint computation. This yields an EXPTIME algorithm for checking firstorder separability. Moreover, the correctness proof of this algorithm yields a stronger result, namely a description of a possible separator. Finally, we prove that this technique can be generalized to answer the same question for regular languages of infinite words. bibtex
@inproceedings{PZ:lics14, author = {T. Place and M. Zeitoun}, title = {Separating Regular Languages with FirstOrder Logic}, booktitle = {{CSLLICS'14}}, year = {2014}, pages = {75:175:10}, publisher = {ACM}, doi = {10.1145/2603088.2603098}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/PZLICS14.pdf}, abstract = {Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular input languages of finite words, decide whether there exists a firstorder definable separator. We prove that in order to answer this question, sufficient information can be extracted from semigroups recognizing the input languages, using a fixpoint computation. This yields an EXPTIME algorithm for checking firstorder separability. Moreover, the correctness proof of this algorithm yields a stronger result, namely a description of a possible separator. Finally, we prove that this technique can be generalized to answer the same question for regular languages of infinite words.}, }
 T. Place, M. Zeitoun, Going higher in the Firstorder Quantifier Alternation Hierarchy on Words. In ICALP'14, pp. 342â353, Springer. 2014. doi pdf abstract We investigate the quantifier alternation hierarchy in firstorder logic on finite words. Levels in this hierarchy are defined by counting the number of quantifier alternations in formulas. We prove that one can decide membership of a regular language to the levels BÎŁ2 (boolean combination of formulas having only 1 alternation) and ÎŁ3 (formulas having only 2 alternations beginning with an existential block). Our proof works by considering a deeper problem, called separation, which, once solved for lower levels, allows us to solve membership for higher levels. bibtex
@inproceedings{PZ:icalp14, author = {T. Place and M. Zeitoun}, title = {Going higher in the Firstorder Quantifier Alternation Hierarchy on Words}, booktitle = {{ICALP'14}}, year = {2014}, series = {Lect. Notes Comp. Sci.}, volume = 8573, pages = {342353}, editor = {Esparza, J. and Fraigniaud, P. and Husfeldt, T. and Koutsoupias, E.}, publisher = {Springer}, doi = {10.1007/9783662439517_29}, url = {http://arxiv.org/pdf/1404.6832v1}, abstract = {We investigate the quantifier alternation hierarchy in firstorder logic on finite words. Levels in this hierarchy are defined by counting the number of quantifier alternations in formulas. We prove that one can decide membership of a regular language to the levels BÎŁ2 (boolean combination of formulas having only 1 alternation) and ÎŁ3 (formulas having only 2 alternations beginning with an existential block). Our proof works by considering a deeper problem, called separation, which, once solved for lower levels, allows us to solve membership for higher levels.} }
2013
 L. van Rooijen, M. Zeitoun, The separation problem for regular languages by piecewise testable languages. , ArXiv. 2013. pdf abstract Separation is a classical problem in mathematics and computer science. It asks whether, given two sets belonging to some class, it is possible to separate them by another set of a smaller class. We present and discuss the separation problem for regular languages. We then give a direct polynomial time algorithm to check whether two given regular languages are separable by a piecewise testable language, that is, whether a BÎŁ1(<) sentence can witness that the languages are indeed disjoint. The proof is a reformulation and a refinement of an algebraic argument already given by Almeida and the second author. bibtex
@TechReport{vRZ:13, author = {L. van Rooijen and M. Zeitoun}, title = {The separation problem for regular languages by piecewise testable languages}, institution = {ArXiv}, year = 2013, url = {http://arxiv.org/abs/1303.2143}, abstract = {Separation is a classical problem in mathematics and computer science. It asks whether, given two sets belonging to some class, it is possible to separate them by another set of a smaller class. We present and discuss the separation problem for regular languages. We then give a direct polynomial time algorithm to check whether two given regular languages are separable by a piecewise testable language, that is, whether a BÎŁ1(<) sentence can witness that the languages are indeed disjoint. The proof is a reformulation and a refinement of an algebraic argument already given by Almeida and the second author.} }
 T. Place, L. van Rooijen, M. Zeitoun, Separating Regular Languages by Locally Testable and Locally Threshold Testable Languages. In FSTTCS'13, pp. 363375, Schloss Dagstuhl  LeibnizZentrum fĂŒr Informatik. 2013. doi pdf abstract A separator for two languages is a third language containing the first one and disjoint from the second one. We investigate the following decision problem: given two regular input languages, decide whether there exists a locally testable (resp. a locally threshold testable) separator. In both cases, we design a decision procedure based on the occurrence of special patterns in automata accepting the input languages. We prove that the problem is computationally harder than deciding membership. The correctness proof of the algorithm yields a stronger result, namely a description of a possible separator. Finally, we discuss the same problem for contextfree input languages. bibtex
@inproceedings{PRZ:fsttcs:13, author = {T. Place and L. van Rooijen and M. Zeitoun}, title = {Separating Regular Languages by Locally Testable and Locally Threshold Testable Languages}, booktitle = {FSTTCS'13}, year = {2013}, volume = {24}, series = {LIPIcs}, publisher = {Schloss Dagstuhl  LeibnizZentrum fĂŒr Informatik}, pages = {363375}, url = {http://drops.dagstuhl.de/opus/volltexte/2013/4386/pdf/27.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2013.363}, abstract = {A separator for two languages is a third language containing the first one and disjoint from the second one. We investigate the following decision problem: given two regular input languages, decide whether there exists a locally testable (resp. a locally threshold testable) separator. In both cases, we design a decision procedure based on the occurrence of special patterns in automata accepting the input languages. We prove that the problem is computationally harder than deciding membership. The correctness proof of the algorithm yields a stronger result, namely a description of a possible separator. Finally, we discuss the same problem for contextfree input languages.} }
 T. Place, L. van Rooijen, M. Zeitoun, Separating Regular Languages by Piecewise Testable and Unambiguous Languages. In MFCS'13, pp. 729740, Springer. 2013. doi pdf abstract Separation is a classical problem asking whether, given two sets belonging to some class, it is possible to separate them by a set from a smaller class. We discuss the separation problem for regular languages. We give a Ptime algorithm to check whether two given regular languages are separable by a piecewise testable language, that is, whether a BÎŁ1(<) sentence can witness that the languages are disjoint. The proof refines an algebraic argument from Almeida and the third author. When separation is possible, we also express a separator by saturating one of the original languages by a suitable congruence. Following the same line, we show that one can as well decide whether two regular languages can be separated by an unambiguous language, albeit with a higher complexity. bibtex
@inproceedings{PRZ:mfcs:13, author = {T. Place and L. van Rooijen and M. Zeitoun}, title = {Separating Regular Languages by Piecewise Testable and Unambiguous Languages}, booktitle = {{MFCS'13}}, year = {2013}, pages = {729740}, series = {Lect. Notes Comp. Sci.}, volume = {8087}, publisher = {Springer}, doi = {10.1007/9783642403132_64}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/mfcs13.pdf}, abstract = {Separation is a classical problem asking whether, given two sets belonging to some class, it is possible to separate them by a set from a smaller class. We discuss the separation problem for regular languages. We give a Ptime algorithm to check whether two given regular languages are separable by a piecewise testable language, that is, whether a BÎŁ1(<) sentence can witness that the languages are disjoint. The proof refines an algebraic argument from Almeida and the third author. When separation is possible, we also express a separator by saturating one of the original languages by a suitable congruence. Following the same line, we show that one can as well decide whether two regular languages can be separated by an unambiguous language, albeit with a higher complexity.} }
2012
 B. Bollig, P. Gastin, B. Monmege, M. Zeitoun, A Probabilistic Kleene Theorem. In ATVA'12, pp. 400â415, Springer. 2012. doi pdf abstract We provide a Kleene Theorem for (Rabin) probabilistic automata over finite words. Probabilistic automata generalize deterministic finite automata and assign to a word an acceptance probability. We provide probabilistic expressions with probabilistic choice, guarded choice, concatenation, and a star operator. We prove that probabilistic expressions and probabilistic automata are expressively equivalent. Our result actually extends to twoway probabilistic automata with pebbles and corresponding expressions. bibtex
@inproceedings{BGMZ:Atva:12, author = {B. Bollig and P. Gastin and B. Monmege and M. Zeitoun}, title = {A Probabilistic Kleene Theorem}, booktitle = {ATVA'12}, volume = 7561, year = 2012, pages = {400415}, editor = {Supratik Chakraborty and Madhavan Mukund}, publisher = {Springer}, series = {Lect. Notes Comp. Sci.}, doi = {10.1007/9783642333866_31}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/BGMZATVA12Probabilistic_Kleene.pdf}, abstract = {We provide a Kleene Theorem for (Rabin) probabilistic automata over finite words. Probabilistic automata generalize deterministic finite automata and assign to a word an acceptance probability. We provide probabilistic expressions with probabilistic choice, guarded choice, concatenation, and a star operator. We prove that probabilistic expressions and probabilistic automata are expressively equivalent. Our result actually extends to twoway probabilistic automata with pebbles and corresponding expressions.}, }
 R. Bonnet, A. Finkel, J. Leroux, M. Zeitoun, Model Checking Vector Addition Systems with one zerotest. Logical Methods in Computer Science 8 (2:11), pp. 1â25, 2012. doi pdf abstract We design a variation of the KarpMiller algorithm to compute, in a forward manner, a finite representation of the cover (i.e., the downward closure of the reachability set) of a vector addition system with one zerotest. This algorithm yields decision procedures for several problems for these systems, open until now, such as placeboundedness or LTL modelchecking. The proof techniques to handle the zerotest are based on two new notions of cover: the refined and the filtered cover. The refined cover is a hybrid between the reachability set and the classical cover. It inherits properties of the reachability set: equality of two refined covers is undecidable, even for usual Vector Addition Systems (with no zerotest), but the refined cover of a Vector Addition System is a recursive set. The second notion of cover, called the filtered cover, is the central tool of our algorithms. It inherits properties of the classical cover, and in particular, one can effectively compute a finite representation of this set, even for Vector Addition Systems with one zerotest. bibtex
@article{Bonnet&Finkel&Leroux&Zeitoun:2012, author = {R. Bonnet and A. Finkel and J. Leroux and M. Zeitoun}, title = {Model Checking Vector Addition Systems with one zerotest}, journal = {Logical Methods in Computer Science}, year = 2012, volume = 8, number = {2:11}, pages = {125}, doi = {10.2168/LMCS8(2:11)2012}, url = {http://arxiv.org/pdf/1205.4458}, abstract = {We design a variation of the KarpMiller algorithm to compute, in a forward manner, a finite representation of the cover (i.e., the downward closure of the reachability set) of a vector addition system with one zerotest. This algorithm yields decision procedures for several problems for these systems, open until now, such as placeboundedness or LTL modelchecking. The proof techniques to handle the zerotest are based on two new notions of cover: the refined and the filtered cover. The refined cover is a hybrid between the reachability set and the classical cover. It inherits properties of the reachability set: equality of two refined covers is undecidable, even for usual Vector Addition Systems (with no zerotest), but the refined cover of a Vector Addition System is a recursive set. The second notion of cover, called the filtered cover, is the central tool of our algorithms. It inherits properties of the classical cover, and in particular, one can effectively compute a finite representation of this set, even for Vector Addition Systems with one zerotest.}, }
2011
 B. Bollig, A. Cyriac, P. Gastin, M. Zeitoun, Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking. In MFCS'11, pp. 132144, Springer. 2011. doi pdf abstract We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic secondorder logic and that, in addition, allows PDLlike path expressions. This captures, in a unifying framework, a wide range of logics defined for ranked and unranked trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satisfiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities. bibtex
@inproceedings{BCGZ:MFCS:2011, author = {Bollig, B. and Cyriac, A. and Gastin, P. and Zeitoun, M.}, title = {Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking}, booktitle = {{MFCS'11}}, pages = {132144}, year = 2011, volume = 6907, series = {Lect. Notes. Comp Sci.}, publisher = {Springer}, doi = {10.1007/9783642229930_15}, url = {http://hal.archivesouvertes.fr/docs/00/59/11/39/PDF/report.pdf}, abstract = {We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic secondorder logic and that, in addition, allows PDLlike path expressions. This captures, in a unifying framework, a wide range of logics defined for ranked and unranked trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satisfiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities.}, }
2010
 R. Bonnet, A. Finkel, J. Leroux, M. Zeitoun, PlaceBoundedness for Vector Addition Systems with one zerotest. In FSTTCS'10, pp. 192â203, LeibnizZentrum fĂŒr Informatik. 2010. doi pdf abstract Reachability and boundedness problems have been shown decidable for Vector Addition Systems with one zerotest. Surprisingly, placeboundedness remained open. We provide here a variation of the KarpMiller algorithm to compute a basis of the downward closure of the reachability set which allows to decide placeboundedness. This forward algorithm is able to pass the zerotests thanks to a finer cover, hybrid between the reachability and cover sets, reclaiming accuracy on one component. We show that this filtered cover is still recursive, but that equality of two such filtered covers, even for usual Vector Addition Systems (with no zerotest), is undecidable. bibtex
@inproceedings{BFLZfsttcs10, author = {Bonnet, R. and Finkel, A. and Leroux, J. and Zeitoun, M.}, booktitle = {{FSTTCS'10}}, DOI = {10.4230/LIPIcs.FSTTCS.2010.192}, editor = {Lodaya, Kamal and Mahajan, Meena}, pages = {192203}, publisher = {LeibnizZentrum fĂŒr Informatik}, series = {LIPIcs}, volume = 8, year = 2010, title = {PlaceBoundedness for Vector Addition Systems with one zerotest}, url = {http://drops.dagstuhl.de/opus/volltexte/2010/2863/pdf/17.pdf}, abstract = {Reachability and boundedness problems have been shown decidable for Vector Addition Systems with one zerotest. Surprisingly, placeboundedness remained open. We provide here a variation of the KarpMiller algorithm to compute a basis of the downward closure of the reachability set which allows to decide placeboundedness. This forward algorithm is able to pass the zerotests thanks to a finer cover, hybrid between the reachability and cover sets, reclaiming accuracy on one component. We show that this filtered cover is still recursive, but that equality of two such filtered covers, even for usual Vector Addition Systems (with no zerotest), is undecidable.}, }
 B. Bollig, P. Gastin, B. Monmege, M. Zeitoun, Pebble weighted automata and transitive closure logics. In ICALP'10, pp. 587598, Springer. 2010. doi pdf abstract We introduce new classes of weighted automata on words. Equipped with pebbles and a twoway mechanism, they go beyond the class of recognizable formal power series, but capture a weighted version of firstorder logic with bounded transitive closure. In contrast to previous work, this logic allows for unrestricted use of universal quantification. Our main result states that pebble weighted automata, nested weighted automata, and this weighted logic are expressively equivalent. We also give new logical characterizations of the recognizable series. bibtex
@inproceedings{Bollig&Gastin&Monmege&Zeitoun:2010, author = {B. Bollig and P. Gastin and B. Monmege and M. Zeitoun}, title = {Pebble weighted automata and transitive closure logics}, booktitle = {{ICALP'10}}, editor = {Samson Abramsky}, pages = {587598}, year = 2010, volume = 6199, series = {Lect. Notes Comp. Sci.}, publisher = {Springer}, doi = {10.1007/9783642141621_49}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/BGMZicalp10.pdf}, abstract = {We introduce new classes of weighted automata on words. Equipped with pebbles and a twoway mechanism, they go beyond the class of recognizable formal power series, but capture a weighted version of firstorder logic with bounded transitive closure. In contrast to previous work, this logic allows for unrestricted use of universal quantification. Our main result states that pebble weighted automata, nested weighted automata, and this weighted logic are expressively equivalent. We also give new logical characterizations of the recognizable series.}, }
2009
 A. Muscholl, I. Walukiewicz, M. Zeitoun, A look at the control of asynchronous automata. In Perspectives in Concurrency Theory  A Festschrift for P.S. Thiagarajan, pp. 356â371, Universities Press. 2009. pdf abstract This paper is a survey of control of distributed systems. bibtex
@inbook{Muscholl&Walukiewicz&Zeitoun:08, author = {A. Muscholl and I. Walukiewicz and M. Zeitoun}, title = {A look at the control of asynchronous automata}, booktitle = {Perspectives in Concurrency Theory  A Festschrift for P.S. Thiagarajan}, pages = {356371}, year = 2009, editor = {K. Lodaya and M. Mukund and R. Ramanujam}, publisher = {Universities Press}, ISBN = {9788173716522}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/DistGamesMWZ.pdf}, abstract = {This paper is a survey of control of distributed systems.}, }
 J. Almeida, J.C. Costa, M. Zeitoun, Some structural properties of the free profinite aperiodic semigroup. In AutoMathA plenary conference, 2009. pdf abstract Profinite semigroups provide powerful tools to understand properties of classes of regular languages. Until very recently however, little was known on the structure of âlargeâ relatively free profinite semigroups. In this paper, we present new results obtained for the class of all finite aperiodic (that is, groupfree) semigroups. Given a finite alphabet X, we focus on the following problems: (1) the word problem for Ïterms on X evaluated on the free proaperiodic semigroup, and (2) the computation of closures of regular languages in the Ïsubsemigroup of the free proaperiodic semigroup generated by X. bibtex
@inproceedings{ACZ:automatha:09, author = {J. Almeida and J.C. Costa and M. Zeitoun}, title = {Some structural properties of the free profinite aperiodic semigroup}, booktitle = {AutoMathA plenary conference}, note = {Local proceedings}, year = 2009, url = {http://hal.archivesouvertes.fr/docs/00/94/89/98/PDF/ACZAutomatha09.pdf}, abstract = {Profinite semigroups provide powerful tools to understand properties of classes of regular languages. Until very recently however, little was known on the structure of "large" relatively free profinite semigroups. In this paper, we present new results obtained for the class of all finite aperiodic (that is, groupfree) semigroups. Given a finite alphabet X, we focus on the following problems: (1) the word problem for Ïterms on X evaluated on the free proaperiodic semigroup, and (2) the computation of closures of regular languages in the Ïsubsemigroup of the free proaperiodic semigroup generated by X.}, }
 P. Gastin, N. Sznajder, M. Zeitoun, Distributed synthesis for wellconnected architectures. Formal Methods in System Design 34 (3), pp. 215â239, 2009. doi pdf abstract We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures with arbitrary delays on processes. External means that the specification only relates input and output variables. We introduce the subclass of uniformly wellconnected (UWC) architectures for which there exists a routing allowing each output process to get the values of all inputs it is connected to, as soon as possible. We prove that the distributed synthesis problem is decidable on UWC architectures if and only if the output variables are totally ordered by their knowledge of input variables. We also show that if we extend this class by letting the routing depend on the output process, then the previous decidability result fails. Finally, we provide a natural restriction on specifications under which the whole class of UWC architectures is decidable. bibtex
@article{Gastin&Sznajder&Zeitoun:2009, author = {P. Gastin and N. Sznajder and M. Zeitoun}, title = {Distributed synthesis for wellconnected architectures}, journal = {Formal Methods in System Design}, year = {2009}, volume = {34}, number = {3}, pages = {215239}, doi = {10.1007/s1070300800647}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/DistSynthGSZ08.pdf}, abstract = {We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures with arbitrary delays on processes. External means that the specification only relates input and output variables. We introduce the subclass of uniformly wellconnected (UWC) architectures for which there exists a routing allowing each output process to get the values of all inputs it is connected to, as soon as possible. We prove that the distributed synthesis problem is decidable on UWC architectures if and only if the output variables are totally ordered by their knowledge of input variables. We also show that if we extend this class by letting the routing depend on the output process, then the previous decidability result fails. Finally, we provide a natural restriction on specifications under which the whole class of UWC architectures is decidable.}, }
2008
 J. Almeida, J. C. Costa, M. Zeitoun, â”terms over finite aperiodic semigroups. In Int. Conf. on Relations, Orders and Graphs, ROGICS'08, pp. 364â371, 2008. pdf abstract This paper provides a characterization of pseudowords over the pseudovariety of all finite aperiodic semigroups that are given by Ïterms, that is that can be obtained from the free generators using only multiplication and the Ïpower. A necessary and sufficient condition for this property to hold turns out to be given by the conjunction of two rather simple finiteness conditions: the nonexistence of infinite antichains of factors and the rationality of the language of McCammond normal forms of Ïterms that define factors. bibtex
@inproceedings{Almeida&Costa&Zeitoun:2008a, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {â”terms over finite aperiodic semigroups}, booktitle = {Int. Conf. on Relations, Orders and Graphs, ROGICS'08}, year = 2008, editor = {Y. Boudabbous and N. Zaguia}, pages = {364371}, isbn = {9780980949803}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/ACZ2008.pdf}, abstract = {This paper provides a characterization of pseudowords over the pseudovariety of all finite aperiodic semigroups that are given by Ïterms, that is that can be obtained from the free generators using only multiplication and the Ïpower. A necessary and sufficient condition for this property to hold turns out to be given by the conjunction of two rather simple finiteness conditions: the nonexistence of infinite antichains of factors and the rationality of the language of McCammond normal forms of Ïterms that define factors.} }
 R. Bernard, S. Metge, F. Pouzolz, P. Bieber, A. Griffault, M. Zeitoun, Altarica refinement for heterogeneous granularity models analysis. , pp. 2B3, HermĂšs. 2008. pdf abstract We define a notion of refinement for AltaRica models in order to analyze the safety of systems described at various levels of detail. We describe a technique based on the Mec V modelchecker to automatically check that one model refines another one. We present two theoretical results: the first one allows to verify refinement by focusing on one component of the model at a time, the second result defines the kind of requirements that are preserved by refinement. We propose to use these theoretical results in order to ease the safety assessment of a set of interconnected aeronautical systems. bibtex
@inproceedings{BMPBGZ08refinement, author = {R. Bernard and S. Metge and F. Pouzolz and P. Bieber and A. Griffault and M. Zeitoun}, title = {Altarica refinement for heterogeneous granularity models analysis}, note = {LambdaMu, 16Ăšme CongrĂšs de MaĂźtrise des Risques et de SĂ»retĂ© de Fonctionnement}, year = 2008, organization = {IMDRSdf}, publisher = {HermĂšs}, pages = {2B3}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/LM16_2B3_RB.pdf}, abstract = {We define a notion of refinement for AltaRica models in order to analyze the safety of systems described at various levels of detail. We describe a technique based on the Mec V modelchecker to automatically check that one model refines another one. We present two theoretical results: the first one allows to verify refinement by focusing on one component of the model at a time, the second result defines the kind of requirements that are preserved by refinement. We propose to use these theoretical results in order to ease the safety assessment of a set of interconnected aeronautical systems.} }
 B. Genest, A. Muscholl, O. Serre, M. Zeitoun, Tree pattern rewritting systems. In ATVA'08, pp. 332â346, Springer. 2008. doi pdf abstract Classical verification often uses abstraction when dealing with data. On the other hand, dynamic XMLbased applications have become pervasive, for instance with the ever growing importance of web services. We define here Tree Pattern Rewriting Systems (TPRS) as an abstract model of dynamic XMLbased documents. TPRS systems generate infinite transition systems, where states are unranked and unordered trees (hence possibly modeling XML documents). Their guarded transition rules are described by means of tree patterns. Our main result is that given a TPRS system (T , R), a tree pattern P and some integer k such that any reachable document from T has depth at most k, it is decidable (albeit of non elementary complexity) whether some tree matching P is reachable from T. bibtex
@InProceedings{Genest&Muscholl&Serre&Zeitoun:2008, author = {B. Genest and A. Muscholl and O. Serre and M. Zeitoun}, title = {Tree pattern rewritting systems}, booktitle = {ATVA'08}, editor = {M. Kim and M. Viswanathan}, pages = {332346}, year = 2008, volume = {5311}, series = {Lect. Notes Comp. Sci.}, publisher = {Springer}, doi = {10.1007/9783540883876_29}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/GenestMuschollSerreZeitounATVA2008long.pdf}, abstract = {Classical verification often uses abstraction when dealing with data. On the other hand, dynamic XMLbased applications have become pervasive, for instance with the ever growing importance of web services. We define here Tree Pattern Rewriting Systems (TPRS) as an abstract model of dynamic XMLbased documents. TPRS systems generate infinite transition systems, where states are unranked and unordered trees (hence possibly modeling XML documents). Their guarded transition rules are described by means of tree patterns. Our main result is that given a TPRS system (T , R), a tree pattern P and some integer k such that any reachable document from T has depth at most k, it is decidable (albeit of non elementary complexity) whether some tree matching P is reachable from T.} }
 N. Caniart, E. Fleury, J. Leroux, M. Zeitoun, Accelerating Interpolationbased ModelChecking. In TACAS'08, pp. 428442, Springer. 2008. doi pdf abstract Interpolationbased modelchecking and acceleration techniques have been widely proved successful and efficient for reachability checking. Surprisingly, these two techniques have never been combined to strengthen each other. Intuitively, acceleration provides underapproximation of the reachability set by computing the exact effect of some controlflow cycles and combining them with other transitions into an underapproximation. On the other hand, interpolationbased modelchecking is refining an overapproximation of the reachable states based on spurious errortraces. The goal of this paper is to combine acceleration techniques with interpolationbased modelchecking at the refinement stage. Our method, the socalled interpolant acceleration, helps to refine the abstraction, ruling out not only a single spurious errortrace but a possibly infinite set of errortraces obtained by any unrolling of its cycles. Interpolant acceleration is also proved to strictly enlarge the set of transformations that can be usually handled by acceleration techniques. bibtex
@InProceedings{caniart&fleury&leroux&zeitoun:2008:tacas, author = {N. Caniart and E. Fleury and J. Leroux and M. Zeitoun}, title = {Accelerating Interpolationbased ModelChecking}, booktitle = {TACAS'08}, Editor = {C. R. Ramakrishnan and J. Rehof}, publisher = {Springer}, series = {Lect. Notes Comp. Sci.}, year = 2008, volume = {4963}, pages = {428442}, doi = {10.1007/9783540788003_32}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/CaniartFleuryLerouxZeitoun.TACAS2008.pdf}, abstract = {Interpolationbased modelchecking and acceleration techniques have been widely proved successful and efficient for reachability checking. Surprisingly, these two techniques have never been combined to strengthen each other. Intuitively, acceleration provides underapproximation of the reachability set by computing the exact effect of some controlflow cycles and combining them with other transitions into an underapproximation. On the other hand, interpolationbased modelchecking is refining an overapproximation of the reachable states based on spurious errortraces. The goal of this paper is to combine acceleration techniques with interpolationbased modelchecking at the refinement stage. Our method, the socalled interpolant acceleration, helps to refine the abstraction, ruling out not only a single spurious errortrace but a possibly infinite set of errortraces obtained by any unrolling of its cycles. Interpolant acceleration is also proved to strictly enlarge the set of transformations that can be usually handled by acceleration techniques.}, }
 J. Almeida, J. C. Costa, M. Zeitoun, Pointlike sets with respect to R and J. J. Pure Applied Algebra 212 (3), pp. 486â499, Elsevier. 2008. doi pdf abstract We present an algorithm to compute the pointlike subsets of a finite semigroup with respect to the pseudovariety R of all finite Rtrivial semigroups. The algorithm is inspired by Henckellâs algorithm for computing the pointlike subsets with respect to the pseudovariety of all finite aperiodic semigroups. We also give an algorithm to compute Jpointlike sets, where J denotes the pseudovariety of all finite Jtrivial semigroups. We finally show that, in contrast with the situation for R, the natural adaptation of Henckellâs algorithm to J computes pointlike sets, but not all of them. bibtex
@Article{Almeida&Costa&Zeitoun:2008:ComputaPointlikeR, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {Pointlike sets with respect to R and J}, journal = {J. Pure Applied Algebra}, publisher = {Elsevier}, year = 2008, volume = 212, number = 3, pages = {486499}, doi = {10.1016/j.jpaa.2007.06.007}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaCostaZeitounJPAA08.pdf}, abstract = {We present an algorithm to compute the pointlike subsets of a finite semigroup with respect to the pseudovariety R of all finite Rtrivial semigroups. The algorithm is inspired by Henckellâs algorithm for computing the pointlike subsets with respect to the pseudovariety of all finite aperiodic semigroups. We also give an algorithm to compute Jpointlike sets, where J denotes the pseudovariety of all finite Jtrivial semigroups. We finally show that, in contrast with the situation for R, the natural adaptation of Henckellâs algorithm to J computes pointlike sets, but not all of them.} }
 J. Almeida, M. Zeitoun, Description and analysis of a bottomup DFA minimization algorithm. Information Processing Letters 107 (2), pp. 52â59, Elsevier. 2008. doi pdf abstract We establish lineartime reductions between the minimization of a deterministic finite automaton (DFA) and the conjunction of 3 subproblems: the minimization of a strongly connected DFA, the isomorphism problem for a set of strongly connected minimized DFAs, and the minimization of a connected DFA consisting in two strongly connected components, both of which are minimized. We apply this procedure to minimize, in linear time, automata whose nontrivial strongly connected components are cycles. bibtex
@Article{Almeida&Zeitoun:2008:BottomUpMinimization, author = {J. Almeida and M. Zeitoun}, title = {Description and analysis of a bottomup DFA minimization algorithm}, journal = {Information Processing Letters}, year = {2008}, publisher = {Elsevier}, volume = {107}, number = {2}, pages = {5259}, doi = {10.1016/j.ipl.2008.01.003}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaZeitounIPL2008.pdf}, abstract = {We establish lineartime reductions between the minimization of a deterministic finite automaton (DFA) and the conjunction of 3 subproblems: the minimization of a strongly connected DFA, the isomorphism problem for a set of strongly connected minimized DFAs, and the minimization of a connected DFA consisting in two strongly connected components, both of which are minimized. We apply this procedure to minimize, in linear time, automata whose nontrivial strongly connected components are cycles.} }
2007
 J. Almeida, M. Zeitoun, An automatatheoretic approach to the word problem for â”terms over R. Theoret. Comput. Sci. 370 (1â3), pp. 131â169, Elsevier. 2007. doi pdf abstract This paper studies the pseudovariety R of all finite Rtrivial semigroups. We give a representation of pseudowords over R by infinite trees, called Rtrees. Then we show that a pseudoword is an Ïterm if and only if its associated tree is regular (i.e., it can be folded into a finite graph), or equivalently, if the Ïterm has a finite number of tails. We give a linear algorithm to compute a compact representation of the Rtree for Ïterms, which yields a linear solution of the word problem for Ïterms over R. We finally exhibit a basis for the Ïvariety generated by R and we show that there is no finite basis. Several results can be compared to recent work of Bloom and Choffrut on long words. bibtex
@article{AZ:AutomTheorApproac:2007, author = {J. Almeida and M. Zeitoun}, title = {An automatatheoretic approach to the word problem for â”terms over R}, journal = {Theoret. Comput. Sci.}, pages = {131169}, volume = 370, number = {13}, publisher = {Elsevier}, doi = {10.1016/j.tcs.2006.10.019}, year = {2007}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaZeitounTCS2007.pdf}, abstract = {This paper studies the pseudovariety R of all finite Rtrivial semigroups. We give a representation of pseudowords over R by infinite trees, called Rtrees. Then we show that a pseudoword is an Ïterm if and only if its associated tree is regular (i.e., it can be folded into a finite graph), or equivalently, if the Ïterm has a finite number of tails. We give a linear algorithm to compute a compact representation of the Rtree for Ïterms, which yields a linear solution of the word problem for Ïterms over R. We finally exhibit a basis for the Ïvariety generated by R and we show that there is no finite basis. Several results can be compared to recent work of Bloom and Choffrut on long words.}, }
 J. Almeida, J. C. Costa, M. Zeitoun, Complete reducibility of systems of equations with respect to R. Portugaliae MatemĂĄtica 64 (4), pp. 445â508, Sociedade Portuguesa de Matematica. 2007. doi pdf abstract It is shown that the pseudovariety R of all finite Rtrivial semigroups is completely reducible with respect to the canonical signature. Informally, if the variables in a finite system of equations with rational constraints may be evaluated by pseudowords so that each value belongs to the closure of the corresponding rational constraint and the system is verified in R, then there is some such evaluation which is âregularâ, that is one in which, additionally, the pseudowords only involve multiplications and Ïpowers. bibtex
@Article{Almeida&Costa&Zeitoun:2007:CompleteReducibilityR, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {Complete reducibility of systems of equations with respect to R}, journal = {Portugaliae MatemĂĄtica}, publisher = {Sociedade Portuguesa de Matematica}, year = 2007, note = {Special issue}, volume = 64, number = 4, pages = {445508}, doi = {10.4171/PM/1792}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaCostaZeitounPortMath2007.pdf}, abstract = {It is shown that the pseudovariety R of all finite Rtrivial semigroups is completely reducible with respect to the canonical signature. Informally, if the variables in a finite system of equations with rational constraints may be evaluated by pseudowords so that each value belongs to the closure of the corresponding rational constraint and the system is verified in R, then there is some such evaluation which is âregularâ, that is one in which, additionally, the pseudowords only involve multiplications and Ïpowers.}, }
 J. Almeida, J. C. Costa, M. Zeitoun, Complete reducibility of pseudovarieties. In Proceedings of the Conference on Semigroups and Formal Languages (Lisbon, 2005), pp. 9â25, World Scientific. 2007. doi pdf abstract The notion of reducibility for a pseudovariety has been introduced as an abstract property which may be used to prove decidability results for various pseudovariety constructions. This paper is a survey of recent results establishing this and the stronger property of complete reducibility for specific pseudovarieties. bibtex
@InProceedings{Almeida&Costa&Zeitoun:CompleteReducibilityR:2007, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {Complete reducibility of pseudovarieties}, booktitle = {Proceedings of the Conference on Semigroups and Formal Languages (Lisbon, 2005)}, year = 2007, pages = {925}, publisher = {World Scientific}, doi = {10.1142/9789812708700_0002}, note = {In honour of D. McAlister's 65th birthday}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaCostaZeitounCSL07.pdf}, abstract = {The notion of reducibility for a pseudovariety has been introduced as an abstract property which may be used to prove decidability results for various pseudovariety constructions. This paper is a survey of recent results establishing this and the stronger property of complete reducibility for specific pseudovarieties.}, }
2006
 B. Genest, A. Muscholl, H. Seidl, M. Zeitoun, Infinitestate High level MSCs: realizability and modelchecking. Journal of Computer and System Sciences 72 (4), pp. 617â647, Elsevier. 2006. doi pdf abstract Message sequence charts (MSC) and HighLevel MSC (HMSC) is a visual notation for asynchronously communicating processes and a standard of the ITU. They usually represent incomplete specifications of required or forbidden properties of communication protocols. We consider in this paper two basic problems concerning the automated validation of HMSC sp ecifications, namely modelchecking and synthesis. We identify natural syntactic restrictions of HMSCs for which we can solve the above questions. We show first that modelchecking for globallycooperative (and locallycooperative) HMSCs is decidable within the same complexity as for the restricted class of bounded HMSCs. Furthermore, modelchecking localchoice HMSCs turns out to be as efficient as for finitestate (sequential) systems. The study of locallycooperative and localchoice HMSCs is motivated by the synthesis question, i.e., the question of implementing HMSCs through communicating finitestate machines (CFM) with additional message data. We show that locallycooperative and localchoice HMSCs are always implementable. Furthermore, the implementation of a localchoice HMSC is deadlockfree and of linear size. bibtex
@Article{genest&muscholl&seidl&zeitoun:2006:jcss, author = {B. Genest and A. Muscholl and H. Seidl and M. Zeitoun}, title = {Infinitestate High level MSCs: realizability and modelchecking}, journal = {Journal of Computer and System Sciences}, year = 2006, publisher = {Elsevier}, doi = {10.1016/j.jcss.2005.09.007}, volume = 72, number = 4, pages = {617647}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/InfStateHMSC.pdf}, abstract = {Message sequence charts (MSC) and HighLevel MSC (HMSC) is a visual notation for asynchronously communicating processes and a standard of the ITU. They usually represent incomplete specifications of required or forbidden properties of communication protocols. We consider in this paper two basic problems concerning the automated validation of HMSC sp ecifications, namely modelchecking and synthesis. We identify natural syntactic restrictions of HMSCs for which we can solve the above questions. We show first that modelchecking for globallycooperative (and locallycooperative) HMSCs is decidable within the same complexity as for the restricted class of bounded HMSCs. Furthermore, modelchecking localchoice HMSCs turns out to be as efficient as for finitestate (sequential) systems. The study of locallycooperative and localchoice HMSCs is motivated by the synthesis question, i.e., the question of implementing HMSCs through communicating finitestate machines (CFM) with additional message data. We show that locallycooperative and localchoice HMSCs are always implementable. Furthermore, the implementation of a localchoice HMSC is deadlockfree and of linear size.} }
 P. Gastin, N. Sznajder, M. Zeitoun, Distributed synthesis for wellconnected architectures. In FSTTCS'06, pp. 321â332, Springer. 2006. doi pdf abstract We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures with arbitrary delays on processes. External means that the specification only relates input and output variables. We introduce the subclass of uniformly wellconnected (UWC) architectures for which there exists a routing allowing each output process to get the values of all inputs it is connected to, as soon as possible. We prove that the distributed synthesis problem is decidable on UWC architectures if and only if the set of all sets of input variables visible by output variables is totally ordered, under set inclusion. We also show that if we extend this class by letting the routing depend on the output process, then the previous decidability result fails. Finally, we provide a natural restriction on specifications under which the whole class of UWC architectures is decidable. bibtex
@InProceedings{gastin&sznajder&zeitoun:2006:fsttcs, author = {P. Gastin and N. Sznajder and M. Zeitoun}, title = {Distributed synthesis for wellconnected architectures}, booktitle = {{FSTTCS'06}}, Editor = {Garg, Naveen and ArunKumar, S.}, publisher = {Springer}, series = {Lect. Notes Comp. Sci.}, year = 2006, volume = {4337}, pages = {321332}, doi = {10.1007/11944836}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/GastinSznajderZeitounFSTTCS06.pdf}, abstract = {We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures with arbitrary delays on processes. External means that the specification only relates input and output variables. We introduce the subclass of uniformly wellconnected (UWC) architectures for which there exists a routing allowing each output process to get the values of all inputs it is connected to, as soon as possible. We prove that the distributed synthesis problem is decidable on UWC architectures if and only if the set of all sets of input variables visible by output variables is totally ordered, under set inclusion. We also show that if we extend this class by letting the routing depend on the output process, then the previous decidability result fails. Finally, we provide a natural restriction on specifications under which the whole class of UWC architectures is decidable.}, }
2005
 L. HĂ©louĂ«t, M. Zeitoun, A. Degorre, Scenarios and Covert channels, another gameâŠ. In Games in Design and Verification, GDV '04, pp. 93â116, Elsevier. 2005. doi pdf abstract Covert channels are information leaks in systems that use resources to transfer secretly a message. They are a threat for security, performance, but also for a system's profitability. This paper proposes a new approach to detect covert channels from scenario models of protocols. The problem of finding covert channels in scenarios is first modeled as a game, in which a pair of malicious users {S,R} is trying to transfer information while the rest of the protocol tries to prevent it. The messages transferred are encoded by behavioral choices at some precise moments, and decoded by a transducer whose input vocabulary is an observation of the system. We then characterize the presence of a covert channel as the existence of a winning strategy for {S,R} and of a decoder. bibtex
@InProceedings{helouet&zeitoun°orre:2005, author = {L. HĂ©louĂ«t and M. Zeitoun and A. Degorre}, title = {Scenarios and Covert channels, another game...}, booktitle = {Games in Design and Verification, GDV '04}, year = 2005, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier}, volume = 119, number = 1, pages = {93116}, doi = {10.1016/j.entcs.2004.07.010}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/GDV04.pdf}, abstract = {Covert channels are information leaks in systems that use resources to transfer secretly a message. They are a threat for security, performance, but also for a system's profitability. This paper proposes a new approach to detect covert channels from scenario models of protocols. The problem of finding covert channels in scenarios is first modeled as a game, in which a pair of malicious users {S,R} is trying to transfer information while the rest of the protocol tries to prevent it. The messages transferred are encoded by behavioral choices at some precise moments, and decoded by a transducer whose input vocabulary is an observation of the system. We then characterize the presence of a covert channel as the existence of a winning strategy for {S,R} and of a decoder.} }
 J. Almeida, J. C. Costa, M. Zeitoun, Tameness of pseudovariety joins involving R. Monatshefte fĂŒr Mathematik 146 (2), pp. 89â111, 2005. doi pdf abstract In this paper, we establish several decidability results for pseudovariety joins of the form V âš W, where V is a subpseudovariety of J or the pseudovariety R. Here, J (resp. R) denotes the pseudovariety of all Jtrivial (resp. Rtrivial) semigroups. In particular, we show that the pseudovariety V âš W is (completely) Îștame when V is a subpseudovariety of J with decidable Îșword problem and W is (completely) Îștame. Moreover, if W is a Îștame pseudovariety which satisfies the pseudoidentity x1 Â·Â·Â·xry^(Ï+1)zt^Ï = x1 Â·Â·Â·xryzt^Ï, then we prove that R âš W is also Îștame. In particular the joins RâšAb, RâšG, RâšOCR, and RâšCR are decidable. bibtex
@Article{almeida&costa&zeitoun:2005:monatshefte, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {Tameness of pseudovariety joins involving R}, journal = {Monatshefte fĂŒr Mathematik}, volume = 146, number = 2, pages = {89111}, doi = {10.1007/s0060500503241}, year = 2005, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaCostaZeitounMonatsHefte05.pdf}, abstract = {In this paper, we establish several decidability results for pseudovariety joins of the form V âš W, where V is a subpseudovariety of J or the pseudovariety R. Here, J (resp. R) denotes the pseudovariety of all Jtrivial (resp. Rtrivial) semigroups. In particular, we show that the pseudovariety V âš W is (completely) Îștame when V is a subpseudovariety of J with decidable Îșword problem and W is (completely) Îștame. Moreover, if W is a Îștame pseudovariety which satisfies the pseudoidentity x1 Â·Â·Â·xry^(Ï+1)zt^Ï = x1 Â·Â·Â·xryzt^Ï, then we prove that R âš W is also Îștame. In particular the joins RâšAb, RâšG, RâšOCR, and RâšCR are decidable.} }
2004
 M. Zeitoun, Concurrence et automates. , 2004. bibtex
@phdthesis{zeitoun:2004:hdr, author = {M. Zeitoun}, title = {Concurrence et automates}, year = 2004, school = {UniversitĂ© Paris 7}, type = {Habilitation Ă diriger des recherches} }
 P. Gastin, P. Moro, M. Zeitoun, Minimization of counterexamples in SPIN. In SPIN'04, pp. 92â108, Springer. 2004. doi pdf abstract We propose an algorithm to find a counterexample to some property in a finite state program. This algorithm is derived from SPIN's one, but it finds a counterexample faster than SPIN does. In particular it still works in linear time. Compared with SPIN's algorithm, it requires only one additional bit per state stored. We further propose another algorithm to compute a counterexample of minimal size. Again, this algorithm does not use more memory than SPIN does to approximate a minimal counterexample. The cost to find a counterexample of minimal size is that one has to revisit more states than SPIN. We provide an implementation and discuss experimental results. bibtex
@InProceedings{gastin&moro&zeitoun:2004:spin, author = {P. Gastin and P. Moro and M. Zeitoun}, title = {Minimization of counterexamples in SPIN}, booktitle = {{SPIN'04}}, publisher = {Springer}, series = {Lect. Notes Comp. Sci.}, year = 2004, volume = 2989, pages = {92108}, doi = {10.1007/b96721}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/SPIN04.pdf}, abstract = {We propose an algorithm to find a counterexample to some property in a finite state program. This algorithm is derived from SPIN's one, but it finds a counterexample faster than SPIN does. In particular it still works in linear time. Compared with SPIN's algorithm, it requires only one additional bit per state stored. We further propose another algorithm to compute a counterexample of minimal size. Again, this algorithm does not use more memory than SPIN does to approximate a minimal counterexample. The cost to find a counterexample of minimal size is that one has to revisit more states than SPIN. We provide an implementation and discuss experimental results.} }
 P. Gastin, B. Lerman, M. Zeitoun, Distributed games with causal memory are decidable for seriesparallel systems. In FSTTCS'04, pp. 275â286, Springer. 2004. doi pdf abstract This paper deals with distributed control problems by means of distributed games played on Mazurkiewicz traces. The main difference with other notions of distributed games recently introduced is that, instead of having a local view, strategies and controllers are able to use a more accurate memory, based on their causal view. Our main result states that using the causal view makes the control synthesis problem decidable for seriesparallel systems for all recognizable winning conditions on finite behaviors, while this problem with local view was proved undecidable even for reachability conditions. bibtex
@InProceedings{gastin&lerman&zeitoun:2004:fsttcs, author = {P. Gastin and B. Lerman and M. Zeitoun}, title = {Distributed games with causal memory are decidable for seriesparallel systems}, Booktitle = {{FSTTCS'04}}, publisher = {Springer}, series = {Lect. Notes Comp. Sci.}, year = 2004, volume = 3328, pages = {275286}, doi = {10.1007/9783540305385_23}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/GastinLermanZeitounFSTTCS04.pdf}, abstract = {This paper deals with distributed control problems by means of distributed games played on Mazurkiewicz traces. The main difference with other notions of distributed games recently introduced is that, instead of having a local view, strategies and controllers are able to use a more accurate memory, based on their causal view. Our main result states that using the causal view makes the control synthesis problem decidable for seriesparallel systems for all recognizable winning conditions on finite behaviors, while this problem with local view was proved undecidable even for reachability conditions.}, }
 P. Gastin, B. Lerman, M. Zeitoun, Distributed games and distributed control for asynchronous systems. In LATIN'04, pp. 455â465, Springer. 2004. doi pdf abstract We introduce distributed games over asynchronous transition systems to model a distributed controller synthesis problem. A game involves two teams and is not turnbased: several players of both teams may simultaneously be enabled. We define distributed strategies based on the causal view that players have of the system. We reduce the problem of finding a winning distributed strategy with a given memory to finding a memoryless winning distributed strategy in a larger distributed game. We reduce the latter problem to finding a strategy in a a classical 2players game. This allows to transfer results from the sequential case to this distributed setting. bibtex
@InProceedings{gastin&lerman&zeitoun:2004:latin, author = {P. Gastin and B. Lerman and M. Zeitoun}, title = {Distributed games and distributed control for asynchronous systems}, booktitle = {{LATIN'04}}, editor = {FarachColton, M.}, publisher = {Springer}, pages = {455465}, series = {Lect. Notes Comp. Sci.}, year = 2004, volume = 2976, doi = {10.1007/b95852}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/LATIN04.pdf}, abstract = {We introduce distributed games over asynchronous transition systems to model a distributed controller synthesis problem. A game involves two teams and is not turnbased: several players of both teams may simultaneously be enabled. We define distributed strategies based on the causal view that players have of the system. We reduce the problem of finding a winning distributed strategy with a given memory to finding a memoryless winning distributed strategy in a larger distributed game. We reduce the latter problem to finding a strategy in a a classical 2players game. This allows to transfer results from the sequential case to this distributed setting.}, }
 J. Almeida, M. Zeitoun, The equational theory of â”terms for finite Rtrivial semigroups. In Semigroups and Languages, pp. 1â23, World Scientific. 2004. doi pdf abstract A new topological representation for free profinite Rtrivial semigroups in terms of spaces of vertexlabeled complete binary trees is obtained. Such a tree may be naturally folded into a finite automaton if and only if the element it represents is an Ïterm. The variety of Ïsemigroups generated by all finite Rtrivial semigroups, with the usual interpretation of the Ïpower, is then studied. A simple infinite basis of identities is exhibited and a lineartime solution of the word problem for relatively free Ïsemigroups is presented. This work is also compared with recent work of Bloom and Choffrut on transfinite words. bibtex
@InProceedings{almeida&zeitoun:2004:sal, author = {J. Almeida and M. Zeitoun}, title = {The equational theory of â”terms for finite Rtrivial semigroups}, booktitle = {Semigroups and Languages}, editor = {M. Branco and G.M.S. Gomes}, year = 2004, publisher = {World Scientific}, doi = {10.1142/9789812702616_0001}, pages = {123}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/Lisbon03.pdf}, abstract = {A new topological representation for free profinite Rtrivial semigroups in terms of spaces of vertexlabeled complete binary trees is obtained. Such a tree may be naturally folded into a finite automaton if and only if the element it represents is an Ïterm. The variety of Ïsemigroups generated by all finite Rtrivial semigroups, with the usual interpretation of the Ïpower, is then studied. A simple infinite basis of identities is exhibited and a lineartime solution of the word problem for relatively free Ïsemigroups is presented. This work is also compared with recent work of Bloom and Choffrut on transfinite words.} }
2003
 L. HĂ©louĂ«t, C. Jard, M. Zeitoun, Covert channels detection in protocols using scenarios. In SPV'03, Security Protocols Verification, pp. 21â25, 2003. pdf abstract This paper presents an approach to detect illegal information flows from requirements expressed as highlevel scenarios. bibtex
@InProceedings{helouet&jard&zeitoun:2003:spv, author = {L. HĂ©louĂ«t and C. Jard and M. Zeitoun}, title = {Covert channels detection in protocols using scenarios}, booktitle = {{SPV'03, Security Protocols Verification}}, editor = {M. Rusinowitch}, year = 2003, pages = {2125}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/spv03.pdf}, abstract = {This paper presents an approach to detect illegal information flows from requirements expressed as highlevel scenarios.}, }
 J. Almeida, M. Zeitoun, Tameness of some locally trivial pseudovarieties. Comm. Algebra 31 (1), pp. 61â77, 2003. doi pdf abstract Tameness is a strong property of semigroup pseudovarieties related to the membership problem. Let Îș be the signature comprising semigroup multiplication and the omega implicit operation. We prove the Îștameness of the pseudovarieties N, D, K and LI. bibtex
@Article{almeida&zeitoun:2003:commalg, author = {J. Almeida and M. Zeitoun}, title = {Tameness of some locally trivial pseudovarieties}, journal = {Comm. Algebra}, year = 2003, volume = 31, number = 1, pages = {6177}, doi = {10.1081/AGB120016749}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaZeitounCommAlgebra2003.pdf}, abstract = {Tameness is a strong property of semigroup pseudovarieties related to the membership problem. Let Îș be the signature comprising semigroup multiplication and the omega implicit operation. We prove the Îștameness of the pseudovarieties N, D, K and LI.} }
2002
 B. Genest, A. Muscholl, H. Seidl, M. Zeitoun, Infinitestate High level MSCs: realizability and modelchecking. In ICALP'02, pp. 657â668, Springer. 2002. doi pdf abstract Message sequence charts (MSC) and HighLevel MSC (HMSC) is a visual notation for asynchronously communicating processes and a standard of the ITU. They usually represent incomplete specifications of required or forbidden properties of communication protocols. We consider in this paper two basic problems concerning the automated validation of HMSC sp ecifications, namely modelchecking and synthesis. We identify natural syntactic restrictions of HMSCs for which we can solve the above questions. We show first that modelchecking for globallycooperative (and locallycooperative) HMSCs is decidable within the same complexity as for the restricted class of bounded HMSCs. Furthermore, modelchecking localchoice HMSCs turns out to be as efficient as for finitestate (sequential) systems. The study of locallycooperative and localchoice HMSCs is motivated by the synthesis question, i.e., the question of implementing HMSCs through communicating finitestate machines (CFM) with additional message data. We show that locallycooperative and localchoice HMSCs are always implementable. Furthermore, the implementation of a localchoice HMSC is deadlockfree and of linear size. bibtex
@InProceedings{genest&muscholl&seidl&zeitoun:2002, author = {B. Genest and A. Muscholl and H. Seidl and M. Zeitoun}, title = {{Infinitestate High level MSCs: realizability and modelchecking}}, booktitle = {{ICALP'02}}, editor = {P. Widmayer and others}, pages = {657668}, year = 2002, volume = 2380, series = {Lect. Notes Comp. Sci.}, publisher = {Springer}, doi = {10.1007/3540454659_56}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/InfHMSC.pdf}, abstract = {Message sequence charts (MSC) and HighLevel MSC (HMSC) is a visual notation for asynchronously communicating processes and a standard of the ITU. They usually represent incomplete specifications of required or forbidden properties of communication protocols. We consider in this paper two basic problems concerning the automated validation of HMSC sp ecifications, namely modelchecking and synthesis. We identify natural syntactic restrictions of HMSCs for which we can solve the above questions. We show first that modelchecking for globallycooperative (and locallycooperative) HMSCs is decidable within the same complexity as for the restricted class of bounded HMSCs. Furthermore, modelchecking localchoice HMSCs turns out to be as efficient as for finitestate (sequential) systems. The study of locallycooperative and localchoice HMSCs is motivated by the synthesis question, i.e., the question of implementing HMSCs through communicating finitestate machines (CFM) with additional message data. We show that locallycooperative and localchoice HMSCs are always implementable. Furthermore, the implementation of a localchoice HMSC is deadlockfree and of linear size.}, }
2000
 Ă. Badouel, S. Boucheron, A. Dicky, A. Petit, M. Santha, P. Weil, M. Zeitoun, Probl. I2000. In ProblĂšmes d'informatique corrigĂ©s, Springer. 2000. bibtex
@InBook{badouel&boucheron&dicky&petit&santha&weil&zeitoun:2000:b, author = {Ă. Badouel and S. Boucheron and A. Dicky and A. Petit and M. Santha and P. Weil and M. Zeitoun}, booktitle = {ProblĂšmes d'informatique corrigĂ©s}, title = {{Probl. I2000}}, publisher = {Springer}, year = 2000, note = {Coord. A. Petit} }
 Ă. Badouel, S. Boucheron, A. Dicky, A. Petit, M. Santha, P. Weil, M. Zeitoun, Probl. I99. In ProblĂšmes d'informatique corrigĂ©s, Springer. 2000. bibtex
@InBook{badouel&boucheron&dicky&petit&santha&weil&zeitoun:2000:a, author = {Ă. Badouel and S. Boucheron and A. Dicky and A. Petit and M. Santha and P. Weil and M. Zeitoun}, booktitle = {ProblĂšmes d'informatique corrigĂ©s}, title = {{Probl. I99}}, publisher = {Springer}, year = 2000, note = {Coord. A. Petit} }
1999
 J. Almeida, A. Azevedo, M. Zeitoun, Pseudovariety joins involving Jtrivial semigroups and completely regular semigroups. Internat. J. Algebra Comput. 9 (1), pp. 99â112, 1999. doi pdf abstract J. Rhodes asked during the Chico conference in 1986 for the calculation of joins of semigroup pseudovarieties. This paper proves that the join JâšV of the pseudovariety J of J trivial semigroups and of any 2strongly decidable pseudovariety V of completely regular semigroups is decidable. This problem was proposed by the first author for V = G, the pseudovariety of finite groups. bibtex
@Article{almeida&azevedo&zeitoun:1999:ijac, author = {J. Almeida and A. Azevedo and M. Zeitoun}, title = {{Pseudovariety joins involving Jtrivial semigroups and completely regular semigroups}}, journal = {Internat. J. Algebra Comput.}, year = 1999, volume = 9, number = 1, pages = {99112}, doi = {10.1142/S0218196799000072}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/JvG.pdf}, abstract = {J. Rhodes asked during the Chico conference in 1986 for the calculation of joins of semigroup pseudovarieties. This paper proves that the join JâšV of the pseudovariety J of J trivial semigroups and of any 2strongly decidable pseudovariety V of completely regular semigroups is decidable. This problem was proposed by the first author for V = G, the pseudovariety of finite groups.}, }
1998
 A. Azevedo, M. Zeitoun, Three examples of join computations. Semigroup Forum 57 (2), pp. 249â277, 1998. doi pdf abstract This article answers three questions of J. Almeida. Using combinatorial, algebraic and topological methods, we compute joins involving the pseudovariety of finite groups, the pseudovariety of semigroups in which each idempotent is a right zero and the pseudovariety generated by monoids M such that each idempotent of M{1} is a left zero. bibtex
@Article{azevedo&zeitoun:1998:sgf, author = {A. Azevedo and M. Zeitoun}, title = {Three examples of join computations}, journal = {Semigroup Forum}, year = 1998, volume = 57, number = 2, pages = {249277}, doi = {10.1007/PL00005976}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/MKvDvG.pdf}, abstract = {This article answers three questions of J. Almeida. Using combinatorial, algebraic and topological methods, we compute joins involving the pseudovariety of finite groups, the pseudovariety of semigroups in which each idempotent is a right zero and the pseudovariety generated by monoids M such that each idempotent of M{1} is a left zero.}, }
1997
 M. Zeitoun, On embeddings of finitely generated profinite semigroups into 2generated profinite semigroups. Algebra Universalis 38 (2), pp. 210â213, 1997. doi pdf abstract Koryakov recently asked the following question: when a pseudovariety V does not satisfy any nontrivial identity, does there exist an embedding from any finitely generated Vfree profinite semigroup into the 2generated Vfree profinite semigroup? During the conference âSemigroups, Automata and Languagesâ in Porto (June 1994), a positive answer to this question was conjectured. We give here a counterexample to this conjecture. bibtex
@Article{zeitoun:1997:au, author = {M. Zeitoun}, title = {On embeddings of finitely generated profinite semigroups into 2generated profinite semigroups}, journal = {Algebra Universalis}, year = 1997, volume = 38, number = 2, pages = {210213}, doi = {10.1007/s000120050049}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/Embedding.pdf}, abstract = {Koryakov recently asked the following question: when a pseudovariety V does not satisfy any nontrivial identity, does there exist an embedding from any finitely generated Vfree profinite semigroup into the 2generated Vfree profinite semigroup? During the conference âSemigroups, Automata and Languagesâ in Porto (June 1994), a positive answer to this question was conjectured. We give here a counterexample to this conjecture.} }
 J. Almeida, M. Zeitoun, The pseudovariety J is hyperdecidable. RAIRO Inform. ThĂ©or. Appl. 31 (5), pp. 457â482, EDP Sciences. 1997. pdf abstract This article defines the notion of hyperdecidability for a class of finite semigroups, which is closely connected to the notion of decidability. It then proves that the pseudovariety J of Jtrivial semigroups is hyperdecidable. bibtex
@Article{almeida&zeitoun:1997:rairo, author = {J. Almeida and M. Zeitoun}, title = {{The pseudovariety J is hyperdecidable}}, year = 1997, volume = 31, number = 5, pages = {457482}, journal = {{RAIRO Inform. ThĂ©or. Appl.}}, publisher = {EDP Sciences}, url = {http://archive.numdam.org/article/ITA_1997__31_5_457_0.pdf}, abstract = {This article defines the notion of hyperdecidability for a class of finite semigroups, which is closely connected to the notion of decidability. It then proves that the pseudovariety J of Jtrivial semigroups is hyperdecidable.}, }
1996
 M. Zeitoun, On the join of two pseudovarieties. In Semigroups, Automata and Languages, pp. 281â288, World Scientific. 1996. pdf abstract This paper is a survey of some recent developments in the theory of finite semigroups. bibtex
@Inproceedings{zeitoun:1996:a, author = {M. Zeitoun}, title = {On the join of two pseudovarieties}, booktitle = {{Semigroups, Automata and Languages}}, year = 1996, pages = {281288}, editor = {J. Almeida and G.M.S. Gomes and P.V. Silva}, publisher = {World Scientific}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/SAL.pdf}, abstract = {This paper is a survey of some recent developments in the theory of finite semigroups.} }
1995
 M. Zeitoun, The join of the pseudovarieties of idempotent semigroups and locally trivial semigroups. Semigroup Forum 50, pp. 367â381, 1995. doi pdf abstract This article solves a problem proposed by Almeida: the computation of the join of two wellknown pseudovarieties of semigroups, namely the pseudovariety of bands and the pseudovariety of locally trivial semigroups. We use a method developed by Almeida, based on the theory of implicit operations. bibtex
@Article{zeitoun:1995:sgf, author = {M. Zeitoun}, title = {The join of the pseudovarieties of idempotent semigroups and locally trivial semigroups}, journal = {Semigroup Forum}, year = 1995, volume = 50, pages = {367381}, doi = {10.1007/BF02573532}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/LIvB.pdf}, abstract = {This article solves a problem proposed by Almeida: the computation of the join of two wellknown pseudovarieties of semigroups, namely the pseudovariety of bands and the pseudovariety of locally trivial semigroups. We use a method developed by Almeida, based on the theory of implicit operations.}, }
1994
 M. Zeitoun, On the decidability of the membership problem of the pseudovariety JvB. Internat. J. Algebra Comput. 4 (4), pp. 47â64, 1994. doi pdf abstract The aim of this article is to prove that the pseudovariety generated by JâȘB, that is to say, the join of the pseudovariety of Jtrivial semigroups and of the pseudovariety of idempotents semigroups, is decidable. The techniques used were developed by Almeida and are based on the study of the topological semigroup of implicit operations. bibtex
@Article{zeitoun:1994:ijac, author = {M. Zeitoun}, title = {{On the decidability of the membership problem of the pseudovariety JvB}}, journal = {Internat. J. Algebra Comput.}, year = 1994, volume = 4, number = 4, pages = {4764}, doi = {10.1142/S0218196795000057}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/JvBd.pdf}, abstract = {The aim of this article is to prove that the pseudovariety generated by JâȘB, that is to say, the join of the pseudovariety of Jtrivial semigroups and of the pseudovariety of idempotents semigroups, is decidable. The techniques used were developed by Almeida and are based on the study of the topological semigroup of implicit operations.}, }
1993
 M. Zeitoun, OpĂ©rations implicites et variĂ©tĂ©s de semigroupes finis. , 1993. bibtex
@phdthesis{zeitoun:1993:phd, author = {M. Zeitoun}, title = {OpĂ©rations implicites et variĂ©tĂ©s de semigroupes finis}, year = 1993, school = {UniversitĂ© Paris 7}, type = {ThĂšse de doctorat} }
1988
 M. Zeitoun, Programmes sur monoĂŻdes finis. , 1988. bibtex
@masterthesis{zeitoun:1988:dea, author = {M. Zeitoun}, title = {Programmes sur monoĂŻdes finis}, school = {UniversitĂ© Paris 7}, year = 1988, type = {{MĂ©moire de DEA}}, note = {Rapports de recherche CERIL et LITP} }
 Only Journal articles
2016
 J. Almeida, J. C. Costa, M. Zeitoun, Reducibility of Pointlike Problems. Semigroup Forum, 2016. doi pdf abstract We show that the pointlike and the idempotent pointlike problems are reducible with respect to natural signatures in the following cases: the pseudovariety of all finite semigroups in which the order of every subgroup is a product of elements of a fixed set Ï of primes; the pseudovariety of all finite semigroups in which every regular Jclass is the product of a rectangular band by a group from a fixed pseudovariety of groups that is reducible for the pointlike problem, respectively graph reducible. Allowing only trivial groups, we obtain Ïreducibility of the pointlike and idempotent pointlike problems, respectively for the pseudovarieties of all finite aperiodic semigroups (A) and of all finite semigroups in which all regular elements are idempotents (DA). bibtex
@article{reducibility:acz:2015, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {Reducibility of Pointlike Problems}, journal = {Semigroup Forum}, year = 2016, doi = {10.1007/s0023301597692}, url = {http://arxiv.org/pdf/1507.03076v1.pdf}, abstract = "We show that the pointlike and the idempotent pointlike problems are reducible with respect to natural signatures in the following cases: the pseudovariety of all finite semigroups in which the order of every subgroup is a product of elements of a fixed set Ï of primes; the pseudovariety of all finite semigroups in which every regular Jclass is the product of a rectangular band by a group from a fixed pseudovariety of groups that is reducible for the pointlike problem, respectively graph reducible. Allowing only trivial groups, we obtain Ïreducibility of the pointlike and idempotent pointlike problems, respectively for the pseudovarieties of all finite aperiodic semigroups (A) and of all finite semigroups in which all regular elements are idempotents (DA).", note = {To appear} }
 T. Place, M. Zeitoun, Separating Regular Languages with FirstOrder Logic. Logical Methods in Computer Science 12 (1), pp. 1â30, 2016. doi pdf abstract Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem, called separation: given two regular languages of finite words, decide whether there exists a firstorder definable separator. A more general problem was solved in an algebraic framework by Henckell in 1988, although the connection with separation was pointed out only in 1996, by Almeida. The result was then generalized by Henckell, Steinberg and Rhodes in 2010. In this paper, we present a new, selfcontained and elementary proof of it, which actually covers the original result of Henckell. We prove that in order to answer this question, sufficient information can be extracted from semigroups recognizing the input languages, using a fixpoint computation, similar to that originally proposed by Henckell. Given as input a morphism recognizing both languages to be separated, this yields an Exptime algorithm for checking firstorder separability. Moreover, the correctness proof of this algorithm yields a stronger result, namely a description of a possible separator. More precisely, one can compute a bound on the quantifier rank of potential separators, as well as a firstorder formula that describes a separator, if there exists one. Finally, we prove that this technique can be generalized to answer the same question for regular languages of infinite words. bibtex
@Article{PZ:FOSep16, author = {T. Place and M. Zeitoun}, title = {Separating Regular Languages with FirstOrder Logic}, journal = {Logical Methods in Computer Science}, year = 2016, url = {http://arxiv.org/pdf/1402.3277v3}, volume = 12, number = 1, pages = {130}, doi = {10.2168/LMCS12(1:5)2016}, abstract = {Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem, called separation: given two regular languages of finite words, decide whether there exists a firstorder definable separator. A more general problem was solved in an algebraic framework by Henckell in 1988, although the connection with separation was pointed out only in 1996, by Almeida. The result was then generalized by Henckell, Steinberg and Rhodes in 2010. In this paper, we present a new, selfcontained and elementary proof of it, which actually covers the original result of Henckell. We prove that in order to answer this question, sufficient information can be extracted from semigroups recognizing the input languages, using a fixpoint computation, similar to that originally proposed by Henckell. Given as input a morphism recognizing both languages to be separated, this yields an Exptime algorithm for checking firstorder separability. Moreover, the correctness proof of this algorithm yields a stronger result, namely a description of a possible separator. More precisely, one can compute a bound on the quantifier rank of potential separators, as well as a firstorder formula that describes a separator, if there exists one. Finally, we prove that this technique can be generalized to answer the same question for regular languages of infinite words.} }
 J. Almeida, J. C. Costa, M. Zeitoun, Factoriality and the PinReutenauer Procedure. Discrete Mathematics & Theoretical Computer Science 18 (3), pp. 123, 2016. pdf abstract We consider implicit signatures over finite semigroups determined by sets of pseudonatural numbers. We prove that, under relatively simple hypotheses on a pseudovariety V of semigroups, the finitely generated free algebra for the largest such signature is closed under taking factors within the free proV semigroup on the same set of generators. Furthermore, we show that the natural analogue of the PinReutenauer descriptive procedure for the closure of a rational language in the free group with respect to the profinite topology holds for the pseudovariety of all finite semigroups. As an application, we establish that a pseudovariety enjoys this property if and only if it is full. bibtex
@article{factoriality:acz:2016, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {{Factoriality and the PinReutenauer Procedure}}, journal = {Discrete Mathematics & Theoretical Computer Science}, year = 2016, volume = 18, number = 3, pages = {123}, url = {http://dmtcs.episciences.org/1412/pdf}, abstract = "We consider implicit signatures over finite semigroups determined by sets of pseudonatural numbers. We prove that, under relatively simple hypotheses on a pseudovariety V of semigroups, the finitely generated free algebra for the largest such signature is closed under taking factors within the free proV semigroup on the same set of generators. Furthermore, we show that the natural analogue of the PinReutenauer descriptive procedure for the closure of a rational language in the free group with respect to the profinite topology holds for the pseudovariety of all finite semigroups. As an application, we establish that a pseudovariety enjoys this property if and only if it is full.", note = {To appear} }
2015
 T. Place, M. Zeitoun, The Tale of the Quantifier Alternation Hierarchy of FirstOrder Logic over Words. SIGLOG news 2 (3), pp. 417, ACM. July 2015. pdf abstract In this survey, we present ideas developed until recently in order to understand the expressive power of logical fragments in the quantifier alternation hierarchy of firstorder logic interpreted on finite words. bibtex
@article{PZ:Siglog15, author = {T. Place and M. Zeitoun}, title = {The Tale of the Quantifier Alternation Hierarchy of FirstOrder Logic over Words}, journal = {SIGLOG news}, year = 2015, volume = 2, number = 3, pages = {417}, month = {July}, publisher = {{ACM}}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/QaltSiglog15.pdf}, abstract = {In this survey, we present ideas developed until recently in order to understand the expressive power of logical fragments in the quantifier alternation hierarchy of firstorder logic interpreted on finite words.} }
 J. Almeida, J. C. Costa, M. Zeitoun, McCammondâs normal forms for free aperiodic semigroups revisited. LMS Journal of Computation and Mathematics 18 (1), pp. 130â147, Cambridge University Press. 2015. doi pdf abstract This paper revisits the solution of the word problem for Ïterms interpreted over finite aperiodic semigroups, obtained by J. McCammond. The original proof of correctness of McCammondâs algorithm, based on normal forms for such terms, uses McCammondâs solution of the word problem for certain Burnside semigroups. In this paper, we establish a new, simpler, correctness proof of McCammondâs algorithm, based on properties of certain regular languages associated with the normal forms. This method leads to new applications. bibtex
@article{ACZ14:McCammonNF, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {{McCammondâs normal forms for free aperiodic semigroups revisited}}, journal = {LMS Journal of Computation and Mathematics}, year = 2015, volume = 18, number = 1, pages = {130147}, doi = {10.1112/S1461157014000448}, publisher = {Cambridge University Press}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/ACZMcCammondNF.pdf}, abstract = {This paper revisits the solution of the word problem for Ïterms interpreted over finite aperiodic semigroups, obtained by J. McCammond. The original proof of correctness of McCammondâs algorithm, based on normal forms for such terms, uses McCammondâs solution of the word problem for certain Burnside semigroups. In this paper, we establish a new, simpler, correctness proof of McCammondâs algorithm, based on properties of certain regular languages associated with the normal forms. This method leads to new applications.}}
2014
 J. Almeida, J. C. Costa, M. Zeitoun, Iterated Periodicity over Finite Aperiodic Semigroups. European J. Combinatorics 37, pp. 115149, 2014. doi pdf abstract This paper provides a characterization of pseudowords over the pseudovariety of all finite aperiodic semigroups that can be described from the free generators using only the operations of multiplication and Ïpower. A necessary and sufficient condition for this property to hold turns out to be given by the conjunction of two rather simple finiteness conditions: the nonexistence of infinite antichains of factors and the rationality of the language of McCammond normal forms of Ïterms that define factors of the given pseudoword. The relationship between pseudowords with this property and arbitrary pseudowords is also investigated. bibtex
@article{ACZ:Iterated:14, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {Iterated Periodicity over Finite Aperiodic Semigroups}, journal = {European J. Combinatorics}, volume = {37}, pages = {115149}, year = {2014}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaCostaZeitounAkterms.pdf}, doi = {10.1016/j.ejc.2013.07.011}, abstract = {This paper provides a characterization of pseudowords over the pseudovariety of all finite aperiodic semigroups that can be described from the free generators using only the operations of multiplication and Ïpower. A necessary and sufficient condition for this property to hold turns out to be given by the conjunction of two rather simple finiteness conditions: the nonexistence of infinite antichains of factors and the rationality of the language of McCammond normal forms of Ïterms that define factors of the given pseudoword. The relationship between pseudowords with this property and arbitrary pseudowords is also investigated.}, }
 J. Almeida, J. C. Costa, M. Zeitoun, Closures of Regular Languages for Profinite Topologies. Semigroup Forum 89 (1), pp. 20â40, 2014. doi pdf abstract The PinReutenauer algorithm gives a method, that can be viewed as a descriptive procedure, to compute the closure in the free group of a regular language with respect to the Hall topology. A similar descriptive procedure is shown to hold for the pseudovariety A of aperiodic semigroups, where the closure is taken in the free aperiodic Ïsemigroup. It is inherited by a subpseudovariety of a given pseudovariety if both of them enjoy the property of being full. The pseudovariety A, as well as some of its subpseudovarieties are shown to be full. The interest in such descriptions stems from the fact that, for each of the main pseudovarieties V in our examples, the closures of two regular languages are disjoint if and only if the languages can be separated by a language whose syntactic semigroup lies in V. In the cases of A and of the pseudovariety DA of semigroups in which all regular elements are idempotents, this is a new result. bibtex
@article{ACZ:Closures:14, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {Closures of Regular Languages for Profinite Topologies}, journal = {Semigroup Forum}, year = {2014}, volume = 89, number = 1, pages = {2040}, doi = {10.1007/s0023301495743}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaCostaZeitounxi2013.pdf}, abstract = {The PinReutenauer algorithm gives a method, that can be viewed as a descriptive procedure, to compute the closure in the free group of a regular language with respect to the Hall topology. A similar descriptive procedure is shown to hold for the pseudovariety A of aperiodic semigroups, where the closure is taken in the free aperiodic Ïsemigroup. It is inherited by a subpseudovariety of a given pseudovariety if both of them enjoy the property of being full. The pseudovariety A, as well as some of its subpseudovarieties are shown to be full. The interest in such descriptions stems from the fact that, for each of the main pseudovarieties V in our examples, the closures of two regular languages are disjoint if and only if the languages can be separated by a language whose syntactic semigroup lies in V. In the cases of A and of the pseudovariety DA of semigroups in which all regular elements are idempotents, this is a new result.} }
 B. Bollig, A. Cyriac, P. Gastin, M. Zeitoun, Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking. Journal of Applied Logic 12 (4), pp. 395â416, 2014. doi pdf abstract We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic secondorder logic and that, in addition, allows PDLlike path expressions. This captures, in a unifying framework, a wide range of logics defined for ranked and unranked trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satifiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities. bibtex
@article{BCGZ:TempLogConcRecurs:14, author = {Bollig, B. and Cyriac, A. and Gastin, P. and Zeitoun, M.}, title = {Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking}, journal = {Journal of Applied Logic}, volume = 12, number = 4, pages = 395â416, year = {2014}, doi = {10.1016/j.jal.2014.05.001}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/BCGZjal14.pdf}, abstract = {We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic secondorder logic and that, in addition, allows PDLlike path expressions. This captures, in a unifying framework, a wide range of logics defined for ranked and unranked trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satifiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities.} }
 B. Bollig, P. Gastin, B. Monmege, M. Zeitoun, Pebble Weighted Automata and Weighted Logics. ACM Transactions on Computational Logic 15 (2), pp. 19:1â19:10, 2014. doi pdf abstract We introduce new classes of weighted automata on words. Equipped with pebbles, they go beyond the class of recognizable formal power series: they capture weighted firstorder logic enriched with a quantitative version of transitive closure. In contrast to previous work, this calculus allows for unrestricted use of existential and universal quantifications over positions of the input word. We actually consider both twoway and oneway pebble weighted automata. The latter class constrains the head of the automaton to walk lefttoright, resetting it each time a pebble is dropped. Such automata have already been considered in the Boolean setting, in the context of data words. Our main result states that twoway pebble weighted automata, oneway pebble weighted automata, and our weighted logic are expressively equivalent. We also give new logical characterizations of standard recognizable series. bibtex
@article{BGMZ:PebbleWeighted:14, author = {B. Bollig and P. Gastin and B. Monmege and M. Zeitoun}, title = {Pebble Weighted Automata and Weighted Logics}, journal = {{ACM Transactions on Computational Logic}}, volume = 15, number = 2, year = {2014}, pages = {19:119:10}, doi = {10.1145/2579819}, url = {http://tocl.acm.org/accepted/bolliggastin_pebble.pdf}, abstract = {We introduce new classes of weighted automata on words. Equipped with pebbles, they go beyond the class of recognizable formal power series: they capture weighted firstorder logic enriched with a quantitative version of transitive closure. In contrast to previous work, this calculus allows for unrestricted use of existential and universal quantifications over positions of the input word. We actually consider both twoway and oneway pebble weighted automata. The latter class constrains the head of the automaton to walk lefttoright, resetting it each time a pebble is dropped. Such automata have already been considered in the Boolean setting, in the context of data words. Our main result states that twoway pebble weighted automata, oneway pebble weighted automata, and our weighted logic are expressively equivalent. We also give new logical characterizations of standard recognizable series.}, }
 T. Place, L. van Rooijen, M. Zeitoun, On Separation by Locally Testable and Locally Threshold Testable Languages. Logical Methods in Computer Science 10 (3:24), pp. 1â28, 2014. doi pdf abstract A separator for two languages is a third language containing the first one and disjoint from the second one. We investigate the following decision problem: given two regular input languages, decide whether there exists a locally testable (resp. a locally threshold testable) separator. In both cases, we design a decision procedure based on the occurrence of special patterns in automata accepting the input languages. We prove that the problem is computationally harder than deciding membership. The correctness proof of the algorithm yields a stronger result, namely a description of a possible separator. Finally, we discuss the same problem for contextfree input languages. bibtex
@article{PvRZ:LTT:14, author = {T. Place and L. van Rooijen and M. Zeitoun}, title = {On Separation by Locally Testable and Locally Threshold Testable Languages}, journal = {Logical Methods in Computer Science}, year = {2014}, volume = 10, number = "3:24", pages = "128", url = {http://arxiv.org/pdf/1308.0181}, doi = {10.2168/LMCS10(3:24)2014}, abstract = {A separator for two languages is a third language containing the first one and disjoint from the second one. We investigate the following decision problem: given two regular input languages, decide whether there exists a locally testable (resp. a locally threshold testable) separator. In both cases, we design a decision procedure based on the occurrence of special patterns in automata accepting the input languages. We prove that the problem is computationally harder than deciding membership. The correctness proof of the algorithm yields a stronger result, namely a description of a possible separator. Finally, we discuss the same problem for contextfree input languages.} }
2012
 R. Bonnet, A. Finkel, J. Leroux, M. Zeitoun, Model Checking Vector Addition Systems with one zerotest. Logical Methods in Computer Science 8 (2:11), pp. 1â25, 2012. doi pdf abstract We design a variation of the KarpMiller algorithm to compute, in a forward manner, a finite representation of the cover (i.e., the downward closure of the reachability set) of a vector addition system with one zerotest. This algorithm yields decision procedures for several problems for these systems, open until now, such as placeboundedness or LTL modelchecking. The proof techniques to handle the zerotest are based on two new notions of cover: the refined and the filtered cover. The refined cover is a hybrid between the reachability set and the classical cover. It inherits properties of the reachability set: equality of two refined covers is undecidable, even for usual Vector Addition Systems (with no zerotest), but the refined cover of a Vector Addition System is a recursive set. The second notion of cover, called the filtered cover, is the central tool of our algorithms. It inherits properties of the classical cover, and in particular, one can effectively compute a finite representation of this set, even for Vector Addition Systems with one zerotest. bibtex
@article{Bonnet&Finkel&Leroux&Zeitoun:2012, author = {R. Bonnet and A. Finkel and J. Leroux and M. Zeitoun}, title = {Model Checking Vector Addition Systems with one zerotest}, journal = {Logical Methods in Computer Science}, year = 2012, volume = 8, number = {2:11}, pages = {125}, doi = {10.2168/LMCS8(2:11)2012}, url = {http://arxiv.org/pdf/1205.4458}, abstract = {We design a variation of the KarpMiller algorithm to compute, in a forward manner, a finite representation of the cover (i.e., the downward closure of the reachability set) of a vector addition system with one zerotest. This algorithm yields decision procedures for several problems for these systems, open until now, such as placeboundedness or LTL modelchecking. The proof techniques to handle the zerotest are based on two new notions of cover: the refined and the filtered cover. The refined cover is a hybrid between the reachability set and the classical cover. It inherits properties of the reachability set: equality of two refined covers is undecidable, even for usual Vector Addition Systems (with no zerotest), but the refined cover of a Vector Addition System is a recursive set. The second notion of cover, called the filtered cover, is the central tool of our algorithms. It inherits properties of the classical cover, and in particular, one can effectively compute a finite representation of this set, even for Vector Addition Systems with one zerotest.}, }
2009
 P. Gastin, N. Sznajder, M. Zeitoun, Distributed synthesis for wellconnected architectures. Formal Methods in System Design 34 (3), pp. 215â239, 2009. doi pdf abstract We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures with arbitrary delays on processes. External means that the specification only relates input and output variables. We introduce the subclass of uniformly wellconnected (UWC) architectures for which there exists a routing allowing each output process to get the values of all inputs it is connected to, as soon as possible. We prove that the distributed synthesis problem is decidable on UWC architectures if and only if the output variables are totally ordered by their knowledge of input variables. We also show that if we extend this class by letting the routing depend on the output process, then the previous decidability result fails. Finally, we provide a natural restriction on specifications under which the whole class of UWC architectures is decidable. bibtex
@article{Gastin&Sznajder&Zeitoun:2009, author = {P. Gastin and N. Sznajder and M. Zeitoun}, title = {Distributed synthesis for wellconnected architectures}, journal = {Formal Methods in System Design}, year = {2009}, volume = {34}, number = {3}, pages = {215239}, doi = {10.1007/s1070300800647}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/DistSynthGSZ08.pdf}, abstract = {We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures with arbitrary delays on processes. External means that the specification only relates input and output variables. We introduce the subclass of uniformly wellconnected (UWC) architectures for which there exists a routing allowing each output process to get the values of all inputs it is connected to, as soon as possible. We prove that the distributed synthesis problem is decidable on UWC architectures if and only if the output variables are totally ordered by their knowledge of input variables. We also show that if we extend this class by letting the routing depend on the output process, then the previous decidability result fails. Finally, we provide a natural restriction on specifications under which the whole class of UWC architectures is decidable.}, }
2008
 J. Almeida, J. C. Costa, M. Zeitoun, Pointlike sets with respect to R and J. J. Pure Applied Algebra 212 (3), pp. 486â499, Elsevier. 2008. doi pdf abstract We present an algorithm to compute the pointlike subsets of a finite semigroup with respect to the pseudovariety R of all finite Rtrivial semigroups. The algorithm is inspired by Henckellâs algorithm for computing the pointlike subsets with respect to the pseudovariety of all finite aperiodic semigroups. We also give an algorithm to compute Jpointlike sets, where J denotes the pseudovariety of all finite Jtrivial semigroups. We finally show that, in contrast with the situation for R, the natural adaptation of Henckellâs algorithm to J computes pointlike sets, but not all of them. bibtex
@Article{Almeida&Costa&Zeitoun:2008:ComputaPointlikeR, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {Pointlike sets with respect to R and J}, journal = {J. Pure Applied Algebra}, publisher = {Elsevier}, year = 2008, volume = 212, number = 3, pages = {486499}, doi = {10.1016/j.jpaa.2007.06.007}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaCostaZeitounJPAA08.pdf}, abstract = {We present an algorithm to compute the pointlike subsets of a finite semigroup with respect to the pseudovariety R of all finite Rtrivial semigroups. The algorithm is inspired by Henckellâs algorithm for computing the pointlike subsets with respect to the pseudovariety of all finite aperiodic semigroups. We also give an algorithm to compute Jpointlike sets, where J denotes the pseudovariety of all finite Jtrivial semigroups. We finally show that, in contrast with the situation for R, the natural adaptation of Henckellâs algorithm to J computes pointlike sets, but not all of them.} }
 J. Almeida, M. Zeitoun, Description and analysis of a bottomup DFA minimization algorithm. Information Processing Letters 107 (2), pp. 52â59, Elsevier. 2008. doi pdf abstract We establish lineartime reductions between the minimization of a deterministic finite automaton (DFA) and the conjunction of 3 subproblems: the minimization of a strongly connected DFA, the isomorphism problem for a set of strongly connected minimized DFAs, and the minimization of a connected DFA consisting in two strongly connected components, both of which are minimized. We apply this procedure to minimize, in linear time, automata whose nontrivial strongly connected components are cycles. bibtex
@Article{Almeida&Zeitoun:2008:BottomUpMinimization, author = {J. Almeida and M. Zeitoun}, title = {Description and analysis of a bottomup DFA minimization algorithm}, journal = {Information Processing Letters}, year = {2008}, publisher = {Elsevier}, volume = {107}, number = {2}, pages = {5259}, doi = {10.1016/j.ipl.2008.01.003}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaZeitounIPL2008.pdf}, abstract = {We establish lineartime reductions between the minimization of a deterministic finite automaton (DFA) and the conjunction of 3 subproblems: the minimization of a strongly connected DFA, the isomorphism problem for a set of strongly connected minimized DFAs, and the minimization of a connected DFA consisting in two strongly connected components, both of which are minimized. We apply this procedure to minimize, in linear time, automata whose nontrivial strongly connected components are cycles.} }
2007
 J. Almeida, M. Zeitoun, An automatatheoretic approach to the word problem for â”terms over R. Theoret. Comput. Sci. 370 (1â3), pp. 131â169, Elsevier. 2007. doi pdf abstract This paper studies the pseudovariety R of all finite Rtrivial semigroups. We give a representation of pseudowords over R by infinite trees, called Rtrees. Then we show that a pseudoword is an Ïterm if and only if its associated tree is regular (i.e., it can be folded into a finite graph), or equivalently, if the Ïterm has a finite number of tails. We give a linear algorithm to compute a compact representation of the Rtree for Ïterms, which yields a linear solution of the word problem for Ïterms over R. We finally exhibit a basis for the Ïvariety generated by R and we show that there is no finite basis. Several results can be compared to recent work of Bloom and Choffrut on long words. bibtex
@article{AZ:AutomTheorApproac:2007, author = {J. Almeida and M. Zeitoun}, title = {An automatatheoretic approach to the word problem for â”terms over R}, journal = {Theoret. Comput. Sci.}, pages = {131169}, volume = 370, number = {13}, publisher = {Elsevier}, doi = {10.1016/j.tcs.2006.10.019}, year = {2007}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaZeitounTCS2007.pdf}, abstract = {This paper studies the pseudovariety R of all finite Rtrivial semigroups. We give a representation of pseudowords over R by infinite trees, called Rtrees. Then we show that a pseudoword is an Ïterm if and only if its associated tree is regular (i.e., it can be folded into a finite graph), or equivalently, if the Ïterm has a finite number of tails. We give a linear algorithm to compute a compact representation of the Rtree for Ïterms, which yields a linear solution of the word problem for Ïterms over R. We finally exhibit a basis for the Ïvariety generated by R and we show that there is no finite basis. Several results can be compared to recent work of Bloom and Choffrut on long words.}, }
 J. Almeida, J. C. Costa, M. Zeitoun, Complete reducibility of systems of equations with respect to R. Portugaliae MatemĂĄtica 64 (4), pp. 445â508, Sociedade Portuguesa de Matematica. 2007. doi pdf abstract It is shown that the pseudovariety R of all finite Rtrivial semigroups is completely reducible with respect to the canonical signature. Informally, if the variables in a finite system of equations with rational constraints may be evaluated by pseudowords so that each value belongs to the closure of the corresponding rational constraint and the system is verified in R, then there is some such evaluation which is âregularâ, that is one in which, additionally, the pseudowords only involve multiplications and Ïpowers. bibtex
@Article{Almeida&Costa&Zeitoun:2007:CompleteReducibilityR, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {Complete reducibility of systems of equations with respect to R}, journal = {Portugaliae MatemĂĄtica}, publisher = {Sociedade Portuguesa de Matematica}, year = 2007, note = {Special issue}, volume = 64, number = 4, pages = {445508}, doi = {10.4171/PM/1792}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaCostaZeitounPortMath2007.pdf}, abstract = {It is shown that the pseudovariety R of all finite Rtrivial semigroups is completely reducible with respect to the canonical signature. Informally, if the variables in a finite system of equations with rational constraints may be evaluated by pseudowords so that each value belongs to the closure of the corresponding rational constraint and the system is verified in R, then there is some such evaluation which is âregularâ, that is one in which, additionally, the pseudowords only involve multiplications and Ïpowers.}, }
2006
 Blaise Genest, Anca Muscholl, Helmut Seidl, M. Zeitoun, Infinitestate High level MSCs: realizability and modelchecking. Journal of Computer and System Sciences 72 (4), pp. 617â647, Elsevier. 2006. doi pdf abstract Message sequence charts (MSC) and HighLevel MSC (HMSC) is a visual notation for asynchronously communicating processes and a standard of the ITU. They usually represent incomplete specifications of required or forbidden properties of communication protocols. We consider in this paper two basic problems concerning the automated validation of HMSC sp ecifications, namely modelchecking and synthesis. We identify natural syntactic restrictions of HMSCs for which we can solve the above questions. We show first that modelchecking for globallycooperative (and locallycooperative) HMSCs is decidable within the same complexity as for the restricted class of bounded HMSCs. Furthermore, modelchecking localchoice HMSCs turns out to be as efficient as for finitestate (sequential) systems. The study of locallycooperative and localchoice HMSCs is motivated by the synthesis question, i.e., the question of implementing HMSCs through communicating finitestate machines (CFM) with additional message data. We show that locallycooperative and localchoice HMSCs are always implementable. Furthermore, the implementation of a localchoice HMSC is deadlockfree and of linear size. bibtex
@Article{genest&muscholl&seidl&zeitoun:2006:jcss, author = {Blaise Genest and Anca Muscholl and Helmut Seidl and M. Zeitoun}, title = {Infinitestate High level MSCs: realizability and modelchecking}, journal = {Journal of Computer and System Sciences}, year = 2006, publisher = {Elsevier}, doi = {10.1016/j.jcss.2005.09.007}, volume = 72, number = 4, pages = {617647}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/InfStateHMSC.pdf}, abstract = {Message sequence charts (MSC) and HighLevel MSC (HMSC) is a visual notation for asynchronously communicating processes and a standard of the ITU. They usually represent incomplete specifications of required or forbidden properties of communication protocols. We consider in this paper two basic problems concerning the automated validation of HMSC sp ecifications, namely modelchecking and synthesis. We identify natural syntactic restrictions of HMSCs for which we can solve the above questions. We show first that modelchecking for globallycooperative (and locallycooperative) HMSCs is decidable within the same complexity as for the restricted class of bounded HMSCs. Furthermore, modelchecking localchoice HMSCs turns out to be as efficient as for finitestate (sequential) systems. The study of locallycooperative and localchoice HMSCs is motivated by the synthesis question, i.e., the question of implementing HMSCs through communicating finitestate machines (CFM) with additional message data. We show that locallycooperative and localchoice HMSCs are always implementable. Furthermore, the implementation of a localchoice HMSC is deadlockfree and of linear size.} }
2005
 J. Almeida, J. C. Costa, M. Zeitoun, Tameness of pseudovariety joins involving R. Monatshefte fĂŒr Mathematik 146 (2), pp. 89â111, 2005. doi pdf abstract In this paper, we establish several decidability results for pseudovariety joins of the form V âš W, where V is a subpseudovariety of J or the pseudovariety R. Here, J (resp. R) denotes the pseudovariety of all Jtrivial (resp. Rtrivial) semigroups. In particular, we show that the pseudovariety V âš W is (completely) Îștame when V is a subpseudovariety of J with decidable Îșword problem and W is (completely) Îștame. Moreover, if W is a Îștame pseudovariety which satisfies the pseudoidentity x1 Â·Â·Â·xry^(Ï+1)zt^Ï = x1 Â·Â·Â·xryzt^Ï, then we prove that R âš W is also Îștame. In particular the joins RâšAb, RâšG, RâšOCR, and RâšCR are decidable. bibtex
@Article{almeida&costa&zeitoun:2005:monatshefte, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {Tameness of pseudovariety joins involving R}, journal = {Monatshefte fĂŒr Mathematik}, volume = 146, number = 2, pages = {89111}, doi = {10.1007/s0060500503241}, year = 2005, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaCostaZeitounMonatsHefte05.pdf}, abstract = {In this paper, we establish several decidability results for pseudovariety joins of the form V âš W, where V is a subpseudovariety of J or the pseudovariety R. Here, J (resp. R) denotes the pseudovariety of all Jtrivial (resp. Rtrivial) semigroups. In particular, we show that the pseudovariety V âš W is (completely) Îștame when V is a subpseudovariety of J with decidable Îșword problem and W is (completely) Îștame. Moreover, if W is a Îștame pseudovariety which satisfies the pseudoidentity x1 Â·Â·Â·xry^(Ï+1)zt^Ï = x1 Â·Â·Â·xryzt^Ï, then we prove that R âš W is also Îștame. In particular the joins RâšAb, RâšG, RâšOCR, and RâšCR are decidable.} }
2003
 J. Almeida, M. Zeitoun, Tameness of some locally trivial pseudovarieties. Comm. Algebra 31 (1), pp. 61â77, 2003. doi pdf abstract Tameness is a strong property of semigroup pseudovarieties related to the membership problem. Let Îș be the signature comprising semigroup multiplication and the omega implicit operation. We prove the Îștameness of the pseudovarieties N, D, K and LI. bibtex
@Article{almeida&zeitoun:2003:commalg, author = {J. Almeida and M. Zeitoun}, title = {Tameness of some locally trivial pseudovarieties}, journal = {Comm. Algebra}, year = 2003, volume = 31, number = 1, pages = {6177}, doi = {10.1081/AGB120016749}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaZeitounCommAlgebra2003.pdf}, abstract = {Tameness is a strong property of semigroup pseudovarieties related to the membership problem. Let Îș be the signature comprising semigroup multiplication and the omega implicit operation. We prove the Îștameness of the pseudovarieties N, D, K and LI.} }
1999
 J. Almeida, Assis Azevedo, M. Zeitoun, Pseudovariety joins involving Jtrivial semigroups and completely regular semigroups. Internat. J. Algebra Comput. 9 (1), pp. 99â112, 1999. doi pdf abstract J. Rhodes asked during the Chico conference in 1986 for the calculation of joins of semigroup pseudovarieties. This paper proves that the join JâšV of the pseudovariety J of J trivial semigroups and of any 2strongly decidable pseudovariety V of completely regular semigroups is decidable. This problem was proposed by the first author for V = G, the pseudovariety of finite groups. bibtex
@Article{almeida&azevedo&zeitoun:1999:ijac, author = {J. Almeida and Assis Azevedo and M. Zeitoun}, title = {{Pseudovariety joins involving Jtrivial semigroups and completely regular semigroups}}, journal = {Internat. J. Algebra Comput.}, year = 1999, volume = 9, number = 1, pages = {99112}, doi = {10.1142/S0218196799000072}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/JvG.pdf}, abstract = {J. Rhodes asked during the Chico conference in 1986 for the calculation of joins of semigroup pseudovarieties. This paper proves that the join JâšV of the pseudovariety J of J trivial semigroups and of any 2strongly decidable pseudovariety V of completely regular semigroups is decidable. This problem was proposed by the first author for V = G, the pseudovariety of finite groups.}, }
1998
 Assis Azevedo, M. Zeitoun, Three examples of join computations. Semigroup Forum 57 (2), pp. 249â277, 1998. doi pdf abstract This article answers three questions of J. Almeida. Using combinatorial, algebraic and topological methods, we compute joins involving the pseudovariety of finite groups, the pseudovariety of semigroups in which each idempotent is a right zero and the pseudovariety generated by monoids M such that each idempotent of M{1} is a left zero. bibtex
@Article{azevedo&zeitoun:1998:sgf, author = {Assis Azevedo and M. Zeitoun}, title = {Three examples of join computations}, journal = {Semigroup Forum}, year = 1998, volume = 57, number = 2, pages = {249277}, doi = {10.1007/PL00005976}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/MKvDvG.pdf}, abstract = {This article answers three questions of J. Almeida. Using combinatorial, algebraic and topological methods, we compute joins involving the pseudovariety of finite groups, the pseudovariety of semigroups in which each idempotent is a right zero and the pseudovariety generated by monoids M such that each idempotent of M{1} is a left zero.}, }
1997
 M. Zeitoun, On embeddings of finitely generated profinite semigroups into 2generated profinite semigroups. Algebra Universalis 38 (2), pp. 210â213, 1997. doi pdf abstract Koryakov recently asked the following question: when a pseudovariety V does not satisfy any nontrivial identity, does there exist an embedding from any finitely generated Vfree profinite semigroup into the 2generated Vfree profinite semigroup? During the conference âSemigroups, Automata and Languagesâ in Porto (June 1994), a positive answer to this question was conjectured. We give here a counterexample to this conjecture. bibtex
@Article{zeitoun:1997:au, author = {M. Zeitoun}, title = {On embeddings of finitely generated profinite semigroups into 2generated profinite semigroups}, journal = {Algebra Universalis}, year = 1997, volume = 38, number = 2, pages = {210213}, doi = {10.1007/s000120050049}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/Embedding.pdf}, abstract = {Koryakov recently asked the following question: when a pseudovariety V does not satisfy any nontrivial identity, does there exist an embedding from any finitely generated Vfree profinite semigroup into the 2generated Vfree profinite semigroup? During the conference âSemigroups, Automata and Languagesâ in Porto (June 1994), a positive answer to this question was conjectured. We give here a counterexample to this conjecture.} }
 J. Almeida, M. Zeitoun, The pseudovariety J is hyperdecidable. RAIRO Inform. ThĂ©or. Appl. 31 (5), pp. 457â482, EDP Sciences. 1997. pdf abstract This article defines the notion of hyperdecidability for a class of finite semigroups, which is closely connected to the notion of decidability. It then proves that the pseudovariety J of Jtrivial semigroups is hyperdecidable. bibtex
@Article{almeida&zeitoun:1997:rairo, author = {J. Almeida and M. Zeitoun}, title = {{The pseudovariety J is hyperdecidable}}, year = 1997, volume = 31, number = 5, pages = {457482}, journal = {{RAIRO Inform. ThĂ©or. Appl.}}, publisher = {EDP Sciences}, url = {http://archive.numdam.org/article/ITA_1997__31_5_457_0.pdf}, abstract = {This article defines the notion of hyperdecidability for a class of finite semigroups, which is closely connected to the notion of decidability. It then proves that the pseudovariety J of Jtrivial semigroups is hyperdecidable.}, }
1995
 M. Zeitoun, The join of the pseudovarieties of idempotent semigroups and locally trivial semigroups. Semigroup Forum 50, pp. 367â381, 1995. doi pdf abstract This article solves a problem proposed by Almeida: the computation of the join of two wellknown pseudovarieties of semigroups, namely the pseudovariety of bands and the pseudovariety of locally trivial semigroups. We use a method developed by Almeida, based on the theory of implicit operations. bibtex
@Article{zeitoun:1995:sgf, author = {M. Zeitoun}, title = {The join of the pseudovarieties of idempotent semigroups and locally trivial semigroups}, journal = {Semigroup Forum}, year = 1995, volume = 50, pages = {367381}, doi = {10.1007/BF02573532}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/LIvB.pdf}, abstract = {This article solves a problem proposed by Almeida: the computation of the join of two wellknown pseudovarieties of semigroups, namely the pseudovariety of bands and the pseudovariety of locally trivial semigroups. We use a method developed by Almeida, based on the theory of implicit operations.}, }
1994
 M. Zeitoun, On the decidability of the membership problem of the pseudovariety JvB. Internat. J. Algebra Comput. 4 (4), pp. 47â64, 1994. doi pdf abstract The aim of this article is to prove that the pseudovariety generated by JâȘB, that is to say, the join of the pseudovariety of Jtrivial semigroups and of the pseudovariety of idempotents semigroups, is decidable. The techniques used were developed by Almeida and are based on the study of the topological semigroup of implicit operations. bibtex
@Article{zeitoun:1994:ijac, author = {M. Zeitoun}, title = {{On the decidability of the membership problem of the pseudovariety JvB}}, journal = {Internat. J. Algebra Comput.}, year = 1994, volume = 4, number = 4, pages = {4764}, doi = {10.1142/S0218196795000057}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/JvBd.pdf}, abstract = {The aim of this article is to prove that the pseudovariety generated by JâȘB, that is to say, the join of the pseudovariety of Jtrivial semigroups and of the pseudovariety of idempotents semigroups, is decidable. The techniques used were developed by Almeida and are based on the study of the topological semigroup of implicit operations.}, }
 Only Conference proceedings
2016
 T. Pierron, T. Place, M. Zeitoun, Quantifier Alternation for Infinite Words. In 19th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS'16, Springer. 2016. doi pdf abstract We investigate the expressive power of the quantifier alternation hierarchy of firstorder logic over words. This hierarchy includes the classes ÎŁi (sentences having at most i blocks of quantifiers starting with an â) and BÎŁi (Boolean combinations of ÎŁi sentences). So far, this expressive power has been effectively characterized for the lower levels only. Recently, a breakthrough was made over finite words, and decidable characterizations were obtained for BÎŁ2 and ÎŁ3, by relying on a decision problem called separation, and solving it for ÎŁ2. The contribution of this paper is a generalization of these results to the setting of infinite words: we solve separation for ÎŁ2 and ÎŁ3, and obtain decidable characterizations of BÎŁ2 and ÎŁ3 as consequences. bibtex
@inproceedings{ppzinf16, author = {T. Pierron and T. Place and M. Zeitoun}, title = {Quantifier Alternation for Infinite Words}, booktitle = {19th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS'16}, year = 2016, editor = {B. Jacobs and C. LĂ¶ding}, series = {Lect. Notes Comp. Sci.}, volume = 9634, publisher = {Springer}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/PPZFOSSACS16.pdf}, doi = {10.1007/9783662496305_14}, abstract = {We investigate the expressive power of the quantifier alternation hierarchy of firstorder logic over words. This hierarchy includes the classes ÎŁi (sentences having at most i blocks of quantifiers starting with an â) and BÎŁi (Boolean combinations of ÎŁi sentences). So far, this expressive power has been effectively characterized for the lower levels only. Recently, a breakthrough was made over finite words, and decidable characterizations were obtained for BÎŁ2 and ÎŁ3, by relying on a decision problem called separation, and solving it for ÎŁ2. The contribution of this paper is a generalization of these results to the setting of infinite words: we solve separation for ÎŁ2 and ÎŁ3, and obtain decidable characterizations of BÎŁ2 and ÎŁ3 as consequences.} }
 T. Place, M. Zeitoun, The Covering Problem: a Unified Approach for Investigating the Expressive Power of Logics. In 41st International Symposium on Mathematical Foundations of Computer Science, MFCS'16, pp. 78:1â78:14, Schloss Dagstuhl  LeibnizZentrum fĂŒr Informatik. 2016. doi pdf abstract An important endeavor in computer science is to precisely understand the expressive power of logical formalisms over discrete structures, such as words. Naturally, âunderstandingâ is not a mathematical notion. Therefore, this investigation requires a concrete objective to capture such a notion. In the literature, the standard choice for this objective is the emph{membership problem}, whose aim is to find a procedure deciding whether an input regular language can be defined in the logic under study. This approach was cemented as the ârightâ one by the seminal work of SchĂŒtzenberger, McNaughton and Papert on firstorder logic and has been in use since then. However, membership questions are hard: for several important fragments, researchers have failed in this endeavor despite decades of investigation. In view of recent results on one of the most famous open questions, namely the quantifier alternation hierarchy of firstorder logic, an explanation may be that membership is too restrictive as a setting. These new results were indeed obtained by considering more general problems than membership, taking advantage of the increased flexibility of the enriched mathematical setting. This opens a promising avenue of research and efforts have been devoted at identifying and solving such problems for natural fragments. However, until now, these problems have been emph{ad hoc}, most fragments relying on a specific one. A unique new problem replacing membership as the right one is still missing. The main contribution of this paper is a suitable candidate to play this role: the Covering Problem. We motivate this problem with three arguments. First, it admits an elementary set theoretic formulation, similar to membership. Second, we are able to reexplain or generalize all known results with this problem. Third, we develop a mathematical framework as well as a methodology tailored to the investigation of this problem. bibtex
@inproceedings{pzcovers:mfcs16, author = {T. Place and M. Zeitoun}, title = {The Covering Problem: a Unified Approach for Investigating the Expressive Power of Logics}, booktitle = {41st International Symposium on Mathematical Foundations of Computer Science, MFCS'16}, year = 2016, editor = {P. Faliszewski and A. Muscholl and R. Niedermeier}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, volume = 58, publisher = {Schloss Dagstuhl  LeibnizZentrum fĂŒr Informatik}, pages = {78:178:14}, doi = {10.4230/LIPIcs.MFCS.2016.78}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/PZMFCS16.pdf}, abstract = {An important endeavor in computer science is to precisely understand the expressive power of logical formalisms over discrete structures, such as words. Naturally, "understanding" is not a mathematical notion. Therefore, this investigation requires a concrete objective to capture such a notion. In the literature, the standard choice for this objective is the emph{membership problem}, whose aim is to find a procedure deciding whether an input regular language can be defined in the logic under study. This approach was cemented as the "right" one by the seminal work of SchĂŒtzenberger, McNaughton and Papert on firstorder logic and has been in use since then. However, membership questions are hard: for several important fragments, researchers have failed in this endeavor despite decades of investigation. In view of recent results on one of the most famous open questions, namely the quantifier alternation hierarchy of firstorder logic, an explanation may be that membership is too restrictive as a setting. These new results were indeed obtained by considering more general problems than membership, taking advantage of the increased flexibility of the enriched mathematical setting. This opens a promising avenue of research and efforts have been devoted at identifying and solving such problems for natural fragments. However, until now, these problems have been emph{ad hoc}, most fragments relying on a specific one. A unique new problem replacing membership as the right one is still missing. The main contribution of this paper is a suitable candidate to play this role: the Covering Problem. We motivate this problem with three arguments. First, it admits an elementary set theoretic formulation, similar to membership. Second, we are able to reexplain or generalize all known results with this problem. Third, we develop a mathematical framework as well as a methodology tailored to the investigation of this problem.} }
2015
 T. Place, M. Zeitoun, Separation and the Successor Relation. In STACS'15, pp. 662â675, Schloss Dagstuhl  LeibnizZentrum fĂŒr Informatik. 2015. doi pdf abstract We investigate two problems for a class C of regular word languages. The Cmembership problem asks for an algorithm to decide whether an input language belongs to C. The Cseparation problem asks for an algorithm that, given as input two regular languages, decides whether there exists a third language in C containing the first language, while being disjoint from the second. These problems are considered as means to obtain a deep understanding of the class C. It is usual for such classes to be defined by logical formalisms. Logics are often built on top of each other, by adding new predicates. A natural construction is to enrich a logic with the successor relation. In this paper, we obtain simple selfcontained proofs of two transfer results: we show that for suitable logically defined classes, the membership, resp. the separation problem for a class enriched with the successor relation reduces to the same problem for the original class. Our reductions work both for languages of finite words and infinite words. The proofs are mostly selfcontained, and only require a basic background on regular languages. This paper therefore gives new, simple proofs of results that were considered as difficult, such as the decidability of the membership problem for the levels 1, 3/2, 2 and 5/2 of the dotdepth hierarchy. bibtex
@inproceedings{PZ:stacs15, author = {T. Place and M. Zeitoun}, title = {Separation and the Successor Relation}, booktitle = {{STACS'15}}, year = {2015}, series = {Lect. Notes Comp. Sci.}, volume = {30}, pages = {662675}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, editor = {Ernst W. Mayr and Nicolas Ollinger}, publisher = {Schloss Dagstuhl  LeibnizZentrum fĂŒr Informatik}, URL = {http://drops.dagstuhl.de/opus/volltexte/2015/4949}, URN = {urn:nbn:de:0030drops49499}, doi = {10.4230/LIPIcs.STACS.2015.662}, abstract = {We investigate two problems for a class C of regular word languages. The Cmembership problem asks for an algorithm to decide whether an input language belongs to C. The Cseparation problem asks for an algorithm that, given as input two regular languages, decides whether there exists a third language in C containing the first language, while being disjoint from the second. These problems are considered as means to obtain a deep understanding of the class C. It is usual for such classes to be defined by logical formalisms. Logics are often built on top of each other, by adding new predicates. A natural construction is to enrich a logic with the successor relation. In this paper, we obtain simple selfcontained proofs of two transfer results: we show that for suitable logically defined classes, the membership, resp. the separation problem for a class enriched with the successor relation reduces to the same problem for the original class. Our reductions work both for languages of finite words and infinite words. The proofs are mostly selfcontained, and only require a basic background on regular languages. This paper therefore gives new, simple proofs of results that were considered as difficult, such as the decidability of the membership problem for the levels 1, 3/2, 2 and 5/2 of the dotdepth hierarchy.} }
 W. Czerwinski, W. Martens, L. van Rooijen, M. Zeitoun, A Note on Decidable Separability by Piecewise Testable Languages. In 20th International Symposium on Fundamentals of Computation Theory, FCT'15, pp. 173185, Springer. 2015. doi pdf abstract The separability problem for languages from a class C by languages of a class S asks, for two given word languages I and E from C, whether there exists a language S from S which includes I and excludes E, that is, I â S and S â© E = â . It is known that separability for contextfree languages by any class containing all definite languages (such as regular languages) is undecidable. We show that separability of contextfree languages by piecewise testable languages is decidable. This contrasts the fact that testing if a contextfree language is piecewise testable is undecidable. We generalize this decidability result by showing that, for every full trio (a class of languages that is closed under rather weak operations) which has decidable diagonal problem, separability with respect to piecewise testable languages is decidable. Examples of such classes are the class of languages defined by labeled vector addition systems and the class of languages accepted by higher order pushdown automata of order two. The proof goes through a result which is of independent interest and shows that, for any kind of languages I and E, separability can be decided by testing the existence of common patterns in I and E. bibtex
@inproceedings{CMvRZ:15, author = {W. Czerwinski and W. Martens and L. van Rooijen and M. Zeitoun}, title = {A Note on Decidable Separability by Piecewise Testable Languages}, booktitle = {20th International Symposium on Fundamentals of Computation Theory, FCT'15}, year = 2015, editor = {A. Kosowski and I. Walukiewicz}, volume = 9210, series = {Lect. Notes Comp. Sci.}, pages = {173185}, publisher = {Springer}, doi = {10.1007/9783319221779}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/PTSepFCT15.pdf}, abstract = {The separability problem for languages from a class C by languages of a class S asks, for two given word languages I and E from C, whether there exists a language S from S which includes I and excludes E, that is, I â S and S â© E = â . It is known that separability for contextfree languages by any class containing all definite languages (such as regular languages) is undecidable. We show that separability of contextfree languages by piecewise testable languages is decidable. This contrasts the fact that testing if a contextfree language is piecewise testable is undecidable. We generalize this decidability result by showing that, for every full trio (a class of languages that is closed under rather weak operations) which has decidable diagonal problem, separability with respect to piecewise testable languages is decidable. Examples of such classes are the class of languages defined by labeled vector addition systems and the class of languages accepted by higher order pushdown automata of order two. The proof goes through a result which is of independent interest and shows that, for any kind of languages I and E, separability can be decided by testing the existence of common patterns in I and E.} }
2014
 T. Place, M. Zeitoun, Separating Regular Languages with FirstOrder Logic. In CSLLICS'14, pp. 75:1â75:10, ACM. 2014. doi pdf abstract Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular input languages of finite words, decide whether there exists a firstorder definable separator. We prove that in order to answer this question, sufficient information can be extracted from semigroups recognizing the input languages, using a fixpoint computation. This yields an EXPTIME algorithm for checking firstorder separability. Moreover, the correctness proof of this algorithm yields a stronger result, namely a description of a possible separator. Finally, we prove that this technique can be generalized to answer the same question for regular languages of infinite words. bibtex
@inproceedings{PZ:lics14, author = {T. Place and M. Zeitoun}, title = {Separating Regular Languages with FirstOrder Logic}, booktitle = {{CSLLICS'14}}, year = {2014}, pages = {75:175:10}, publisher = {ACM}, doi = {10.1145/2603088.2603098}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/PZLICS14.pdf}, abstract = {Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular input languages of finite words, decide whether there exists a firstorder definable separator. We prove that in order to answer this question, sufficient information can be extracted from semigroups recognizing the input languages, using a fixpoint computation. This yields an EXPTIME algorithm for checking firstorder separability. Moreover, the correctness proof of this algorithm yields a stronger result, namely a description of a possible separator. Finally, we prove that this technique can be generalized to answer the same question for regular languages of infinite words.}, }
 B. Bollig, P. Gastin, B. Monmege, M. Zeitoun, Logical Characterization of Weighted Pebble Walking Automata. In CSLLICS'14, pp. 19:1â19:10, ACM. 2014. doi pdf abstract Weighted automata are a conservative quantitative extension of finite automata that enjoys applications, e.g., in language processing and speech recognition. Their expressive power, however, appears to be limited, especially when they are applied to more general structures than words, such as graphs. To address this drawback, weighted automata have recently been generalized to weighted pebble walking automata, which proved useful as a tool for the specification and evaluation of quantitative properties over words and nested words. In this paper, we establish the expressive power of weighted pebble walking automata in terms of transitive closure logic, lifting a similar result by Engelfriet and Hoogeboom from the Boolean case to a quantitative setting. This result applies to a general class of graphs that subsumes all the aforementioned classes. bibtex
@inproceedings{BGMZ:lics14, author = {B. Bollig and P. Gastin and B. Monmege and M. Zeitoun}, title = {Logical Characterization of Weighted Pebble Walking Automata}, booktitle = {{CSLLICS'14}}, year = {2014}, pages = {19:119:10}, publisher = {ACM}, doi = {10.1145/2603088.2603118}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/graphsBGMZlics14.pdf}, abstract = {Weighted automata are a conservative quantitative extension of finite automata that enjoys applications, e.g., in language processing and speech recognition. Their expressive power, however, appears to be limited, especially when they are applied to more general structures than words, such as graphs. To address this drawback, weighted automata have recently been generalized to weighted pebble walking automata, which proved useful as a tool for the specification and evaluation of quantitative properties over words and nested words. In this paper, we establish the expressive power of weighted pebble walking automata in terms of transitive closure logic, lifting a similar result by Engelfriet and Hoogeboom from the Boolean case to a quantitative setting. This result applies to a general class of graphs that subsumes all the aforementioned classes.} }
 T. Place, M. Zeitoun, Going higher in the Firstorder Quantifier Alternation Hierarchy on Words. In ICALP'14, pp. 342â353, Springer. 2014. doi pdf abstract We investigate the quantifier alternation hierarchy in firstorder logic on finite words. Levels in this hierarchy are defined by counting the number of quantifier alternations in formulas. We prove that one can decide membership of a regular language to the levels BÎŁ2 (boolean combination of formulas having only 1 alternation) and ÎŁ3 (formulas having only 2 alternations beginning with an existential block). Our proof works by considering a deeper problem, called separation, which, once solved for lower levels, allows us to solve membership for higher levels. bibtex
@inproceedings{PZ:icalp14, author = {T. Place and M. Zeitoun}, title = {Going higher in the Firstorder Quantifier Alternation Hierarchy on Words}, booktitle = {{ICALP'14}}, year = {2014}, series = {Lect. Notes Comp. Sci.}, volume = 8573, pages = {342353}, editor = {Esparza, J. and Fraigniaud, P. and Husfeldt, T. and Koutsoupias, E.}, publisher = {Springer}, doi = {10.1007/9783662439517_29}, url = {http://arxiv.org/pdf/1404.6832v1}, abstract = {We investigate the quantifier alternation hierarchy in firstorder logic on finite words. Levels in this hierarchy are defined by counting the number of quantifier alternations in formulas. We prove that one can decide membership of a regular language to the levels BÎŁ2 (boolean combination of formulas having only 1 alternation) and ÎŁ3 (formulas having only 2 alternations beginning with an existential block). Our proof works by considering a deeper problem, called separation, which, once solved for lower levels, allows us to solve membership for higher levels.} }
2013
 T. Place, L. van Rooijen, M. Zeitoun, Separating Regular Languages by Locally Testable and Locally Threshold Testable Languages. In FSTTCS'13, pp. 363375, Schloss Dagstuhl  LeibnizZentrum fĂŒr Informatik. 2013. doi pdf abstract A separator for two languages is a third language containing the first one and disjoint from the second one. We investigate the following decision problem: given two regular input languages, decide whether there exists a locally testable (resp. a locally threshold testable) separator. In both cases, we design a decision procedure based on the occurrence of special patterns in automata accepting the input languages. We prove that the problem is computationally harder than deciding membership. The correctness proof of the algorithm yields a stronger result, namely a description of a possible separator. Finally, we discuss the same problem for contextfree input languages. bibtex
@inproceedings{PRZ:fsttcs:13, author = {T. Place and L. van Rooijen and M. Zeitoun}, title = {Separating Regular Languages by Locally Testable and Locally Threshold Testable Languages}, booktitle = {FSTTCS'13}, year = {2013}, volume = {24}, series = {LIPIcs}, publisher = {Schloss Dagstuhl  LeibnizZentrum fĂŒr Informatik}, pages = {363375}, url = {http://drops.dagstuhl.de/opus/volltexte/2013/4386/pdf/27.pdf}, doi = {10.4230/LIPIcs.FSTTCS.2013.363}, abstract = {A separator for two languages is a third language containing the first one and disjoint from the second one. We investigate the following decision problem: given two regular input languages, decide whether there exists a locally testable (resp. a locally threshold testable) separator. In both cases, we design a decision procedure based on the occurrence of special patterns in automata accepting the input languages. We prove that the problem is computationally harder than deciding membership. The correctness proof of the algorithm yields a stronger result, namely a description of a possible separator. Finally, we discuss the same problem for contextfree input languages.} }
 T. Place, L. van Rooijen, M. Zeitoun, Separating Regular Languages by Piecewise Testable and Unambiguous Languages. In MFCS'13, pp. 729740, Springer. 2013. doi pdf abstract Separation is a classical problem asking whether, given two sets belonging to some class, it is possible to separate them by a set from a smaller class. We discuss the separation problem for regular languages. We give a Ptime algorithm to check whether two given regular languages are separable by a piecewise testable language, that is, whether a BÎŁ1(<) sentence can witness that the languages are disjoint. The proof refines an algebraic argument from Almeida and the third author. When separation is possible, we also express a separator by saturating one of the original languages by a suitable congruence. Following the same line, we show that one can as well decide whether two regular languages can be separated by an unambiguous language, albeit with a higher complexity. bibtex
@inproceedings{PRZ:mfcs:13, author = {T. Place and L. van Rooijen and M. Zeitoun}, title = {Separating Regular Languages by Piecewise Testable and Unambiguous Languages}, booktitle = {{MFCS'13}}, year = {2013}, pages = {729740}, series = {Lect. Notes Comp. Sci.}, volume = {8087}, publisher = {Springer}, doi = {10.1007/9783642403132_64}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/mfcs13.pdf}, abstract = {Separation is a classical problem asking whether, given two sets belonging to some class, it is possible to separate them by a set from a smaller class. We discuss the separation problem for regular languages. We give a Ptime algorithm to check whether two given regular languages are separable by a piecewise testable language, that is, whether a BÎŁ1(<) sentence can witness that the languages are disjoint. The proof refines an algebraic argument from Almeida and the third author. When separation is possible, we also express a separator by saturating one of the original languages by a suitable congruence. Following the same line, we show that one can as well decide whether two regular languages can be separated by an unambiguous language, albeit with a higher complexity.} }
2012
 B. Bollig, P. Gastin, B. Monmege, M. Zeitoun, A Probabilistic Kleene Theorem. In ATVA'12, pp. 400â415, Springer. 2012. doi pdf abstract We provide a Kleene Theorem for (Rabin) probabilistic automata over finite words. Probabilistic automata generalize deterministic finite automata and assign to a word an acceptance probability. We provide probabilistic expressions with probabilistic choice, guarded choice, concatenation, and a star operator. We prove that probabilistic expressions and probabilistic automata are expressively equivalent. Our result actually extends to twoway probabilistic automata with pebbles and corresponding expressions. bibtex
@inproceedings{BGMZ:Atva:12, author = {B. Bollig and P. Gastin and B. Monmege and M. Zeitoun}, title = {A Probabilistic Kleene Theorem}, booktitle = {ATVA'12}, volume = 7561, year = 2012, pages = {400415}, editor = {Supratik Chakraborty and Madhavan Mukund}, publisher = {Springer}, series = {Lect. Notes Comp. Sci.}, doi = {10.1007/9783642333866_31}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/BGMZATVA12Probabilistic_Kleene.pdf}, abstract = {We provide a Kleene Theorem for (Rabin) probabilistic automata over finite words. Probabilistic automata generalize deterministic finite automata and assign to a word an acceptance probability. We provide probabilistic expressions with probabilistic choice, guarded choice, concatenation, and a star operator. We prove that probabilistic expressions and probabilistic automata are expressively equivalent. Our result actually extends to twoway probabilistic automata with pebbles and corresponding expressions.}, }
2011
 B. Bollig, A. Cyriac, P. Gastin, M. Zeitoun, Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking. In MFCS'11, pp. 132144, Springer. 2011. doi pdf abstract We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic secondorder logic and that, in addition, allows PDLlike path expressions. This captures, in a unifying framework, a wide range of logics defined for ranked and unranked trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satisfiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities. bibtex
@inproceedings{BCGZ:MFCS:2011, author = {Bollig, B. and Cyriac, A. and Gastin, P. and Zeitoun, M.}, title = {Temporal Logics for Concurrent Recursive Programs: Satisfiability and Model Checking}, booktitle = {{MFCS'11}}, pages = {132144}, year = 2011, volume = 6907, series = {Lect. Notes. Comp Sci.}, publisher = {Springer}, doi = {10.1007/9783642229930_15}, url = {http://hal.archivesouvertes.fr/docs/00/59/11/39/PDF/report.pdf}, abstract = {We develop a general framework for the design of temporal logics for concurrent recursive programs. A program execution is modeled as a partial order with multiple nesting relations. To specify properties of executions, we consider any temporal logic whose modalities are definable in monadic secondorder logic and that, in addition, allows PDLlike path expressions. This captures, in a unifying framework, a wide range of logics defined for ranked and unranked trees, nested words, and Mazurkiewicz traces that have been studied separately. We show that satisfiability and model checking are decidable in EXPTIME and 2EXPTIME, depending on the precise path modalities.}, }
2010
 R. Bonnet, A. Finkel, J. Leroux, M. Zeitoun, PlaceBoundedness for Vector Addition Systems with one zerotest. In FSTTCS'10, pp. 192â203, LeibnizZentrum fĂŒr Informatik. 2010. doi pdf abstract Reachability and boundedness problems have been shown decidable for Vector Addition Systems with one zerotest. Surprisingly, placeboundedness remained open. We provide here a variation of the KarpMiller algorithm to compute a basis of the downward closure of the reachability set which allows to decide placeboundedness. This forward algorithm is able to pass the zerotests thanks to a finer cover, hybrid between the reachability and cover sets, reclaiming accuracy on one component. We show that this filtered cover is still recursive, but that equality of two such filtered covers, even for usual Vector Addition Systems (with no zerotest), is undecidable. bibtex
@inproceedings{BFLZfsttcs10, author = {Bonnet, R. and Finkel, A. and Leroux, J. and Zeitoun, M.}, booktitle = {{FSTTCS'10}}, DOI = {10.4230/LIPIcs.FSTTCS.2010.192}, editor = {Lodaya, Kamal and Mahajan, Meena}, pages = {192203}, publisher = {LeibnizZentrum fĂŒr Informatik}, series = {LIPIcs}, volume = 8, year = 2010, title = {PlaceBoundedness for Vector Addition Systems with one zerotest}, url = {http://drops.dagstuhl.de/opus/volltexte/2010/2863/pdf/17.pdf}, abstract = {Reachability and boundedness problems have been shown decidable for Vector Addition Systems with one zerotest. Surprisingly, placeboundedness remained open. We provide here a variation of the KarpMiller algorithm to compute a basis of the downward closure of the reachability set which allows to decide placeboundedness. This forward algorithm is able to pass the zerotests thanks to a finer cover, hybrid between the reachability and cover sets, reclaiming accuracy on one component. We show that this filtered cover is still recursive, but that equality of two such filtered covers, even for usual Vector Addition Systems (with no zerotest), is undecidable.}, }
 B. Bollig, P. Gastin, B. Monmege, M. Zeitoun, Pebble weighted automata and transitive closure logics. In ICALP'10, pp. 587598, Springer. 2010. doi pdf abstract We introduce new classes of weighted automata on words. Equipped with pebbles and a twoway mechanism, they go beyond the class of recognizable formal power series, but capture a weighted version of firstorder logic with bounded transitive closure. In contrast to previous work, this logic allows for unrestricted use of universal quantification. Our main result states that pebble weighted automata, nested weighted automata, and this weighted logic are expressively equivalent. We also give new logical characterizations of the recognizable series. bibtex
@inproceedings{Bollig&Gastin&Monmege&Zeitoun:2010, author = {B. Bollig and P. Gastin and B. Monmege and M. Zeitoun}, title = {Pebble weighted automata and transitive closure logics}, booktitle = {{ICALP'10}}, editor = {Samson Abramsky}, pages = {587598}, year = 2010, volume = 6199, series = {Lect. Notes Comp. Sci.}, publisher = {Springer}, doi = {10.1007/9783642141621_49}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/BGMZicalp10.pdf}, abstract = {We introduce new classes of weighted automata on words. Equipped with pebbles and a twoway mechanism, they go beyond the class of recognizable formal power series, but capture a weighted version of firstorder logic with bounded transitive closure. In contrast to previous work, this logic allows for unrestricted use of universal quantification. Our main result states that pebble weighted automata, nested weighted automata, and this weighted logic are expressively equivalent. We also give new logical characterizations of the recognizable series.}, }
2009
 A. Muscholl, I. Walukiewicz, M. Zeitoun, A look at the control of asynchronous automata. In Perspectives in Concurrency Theory  A Festschrift for P.S. Thiagarajan, pp. 356â371, Universities Press. 2009. pdf abstract This paper is a survey of control of distributed systems. bibtex
@inbook{Muscholl&Walukiewicz&Zeitoun:08, author = {A. Muscholl and I. Walukiewicz and M. Zeitoun}, title = {A look at the control of asynchronous automata}, booktitle = {Perspectives in Concurrency Theory  A Festschrift for P.S. Thiagarajan}, pages = {356371}, year = 2009, editor = {K. Lodaya and M. Mukund and R. Ramanujam}, publisher = {Universities Press}, ISBN = {9788173716522}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/DistGamesMWZ.pdf}, abstract = {This paper is a survey of control of distributed systems.}, }
 J. Almeida, J.C. Costa, M. Zeitoun, Some structural properties of the free profinite aperiodic semigroup. In AutoMathA plenary conference, 2009. pdf abstract Profinite semigroups provide powerful tools to understand properties of classes of regular languages. Until very recently however, little was known on the structure of âlargeâ relatively free profinite semigroups. In this paper, we present new results obtained for the class of all finite aperiodic (that is, groupfree) semigroups. Given a finite alphabet X, we focus on the following problems: (1) the word problem for Ïterms on X evaluated on the free proaperiodic semigroup, and (2) the computation of closures of regular languages in the Ïsubsemigroup of the free proaperiodic semigroup generated by X. bibtex
@inproceedings{ACZ:automatha:09, author = {J. Almeida and J.C. Costa and M. Zeitoun}, title = {Some structural properties of the free profinite aperiodic semigroup}, booktitle = {AutoMathA plenary conference}, note = {Local proceedings}, year = 2009, url = {http://hal.archivesouvertes.fr/docs/00/94/89/98/PDF/ACZAutomatha09.pdf}, abstract = {Profinite semigroups provide powerful tools to understand properties of classes of regular languages. Until very recently however, little was known on the structure of "large" relatively free profinite semigroups. In this paper, we present new results obtained for the class of all finite aperiodic (that is, groupfree) semigroups. Given a finite alphabet X, we focus on the following problems: (1) the word problem for Ïterms on X evaluated on the free proaperiodic semigroup, and (2) the computation of closures of regular languages in the Ïsubsemigroup of the free proaperiodic semigroup generated by X.}, }
2008
 R. Bernard, S. Metge, F. Pouzolz, P. Bieber, A. Griffault, M. Zeitoun, Altarica refinement for heterogeneous granularity models analysis. , pp. 2B3, HermĂšs. 2008. pdf abstract We define a notion of refinement for AltaRica models in order to analyze the safety of systems described at various levels of detail. We describe a technique based on the Mec V modelchecker to automatically check that one model refines another one. We present two theoretical results: the first one allows to verify refinement by focusing on one component of the model at a time, the second result defines the kind of requirements that are preserved by refinement. We propose to use these theoretical results in order to ease the safety assessment of a set of interconnected aeronautical systems. bibtex
@inproceedings{BMPBGZ08refinement, author = {R. Bernard and S. Metge and F. Pouzolz and P. Bieber and A. Griffault and M. Zeitoun}, title = {Altarica refinement for heterogeneous granularity models analysis}, note = {LambdaMu, 16Ăšme CongrĂšs de MaĂźtrise des Risques et de SĂ»retĂ© de Fonctionnement}, year = 2008, organization = {IMDRSdf}, publisher = {HermĂšs}, pages = {2B3}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/LM16_2B3_RB.pdf}, abstract = {We define a notion of refinement for AltaRica models in order to analyze the safety of systems described at various levels of detail. We describe a technique based on the Mec V modelchecker to automatically check that one model refines another one. We present two theoretical results: the first one allows to verify refinement by focusing on one component of the model at a time, the second result defines the kind of requirements that are preserved by refinement. We propose to use these theoretical results in order to ease the safety assessment of a set of interconnected aeronautical systems.} }
 J. Almeida, J. C. Costa, M. Zeitoun, â”terms over finite aperiodic semigroups. In Int. Conf. on Relations, Orders and Graphs, ROGICS'08, pp. 364â371, 2008. pdf abstract This paper provides a characterization of pseudowords over the pseudovariety of all finite aperiodic semigroups that are given by Ïterms, that is that can be obtained from the free generators using only multiplication and the Ïpower. A necessary and sufficient condition for this property to hold turns out to be given by the conjunction of two rather simple finiteness conditions: the nonexistence of infinite antichains of factors and the rationality of the language of McCammond normal forms of Ïterms that define factors. bibtex
@inproceedings{Almeida&Costa&Zeitoun:2008a, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {â”terms over finite aperiodic semigroups}, booktitle = {Int. Conf. on Relations, Orders and Graphs, ROGICS'08}, year = 2008, editor = {Y. Boudabbous and N. Zaguia}, pages = {364371}, isbn = {9780980949803}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/ACZ2008.pdf}, abstract = {This paper provides a characterization of pseudowords over the pseudovariety of all finite aperiodic semigroups that are given by Ïterms, that is that can be obtained from the free generators using only multiplication and the Ïpower. A necessary and sufficient condition for this property to hold turns out to be given by the conjunction of two rather simple finiteness conditions: the nonexistence of infinite antichains of factors and the rationality of the language of McCammond normal forms of Ïterms that define factors.} }
 B. Genest, A. Muscholl, O. Serre, M. Zeitoun, Tree pattern rewritting systems. In ATVA'08, pp. 332â346, Springer. 2008. doi pdf abstract Classical verification often uses abstraction when dealing with data. On the other hand, dynamic XMLbased applications have become pervasive, for instance with the ever growing importance of web services. We define here Tree Pattern Rewriting Systems (TPRS) as an abstract model of dynamic XMLbased documents. TPRS systems generate infinite transition systems, where states are unranked and unordered trees (hence possibly modeling XML documents). Their guarded transition rules are described by means of tree patterns. Our main result is that given a TPRS system (T , R), a tree pattern P and some integer k such that any reachable document from T has depth at most k, it is decidable (albeit of non elementary complexity) whether some tree matching P is reachable from T. bibtex
@InProceedings{Genest&Muscholl&Serre&Zeitoun:2008, author = {B. Genest and A. Muscholl and O. Serre and M. Zeitoun}, title = {Tree pattern rewritting systems}, booktitle = {ATVA'08}, editor = {M. Kim and M. Viswanathan}, pages = {332346}, year = 2008, volume = {5311}, series = {Lect. Notes Comp. Sci.}, publisher = {Springer}, doi = {10.1007/9783540883876_29}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/GenestMuschollSerreZeitounATVA2008long.pdf}, abstract = {Classical verification often uses abstraction when dealing with data. On the other hand, dynamic XMLbased applications have become pervasive, for instance with the ever growing importance of web services. We define here Tree Pattern Rewriting Systems (TPRS) as an abstract model of dynamic XMLbased documents. TPRS systems generate infinite transition systems, where states are unranked and unordered trees (hence possibly modeling XML documents). Their guarded transition rules are described by means of tree patterns. Our main result is that given a TPRS system (T , R), a tree pattern P and some integer k such that any reachable document from T has depth at most k, it is decidable (albeit of non elementary complexity) whether some tree matching P is reachable from T.} }
 N. Caniart, E. Fleury, J. Leroux, M. Zeitoun, Accelerating Interpolationbased ModelChecking. In TACAS'08, pp. 428442, Springer. 2008. doi pdf abstract Interpolationbased modelchecking and acceleration techniques have been widely proved successful and efficient for reachability checking. Surprisingly, these two techniques have never been combined to strengthen each other. Intuitively, acceleration provides underapproximation of the reachability set by computing the exact effect of some controlflow cycles and combining them with other transitions into an underapproximation. On the other hand, interpolationbased modelchecking is refining an overapproximation of the reachable states based on spurious errortraces. The goal of this paper is to combine acceleration techniques with interpolationbased modelchecking at the refinement stage. Our method, the socalled interpolant acceleration, helps to refine the abstraction, ruling out not only a single spurious errortrace but a possibly infinite set of errortraces obtained by any unrolling of its cycles. Interpolant acceleration is also proved to strictly enlarge the set of transformations that can be usually handled by acceleration techniques. bibtex
@InProceedings{caniart&fleury&leroux&zeitoun:2008:tacas, author = {N. Caniart and E. Fleury and J. Leroux and M. Zeitoun}, title = {Accelerating Interpolationbased ModelChecking}, booktitle = {TACAS'08}, Editor = {C. R. Ramakrishnan and J. Rehof}, publisher = {Springer}, series = {Lect. Notes Comp. Sci.}, year = 2008, volume = {4963}, pages = {428442}, doi = {10.1007/9783540788003_32}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/CaniartFleuryLerouxZeitoun.TACAS2008.pdf}, abstract = {Interpolationbased modelchecking and acceleration techniques have been widely proved successful and efficient for reachability checking. Surprisingly, these two techniques have never been combined to strengthen each other. Intuitively, acceleration provides underapproximation of the reachability set by computing the exact effect of some controlflow cycles and combining them with other transitions into an underapproximation. On the other hand, interpolationbased modelchecking is refining an overapproximation of the reachable states based on spurious errortraces. The goal of this paper is to combine acceleration techniques with interpolationbased modelchecking at the refinement stage. Our method, the socalled interpolant acceleration, helps to refine the abstraction, ruling out not only a single spurious errortrace but a possibly infinite set of errortraces obtained by any unrolling of its cycles. Interpolant acceleration is also proved to strictly enlarge the set of transformations that can be usually handled by acceleration techniques.}, }
2007
 J. Almeida, J. C. Costa, M. Zeitoun, Complete reducibility of pseudovarieties. In Proceedings of the Conference on Semigroups and Formal Languages (Lisbon, 2005), pp. 9â25, World Scientific. 2007. doi pdf abstract The notion of reducibility for a pseudovariety has been introduced as an abstract property which may be used to prove decidability results for various pseudovariety constructions. This paper is a survey of recent results establishing this and the stronger property of complete reducibility for specific pseudovarieties. bibtex
@InProceedings{Almeida&Costa&Zeitoun:CompleteReducibilityR:2007, author = {J. Almeida and J. C. Costa and M. Zeitoun}, title = {Complete reducibility of pseudovarieties}, booktitle = {Proceedings of the Conference on Semigroups and Formal Languages (Lisbon, 2005)}, year = 2007, pages = {925}, publisher = {World Scientific}, doi = {10.1142/9789812708700_0002}, note = {In honour of D. McAlister's 65th birthday}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/AlmeidaCostaZeitounCSL07.pdf}, abstract = {The notion of reducibility for a pseudovariety has been introduced as an abstract property which may be used to prove decidability results for various pseudovariety constructions. This paper is a survey of recent results establishing this and the stronger property of complete reducibility for specific pseudovarieties.}, }
2006
 P. Gastin, N. Sznajder, M. Zeitoun, Distributed synthesis for wellconnected architectures. In FSTTCS'06, pp. 321â332, Springer. 2006. doi pdf abstract We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures with arbitrary delays on processes. External means that the specification only relates input and output variables. We introduce the subclass of uniformly wellconnected (UWC) architectures for which there exists a routing allowing each output process to get the values of all inputs it is connected to, as soon as possible. We prove that the distributed synthesis problem is decidable on UWC architectures if and only if the set of all sets of input variables visible by output variables is totally ordered, under set inclusion. We also show that if we extend this class by letting the routing depend on the output process, then the previous decidability result fails. Finally, we provide a natural restriction on specifications under which the whole class of UWC architectures is decidable. bibtex
@InProceedings{gastin&sznajder&zeitoun:2006:fsttcs, author = {P. Gastin and N. Sznajder and M. Zeitoun}, title = {Distributed synthesis for wellconnected architectures}, booktitle = {{FSTTCS'06}}, Editor = {Garg, Naveen and ArunKumar, S.}, publisher = {Springer}, series = {Lect. Notes Comp. Sci.}, year = 2006, volume = {4337}, pages = {321332}, doi = {10.1007/11944836}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/GastinSznajderZeitounFSTTCS06.pdf}, abstract = {We study the synthesis problem for external linear or branching specifications and distributed, synchronous architectures with arbitrary delays on processes. External means that the specification only relates input and output variables. We introduce the subclass of uniformly wellconnected (UWC) architectures for which there exists a routing allowing each output process to get the values of all inputs it is connected to, as soon as possible. We prove that the distributed synthesis problem is decidable on UWC architectures if and only if the set of all sets of input variables visible by output variables is totally ordered, under set inclusion. We also show that if we extend this class by letting the routing depend on the output process, then the previous decidability result fails. Finally, we provide a natural restriction on specifications under which the whole class of UWC architectures is decidable.}, }
2005
 LoĂŻc HĂ©louĂ«t, M. Zeitoun, Aldric Degorre, Scenarios and Covert channels, another gameâŠ. In Games in Design and Verification, GDV '04, pp. 93â116, Elsevier. 2005. doi pdf abstract Covert channels are information leaks in systems that use resources to transfer secretly a message. They are a threat for security, performance, but also for a system's profitability. This paper proposes a new approach to detect covert channels from scenario models of protocols. The problem of finding covert channels in scenarios is first modeled as a game, in which a pair of malicious users {S,R} is trying to transfer information while the rest of the protocol tries to prevent it. The messages transferred are encoded by behavioral choices at some precise moments, and decoded by a transducer whose input vocabulary is an observation of the system. We then characterize the presence of a covert channel as the existence of a winning strategy for {S,R} and of a decoder. bibtex
@InProceedings{helouet&zeitoun°orre:2005, author = {LoĂŻc HĂ©louĂ«t and M. Zeitoun and Aldric Degorre}, title = {Scenarios and Covert channels, another game...}, booktitle = {Games in Design and Verification, GDV '04}, year = 2005, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier}, volume = 119, number = 1, pages = {93116}, doi = {10.1016/j.entcs.2004.07.010}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/GDV04.pdf}, abstract = {Covert channels are information leaks in systems that use resources to transfer secretly a message. They are a threat for security, performance, but also for a system's profitability. This paper proposes a new approach to detect covert channels from scenario models of protocols. The problem of finding covert channels in scenarios is first modeled as a game, in which a pair of malicious users {S,R} is trying to transfer information while the rest of the protocol tries to prevent it. The messages transferred are encoded by behavioral choices at some precise moments, and decoded by a transducer whose input vocabulary is an observation of the system. We then characterize the presence of a covert channel as the existence of a winning strategy for {S,R} and of a decoder.} }
2004
 P. Gastin, P. Moro, M. Zeitoun, Minimization of counterexamples in SPIN. In SPIN'04, pp. 92â108, Springer. 2004. doi pdf abstract We propose an algorithm to find a counterexample to some property in a finite state program. This algorithm is derived from SPIN's one, but it finds a counterexample faster than SPIN does. In particular it still works in linear time. Compared with SPIN's algorithm, it requires only one additional bit per state stored. We further propose another algorithm to compute a counterexample of minimal size. Again, this algorithm does not use more memory than SPIN does to approximate a minimal counterexample. The cost to find a counterexample of minimal size is that one has to revisit more states than SPIN. We provide an implementation and discuss experimental results. bibtex
@InProceedings{gastin&moro&zeitoun:2004:spin, author = {P. Gastin and P. Moro and M. Zeitoun}, title = {Minimization of counterexamples in SPIN}, booktitle = {{SPIN'04}}, publisher = {Springer}, series = {Lect. Notes Comp. Sci.}, year = 2004, volume = 2989, pages = {92108}, doi = {10.1007/b96721}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/SPIN04.pdf}, abstract = {We propose an algorithm to find a counterexample to some property in a finite state program. This algorithm is derived from SPIN's one, but it finds a counterexample faster than SPIN does. In particular it still works in linear time. Compared with SPIN's algorithm, it requires only one additional bit per state stored. We further propose another algorithm to compute a counterexample of minimal size. Again, this algorithm does not use more memory than SPIN does to approximate a minimal counterexample. The cost to find a counterexample of minimal size is that one has to revisit more states than SPIN. We provide an implementation and discuss experimental results.} }
 P. Gastin, Benjamin Lerman, M. Zeitoun, Distributed games with causal memory are decidable for seriesparallel systems. In FSTTCS'04, pp. 275â286, Springer. 2004. doi pdf abstract This paper deals with distributed control problems by means of distributed games played on Mazurkiewicz traces. The main difference with other notions of distributed games recently introduced is that, instead of having a local view, strategies and controllers are able to use a more accurate memory, based on their causal view. Our main result states that using the causal view makes the control synthesis problem decidable for seriesparallel systems for all recognizable winning conditions on finite behaviors, while this problem with local view was proved undecidable even for reachability conditions. bibtex
@InProceedings{gastin&lerman&zeitoun:2004:fsttcs, author = {P. Gastin and Benjamin Lerman and M. Zeitoun}, title = {Distributed games with causal memory are decidable for seriesparallel systems}, Booktitle = {{FSTTCS'04}}, publisher = {Springer}, series = {Lect. Notes Comp. Sci.}, year = 2004, volume = 3328, pages = {275286}, doi = {10.1007/9783540305385_23}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/GastinLermanZeitounFSTTCS04.pdf}, abstract = {This paper deals with distributed control problems by means of distributed games played on Mazurkiewicz traces. The main difference with other notions of distributed games recently introduced is that, instead of having a local view, strategies and controllers are able to use a more accurate memory, based on their causal view. Our main result states that using the causal view makes the control synthesis problem decidable for seriesparallel systems for all recognizable winning conditions on finite behaviors, while this problem with local view was proved undecidable even for reachability conditions.}, }
 P. Gastin, Benjamin Lerman, M. Zeitoun, Distributed games and distributed control for asynchronous systems. In LATIN'04, pp. 455â465, Springer. 2004. doi pdf abstract We introduce distributed games over asynchronous transition systems to model a distributed controller synthesis problem. A game involves two teams and is not turnbased: several players of both teams may simultaneously be enabled. We define distributed strategies based on the causal view that players have of the system. We reduce the problem of finding a winning distributed strategy with a given memory to finding a memoryless winning distributed strategy in a larger distributed game. We reduce the latter problem to finding a strategy in a a classical 2players game. This allows to transfer results from the sequential case to this distributed setting. bibtex
@InProceedings{gastin&lerman&zeitoun:2004:latin, author = {P. Gastin and Benjamin Lerman and M. Zeitoun}, title = {Distributed games and distributed control for asynchronous systems}, booktitle = {{LATIN'04}}, editor = {FarachColton, M.}, publisher = {Springer}, pages = {455465}, series = {Lect. Notes Comp. Sci.}, year = 2004, volume = 2976, doi = {10.1007/b95852}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/LATIN04.pdf}, abstract = {We introduce distributed games over asynchronous transition systems to model a distributed controller synthesis problem. A game involves two teams and is not turnbased: several players of both teams may simultaneously be enabled. We define distributed strategies based on the causal view that players have of the system. We reduce the problem of finding a winning distributed strategy with a given memory to finding a memoryless winning distributed strategy in a larger distributed game. We reduce the latter problem to finding a strategy in a a classical 2players game. This allows to transfer results from the sequential case to this distributed setting.}, }
 J. Almeida, M. Zeitoun, The equational theory of â”terms for finite Rtrivial semigroups. In Semigroups and Languages, pp. 1â23, World Scientific. 2004. doi pdf abstract A new topological representation for free profinite Rtrivial semigroups in terms of spaces of vertexlabeled complete binary trees is obtained. Such a tree may be naturally folded into a finite automaton if and only if the element it represents is an Ïterm. The variety of Ïsemigroups generated by all finite Rtrivial semigroups, with the usual interpretation of the Ïpower, is then studied. A simple infinite basis of identities is exhibited and a lineartime solution of the word problem for relatively free Ïsemigroups is presented. This work is also compared with recent work of Bloom and Choffrut on transfinite words. bibtex
@InProceedings{almeida&zeitoun:2004:sal, author = {J. Almeida and M. Zeitoun}, title = {The equational theory of â”terms for finite Rtrivial semigroups}, booktitle = {Semigroups and Languages}, editor = {M. Branco and G.M.S. Gomes}, year = 2004, publisher = {World Scientific}, doi = {10.1142/9789812702616_0001}, pages = {123}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/Lisbon03.pdf}, abstract = {A new topological representation for free profinite Rtrivial semigroups in terms of spaces of vertexlabeled complete binary trees is obtained. Such a tree may be naturally folded into a finite automaton if and only if the element it represents is an Ïterm. The variety of Ïsemigroups generated by all finite Rtrivial semigroups, with the usual interpretation of the Ïpower, is then studied. A simple infinite basis of identities is exhibited and a lineartime solution of the word problem for relatively free Ïsemigroups is presented. This work is also compared with recent work of Bloom and Choffrut on transfinite words.} }
2003
 LoĂŻc HĂ©louĂ«t, Claude Jard, M. Zeitoun, Covert channels detection in protocols using scenarios. In SPV'03, Security Protocols Verification, pp. 21â25, 2003. pdf abstract This paper presents an approach to detect illegal information flows from requirements expressed as highlevel scenarios. bibtex
@InProceedings{helouet&jard&zeitoun:2003:spv, author = {LoĂŻc HĂ©louĂ«t and Claude Jard and M. Zeitoun}, title = {Covert channels detection in protocols using scenarios}, booktitle = {{SPV'03, Security Protocols Verification}}, editor = {M. Rusinowitch}, year = 2003, pages = {2125}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/spv03.pdf}, abstract = {This paper presents an approach to detect illegal information flows from requirements expressed as highlevel scenarios.}, }
2002
 Blaise Genest, Anca Muscholl, Helmut Seidl, M. Zeitoun, Infinitestate High level MSCs: realizability and modelchecking. In ICALP'02, pp. 657â668, Springer. 2002. doi pdf abstract Message sequence charts (MSC) and HighLevel MSC (HMSC) is a visual notation for asynchronously communicating processes and a standard of the ITU. They usually represent incomplete specifications of required or forbidden properties of communication protocols. We consider in this paper two basic problems concerning the automated validation of HMSC sp ecifications, namely modelchecking and synthesis. We identify natural syntactic restrictions of HMSCs for which we can solve the above questions. We show first that modelchecking for globallycooperative (and locallycooperative) HMSCs is decidable within the same complexity as for the restricted class of bounded HMSCs. Furthermore, modelchecking localchoice HMSCs turns out to be as efficient as for finitestate (sequential) systems. The study of locallycooperative and localchoice HMSCs is motivated by the synthesis question, i.e., the question of implementing HMSCs through communicating finitestate machines (CFM) with additional message data. We show that locallycooperative and localchoice HMSCs are always implementable. Furthermore, the implementation of a localchoice HMSC is deadlockfree and of linear size. bibtex
@InProceedings{genest&muscholl&seidl&zeitoun:2002, author = {Blaise Genest and Anca Muscholl and Helmut Seidl and M. Zeitoun}, title = {{Infinitestate High level MSCs: realizability and modelchecking}}, booktitle = {{ICALP'02}}, editor = {P. Widmayer and others}, pages = {657668}, year = 2002, volume = 2380, series = {Lect. Notes Comp. Sci.}, publisher = {Springer}, doi = {10.1007/3540454659_56}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/InfHMSC.pdf}, abstract = {Message sequence charts (MSC) and HighLevel MSC (HMSC) is a visual notation for asynchronously communicating processes and a standard of the ITU. They usually represent incomplete specifications of required or forbidden properties of communication protocols. We consider in this paper two basic problems concerning the automated validation of HMSC sp ecifications, namely modelchecking and synthesis. We identify natural syntactic restrictions of HMSCs for which we can solve the above questions. We show first that modelchecking for globallycooperative (and locallycooperative) HMSCs is decidable within the same complexity as for the restricted class of bounded HMSCs. Furthermore, modelchecking localchoice HMSCs turns out to be as efficient as for finitestate (sequential) systems. The study of locallycooperative and localchoice HMSCs is motivated by the synthesis question, i.e., the question of implementing HMSCs through communicating finitestate machines (CFM) with additional message data. We show that locallycooperative and localchoice HMSCs are always implementable. Furthermore, the implementation of a localchoice HMSC is deadlockfree and of linear size.}, }
1996
 M. Zeitoun, On the join of two pseudovarieties. In Semigroups, Automata and Languages, pp. 281â288, World Scientific. 1996. pdf abstract This paper is a survey of some recent developments in the theory of finite semigroups. bibtex
@Inproceedings{zeitoun:1996:a, author = {M. Zeitoun}, title = {On the join of two pseudovarieties}, booktitle = {{Semigroups, Automata and Languages}}, year = 1996, pages = {281288}, editor = {J. Almeida and G.M.S. Gomes and P.V. Silva}, publisher = {World Scientific}, url = {http://www.labri.fr/perso/zeitoun/research/pdf/SAL.pdf}, abstract = {This paper is a survey of some recent developments in the theory of finite semigroups.} }
Enseignement
Supports d'enseignement 2016â17
 Logique et langages, M2 AMF IF.
 ThĂ©orie de la ComplexitĂ©, M1 CSI.
 Informatique, Licence Culture Humaniste & Scientifique.
 Programmation Fonctionnelle, L2 Informatique.
Sites et textes sur l'enseignement de l'informatique
 L'informatique sans ordinateur: CS Unplugged.
 Blog binaire.
 Association Enseignement public & informatique
 Liens sur la page du cours Licence CHS.
 Math Ă modeler en Aquitaine