Thomas Colcombet: Bibliography

# Disclaimer

The electronic documents provided on this page fulfill the copyright of the publishers. In particular, the publisher’s versions are not available, but the pre-refereeing or post-refereeing versions are.

If you want to know what you are allowed or not allowed to do, you can use the Sherpa/Romeo database which collects the publisher copyright policies.

# Unpublished

• [Col13] . “The Factorisation Forest Theorem”. To appear in the handbook “Automata: from Mathematics to Applications”. 37 pages. 2013. -pdf--
Abstract: This chapter is devoted to the presentation of the factorisation forest theorem, a deep result due to Simon, which provides advanced Ramsey-like arguments in the context of algebra, automata, and logic. We present several proofs and several variants the result, as well as applications.
• [CGM13] , , . “Uniformization Results on Regular Cost Functions”. In preparation. 2013. --
Abstract: B-automata are automata that can compute functions from words to non-negative integers or infinity. In this paper we give another semantics to the hierarchical variant of these automata. This new semantics is equivalent to the classical one in the terminology of cost functions: functions computed are equivalent up to a polynomial factor. We provide three applications of the technique. Our first application shows that it is possible to evaluate, reading once the word from left to right, in deterministic logspace, a B-automaton with the new semantics. A similar evaluation would require polynomial space with the original semantics. Our second theorem shows that for games with hB-quantitative objectives, there are positional determinacy strategies that are uniformly optimal, i.e., optimal from any starting point. Finally, we introduce a new form of history-determinism that is uniform in the sense that translation strategies are independent from bounds. We show that uniform history-determinism cannot be enforced for usual B-automata, and we disclose new forms of (equivalent) automata that have this property.
• [Col11] . “Safra-like constructions for regular cost functions over finite words”. working paper or preprint. Mar. 2011. -url-pdf--
Abstract: Regular cost functions have been introduced recently as an extension of the notion of regular languages with counting capabilities, which retains strong closure, equivalence, and decidability properties. Cost functions are functions ranging over $N\cup \left\{\infty \right\}$, and considered modulo an equivalence which preserves the existence of bounds over each subset of the domain. A central result in the theory of regular cost functions over words is the duality theorem stating that the two dual forms of automata, namely Band S-automata, are equivalent. The only known proof of this result relies on the translation into an equivalent algebraic formalism. In this paper, we describe direct translations from hierarchical B-automata to history-deterministic S-automata and from hierarchical S-automata to history deterministic B-automata. We furthermore describe how to optimize the number of counters of the output automaton, and how to make them hierarchical. This construction is reminiscent of the famous construction of Safra for the determinization of automata over infinite words.
• [CF18] , . Parity games and universal graphs. arXiv. 2018. -url-pdf--.

# 2018

• [CCP18] , , . “An algebraic approach to MSO-definability on countable linear orderings”. In: The Journal of Symbolic Logic 83.3 (2018), pages 1147–1189. -pdf--
Abstract: We develop an algebraic notion of recognizability for languages of words indexed by countable linear orderings. We prove that this notion is effectively equivalent to definability in monadic second-order (MSO) logic. We also provide three logical applications. First, we establish the first known collapse result for the quantifier alternation of MSO logic over countable linear orderings. Second, we solve an open problem posed by Gurevich and Rabinovich, concerning the MSO-definability of sets of rational numbers using the reals in the background. Third, we establish the MSO-definability of the set of yields induced by an MSO-definable set of trees, confirming a conjecture posed by Bruyère, Carton, and Sénizergues.

# 2017

• [BC17] , . “Bounds in $\omega$-regularity”. In: Logical Methods in Computer Science 13.4 (2017). -pdf--
Abstract: We define a new class of languages of $\omega$-words, strictly extending $\omega$-regular languages. One way to present this new class is by a type of regular expressions. The new expressions are an extension of $\omega$-regular expressions where two new variants of the Kleene star $L*$ are added: $LB$ and $LS$. These new exponents are used to say that parts of the input word have bounded size, and that parts of the input can have arbitrarily large sizes, respectively. For instance, the expression $\left(aBb\right)\omega$ represents the language of infinite words over the letters $a,b$ where there is a common bound on the number of consecutive letters $a$. The expression $\left(aSb\right)\omega$ represents a similar language, but this time the distance between consecutive $b$’s is required to tend toward the infinite. We develop a theory for these languages, with a focus on decidability and closure. We define an equivalent automaton model, extending Büchi automata. The main technical result is a complementation lemma that works for languages where only one type of exponent—either $LB$ or $LS$—is used. We use the closure and decidability results to obtain partial decidability results for the logic MSOLB, a logic obtained by extending monadic second-order logic with new quantifiers that speak about the size of sets.
• [CP17a] , . “Automata Minimization: a Functorial Approach”. In: CALCO: Algebra and Coalgebra in Computer Science. 2017. -url--
Abstract: In this paper we regard languages and their acceptors – such as deterministic or weighted automata or transducers – as functors from input categories that specify the type of the languages and of the machines to categories that specify the type of outputs. Our results are as follows: a) We provide sufficient conditions on the output category so that minimization of the corresponding automata is guaranteed. b) We show how to lift adjunctions between the categories for output values to adjunctions between categories of automata. c) We show how this framework can be instantiated to unify several phenomena in automata theory, starting with determinization and minimization (which have been previously studied from a coalgebraic and duality theoretic perspective). We also show how subsequential transducers can be seen as functors valued in a Kleisli category and explain Choffrut’s minimization algorithm. We also give an alternative proof of correctness of Brzozowski’s minimization algorithm.
• [CP17b] , . “Automata in the Category of Glued vector spaces”. In: MFCS 2017: Mathematical Foundations of Computer Science. 2017, 52:1–52:14. -url-pdf-slides--
Abstract: In this paper, we adopt of categorical approach to the conception of automata classes enjoying minimisation by design. The main instantiation of this construction is the new class of automata that are hybrid between deterministic and vector space automata.
• [CP17c] , . “Automata and Minimization”. In: SIGLOG News 4.2 (2017), pages 4–27. -pdf-slides--
Abstract: Already in the seventies, strong results illustrating the intimate relationship between category theory and automata theory have been described and are still investigated. In this column, we provide a uniform presentation of the basic concepts that underlie minimization results in automata theory. We then use this knowledge for introducing a new model of automata that is an hybrid of deterministic finite automata and automata weighted over a field. These automata are very natural, and enjoy minimization result by design. The presentation of this paper is indeed categorical in essence, but it assumes no prior knowledge from the reader. It is also non-conventional in that it is neither algebraic, nor co-algebraic oriented.
• [CJLS17] , , , . “Perfect Half Space Games”. In: LICS. IEEE Computer Society, 2017, pages 1–11. -pdf--
Abstract: We introduce perfect half space games, in which the goal of Player 2 is to make the sums of encountered multi-dimensional weights diverge in a direction which is consistent with a chosen sequence of perfect half spaces (chosen dynamically by Player 2). We establish that the bounding games of Jurdzinski et al. (ICALP 2015) can be reduced to perfect half space games, which in turn can be translated to the lexicographic energy games of Colcombet and Niwinski, and are positionally determined in a strong sense (Player 2 can play without knowing the current perfect half space). We finally show how perfect half space games and bounding games can be employed to solve multi-dimensional energy parity games in pseudo-polynomial time when both the numbers of energy dimensions and of priorities are fixed, regardless of whether the initial credit is given as part of the input or existentially quantified. This also yields an optimal 2-EXPTIME complexity with given initial credit, where the best known upper bound was non-elementary.
• [Col17] . “Logic and Regular Cost Functions”. In: LICS. Invited tutorial. IEEE Computer Society, 2017, pages 1–4. -pdf-slides--
Abstract: Regular cost functions offer a toolbox for automatically solving problems of existence of bounds, in a way similar to the theory of regular languages. More precisely, it allows to test the existence of bounds for quantities that can be defined in cost monadic second-order logic (a quantitative variant of monadic second-order logic) with inputs that range over finite words, infinite words, finite trees, and (sometimes) infinite trees. Though the initial results date from the works of Hashiguchi in the early eighties, it is during the last decade that the theory took its current shape and that many new results and applications have been established. In this tutorial, two connections linking logic with the theory of regular cost functions will be described. The first connection is a proof of a result of Blumensath, Otto and Weyer stating that it is decidable whether the fixpoint of a monadic second- order formula is reached within a bounded number of iterations over the class of infinite trees. The second connection is how non- standard models (and more precisely non-standard analysis) give rise to a unification of the theory of regular cost functions with the one of regular languages.
• [CDZ17] , , . “Automata and Program Analysis”. In: FCT. Springer, 2017, pages 3–10. -pdf-slides--
Abstract: We show how recent results concerning quantitative forms of automata help providing refined understanding of the properties of a system (for instance, a program). In particular, combining the size-change abstraction together with results concerning the asymptotic behavior of tropical au- tomata yields extremely fine complexity analysis of some pieces of code.

# 2016

• [CD16] , . “Approximate Comparison of Functions Computed by Distance Automata”. In: Theory Comput. Syst. 58.4 (2016), pages 579–613. -url--
Abstract: Distance automata are automata weighted over the semiring $\left(N\cup \left\{\infty \right\},min,+\right)$ (the tropical semiring). Such automata compute functions from words to $N\cup \left\{\infty \right\}$. It is known from Krob that the problems of deciding ‘$f\le g$’ or ‘$f=g$’ for $f$ and $g$ computed by distance automata is an undecidable problem. The main contribution of this paper is to show that an approximation of this problem is decidable. We present an algorithm which, given $\epsilon >0$ and two functions $f,g$ computed by distance automata, answers “yes” if $f\le \left(1-\epsilon \right)g$, “no” if $f\nleqq g$, and may answer “yes” or “no” in all other cases. This result highly refines previously known decidability results of the same type. The core argument behind this quasi-decision procedure is an algorithm which is able to provide an approximated finite presentation of the closure under products of sets of matrices over the tropical semiring. We also establish another theorem, of affine domination, stating that previously known decision procedures for cost-automata have an improved precision when used over distance automata.
• [CKMT16] , , , . “Cost Functions Definable by Min/Max Automata”. In: 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Edited by , . Volume 47. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, 29:1–29:13. isbn: 978-3-95977-001-9. -url-pdf--
Abstract: Regular cost functions form a quantitative extension of regular languages that share the array of characterisations the latter possess. In this theory, functions are treated only up to preservation of boundedness on all subsets of the domain. In this work, we subject the well known distance automata (also called min-automata), and their dual max-automata to this framework, and obtain a number of effective characterisations in terms of logic, expressions and algebra.
• [BCP16] , , . “On a Fragment of AMSO and Tiling Systems”. In: 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Edited by , . Volume 47. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, 19:1–19:14. isbn: 978-3-95977-001-9. -url-pdf--
Abstract: We prove that satisfiability over infinite words is decidable for a fragment of asymptotic monadic second-order logic. In this fragment we only allow formulae of the form $\exists t\forall s\exists r\varphi \left(r,s,t\right)$, where $\varphi$ does not use quantifiers over number variables, and variables r and s can be only used simul- taneously, in subformulae of the form $s.
• [CG16] , . “Games with bound guess actions”. In: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016. 2016, pages 257–266. -url-pdf-slides--
Abstract: We introduce games with (bound) guess actions. These are games in which the players may be asked along the play to provide numbers that need to satisfy some bounding constraints. These are natural extensions of domination games occurring in the regular cost function theory. In this paper we consider more specifically the case where the constraints to be bounded are regular cost functions, and the long term goal is an $\omega$-regular winning condition. We show that such games are decidable on finite arenas.
• [CF16] , . “The Bridge Between Regular Cost Functions and Omega-Regular Languages”. In: 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy. 2016, 126:1–126:13. -url-pdf-pdf(long)-slides--
Abstract: In this paper, we exhibit a one-to-one correspondence between $\omega$-regular languages and a subclass of regular cost functions over finite words, called $\omega$-regular like cost functions. This bridge between the two models allows one to readily import classical results such as the last appearance record or the McNaughton-Safra constructions to the realm of regular cost functions. In combination with game theoretic techniques, this also yields an optimal and simple procedure of history-determinisation for cost automata, a central result in the theory of regular cost functions.

# 2015

• [CLP15] , , . “Logics with rigidly guarded data tests”. In: Logical Methods in Computer Science 11.3 (2015). -url-pdf--
Abstract: The notion of orbit finite data monoid was recently introduced by Bojanczyk as an algebraic object for defining recognizable languages of data words. Following Buchi’s approach, we introduce a variant of monadic second-order logic with data equality tests that captures precisely the data languages recognizable by orbit finite data monoids. We also establish, following this time the approach of Schutzenberger, McNaughton and Papert, that the first-order fragment of this logic defines exactly the data languages recognizable by aperiodic orbit finite data monoids. Finally, we consider another variant of the logic that can be interpreted over generic structures with data. The data languages defined in this variant are also recognized by unambiguous finite memory automata.
• [CM15a] , . “Fragments of Fixpoint Logic on Data Words”. In: 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015. Edited by , . Volume 45. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pages 98–111. -url-pdf--
Abstract: We study two fragments of a fixpoint logic on data words that enjoy Boolean closure, and contain previously defined logics, namely two-variable first order logic and DataLTL. Our main contribution is the separation of these two classes using a reduction to circuit inexpressibility.
• [BCCV15] , , , . “The Complexity of Boundedness for Guarded Logics”. In: 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015. IEEE, 2015, pages 293–304. -url-pdf(long)--
Abstract: Given a formula phi(x,X) positive in X , the boundedness problem asks whether the fixpoint induced by phi is reached within some uniform bound independent of the structure (i.e. whether the fixpoint is spurious, and can in fact be captured by a finite unfolding of the formula). In this paper, we study the boundedness problem when phi is in the guarded fragment or guarded negation fragment of first-order logic, or the fixpoint extensions of these logics. It is known that guarded logics have many desirable computational and model theoretic properties, including in some cases decidable boundedness. We prove that boundedness for guarded negation fixpoint logic is decidable, and even 2EXPTIME-complete. Our proof extends the connection between guarded logics and automata, reducing boundedness for guarded logics to a question about cost automata on trees, a type of automaton with counters that assigns a natural number to each input rather than just a boolean.
• [CA15] , “Limited Set Quantifiers over Countable Linear Orders”. In: Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015. Edited by , , , . Volume 9135. Lecture Notes in Computer Science. Springer, 2015, pages 146–158. -url-pdf-pdf(long)-slides--
Abstract: In this paper, we study several sublogics of monadic second-order logic over countable linear orderings, such as first-order logic, first-order logic on cuts, weak monadic second-order logic, weak monadic second-ordered logic with cuts, as well as fragments of monadic second-order logic in which sets have to be well ordered or scattered. We give decidable algebraic characterizations of all these logics and compare their respective expressive power.
• [CM15b] , . “Combinatorial Expressions and Lowerbounds”. In: 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015. Edited by , . Volume 30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015, pages 249–261. -url-pdf-slides--
Abstract: A new paradigm, called combinatorial expressions, for computing functions expressing properties over an infinite domains is introduced. The main result is a generic technique, for showing indefinability of certain functions by the expressions, which uses a result, namely Hales-Jewett theorem, from Ramsey theory. An application of the technique for proving inexpressibility results for logics on metafinite structures is given. Apart from this, some extensions and normal form theorems are also presented.
• [Col15] . “Non-ambiguity in Automata Theory”. In: Descriptional Complexity of Formal Systems - 17th International Workshop, DCFS 2015. Edited by , . Volume 9118. Lecture Notes in Computer Science. Springer, 2015, pages 3–18. -url-pdf--
Abstract: Determinism of devices is a key aspect throughout all of computer science, simply for considerations of efficiency of the implementation. One possible way (among others) to relax this notion is to consider unambiguous machines: nondeterministic machines that have at most one accepting input on each entry. In this talk, we will investigate the nature of non-ambiguity in automata theory, surveying the cases of standard finite words up to infinite trees, as well as data-words. The goal of this talk will be to show how this notion of unambiguity is so far not well understood, yielding to difficult open questions. In the last part, I will present recent results with Gabriele Puppis and Michal Skrypczak that provide a deep insight in the data-word case.

# 2014

• [CFH14] , , . “Playing Safe”. In: FSTTCS 2014: Foundations of Software Technology and Theoretical Computer Science. Edited by , . Volume 29. LIPICs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pages 379–390. -pdf--
Abstract: We consider two-player games over graphs and give tight bounds on the memory size of strategies ensuring safety conditions. More specifically, we show that the minimal number of memory states of a strategy ensuring a safety condition is given by the size of the maximal antichain of left quotients with respect to language inclusion. This result holds for all safety conditions without any regularity assumptions, and for all (finite or infinite) graphs of finite degree. We give several applications of this general principle. In particular, we characterize the exact memory requirements for the opponent in generalized reachability games, and we prove the existence of optimal positional strategies in games with counters.
• [CM14] , . “Generalized Data Automata and Fixpoint Logic”. In: FSTTCS 2014: Foundations of Software Technology and Theoretical Computer Science. Edited by , . Volume 29. LIPICs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014, pages 267–278. -pdf--
Abstract: Data $\omega$-words are $\omega$-words where each position is additionally labelled by a data value from an infinite alphabet. They can be seen as graphs equipped with two sorts of edges: ‘next position’ and ‘next position with the same data value’. Based on this view, an extension of Data Automata called Generalized Data Automata (GDA) is introduced. While the decidability of emptiness of GDA is open, the decidability for a subclass class called Büchi GDA is shown using Multicounter Automata. Next a natural fixpoint logic is defined on the graphs of data $\omega$-words and it is shown that the $\mu$-fragment as well as the alternation-free fragment is undecidable. But the fragment which is defined by limiting the number of alternations between future and past formulas is shown to be decidable, by first converting the formulas to equivalent alternating Büchi automata and then to Büchi GDA.
• [BCC14] , , . “Asymptotic Monadic Second-Order Logic”. In: MFCS 2014: Mathematical Foundations of Computer Science. Edited by , , . Springer, 2014, pages 87–98. -pdf--
Abstract: This paper continues a research programme on the development of decidable extensions of monadic second-order logic in the spirit of the logic MSO+U. We introduce an extension of monadic second-order logic, asymptotic monadic second-order logic (AMSO), which refers to structures whose elements are weighted with non-negative integers and which can express constraints on these values. We provide several results concerning the expressive power of this logic over weighted infinite words, the most important being (1) the ”equivalence” of a natural extension of it, EAMSO, with MSO+U; (2) the proof that AMSO reaches arbitrarily high in the projective hierarchy; (3) the equivalence of the ”number-prenex fragment of AMSO” with WAMSO, the weak fragment of AMSO; (4) the proof that WAMSO reaches all finite levels of the Borel hierarchy; (5) new forms of tiling problems which are equivalent to the satisfiability of WAMSO. Our conjecture is that the satisfiability of AMSO is decidable (as for MSOpU). We believe it may be significantly simpler to solve this conjecture for AMSO than for MSOpU. The weak fragment is a promising intermediate step.
• [CDZ14] , , . “Size-Change Abstraction and Max-Plus Automata”. In: MFCS 2014: Mathematical Foundations of Computer Science Symposium, MFCS 2014. Edited by , , . Springer, 2014, pages 208–219. -pdf--
Abstract: Max-plus automata (over $ℕ\cup \left\{-\infty \right\}$) are finite devices that map input words to non-negative integers or $-\infty$. In this paper we present (a) an algorithm allowing to compute the asymptotic behaviour of max-plus automata, and (b) an application of this technique to the evaluation of the computational time complexity of programs. (a) Given a max-plus automaton computing a function $f$, we show that the longest word of value at most $N$ for $f$ has length $\Theta \left(N\alpha \right)$, where $\alpha$ is a computable rational number (or is infinite). (b) The size-change abstraction (SCA) is an a computational model used for abstracting the behaviour of real programs. Thanks to result (a), we show that the computational time complexity of terminating SCA instances is decidable: the maximal length of any sequence of transitions is exactly of asymptotic order $\Theta \left(N\alpha \right)$, where $\alpha$ is a computable rational number and where $N$ is the maximal value of the variables in the program.
• [BCKBP14] , , , , . “Two-Way Cost Automata and Cost Logics over Infinite Trees”. In: CSL-LICS 2014: 23rd EACSL Annual Conference on Computer Science Logic and 29th Annual ACM/IEEE Symposium on Logic in Computer Science. 2014, page 16. -pdf--
Abstract: Regular cost functions provide a quantitative extension of regular languages that retains most of their important properties, such as expressive power and decidability, at least over finite and infinite words and over finite trees. Much less is known over infinite trees. We consider cost functions over infinite trees defined by an extension of weak monadic second-order logic with a new fixed- point-like operator. We show this logic to be decidable, improving previously known decidability results for cost logics over infinite trees. The proof relies on an equivalence with a form of automata with counters called quasi-weak cost automata, as well as results about converting two-way alternating cost automata to one-way alternating cost automata.
• [CLP14] , , . Logics with rigidly guarded data tests. Long version of the MFCS 2011 paper. Published in Logical Methods in Computer Science, 2015. 2014. eprint: arXiv:1410.2022. -pdf--
Abstract: The notion of orbit finite data monoid was recently introduced by Bojańczyk as an algebraic object for defining recognizable languages of data words. Following Buuchi’s approach, we introduce a variant of monadic second-order logic with data equality tests that captures precisely the data languages recognizable by orbit finite data monoids. We also establish, following this time the approach of Schutzenberger, McNaughton and Papert, that the first-order fragment of this logic defines exactly the data languages recognizable by aperiodic orbit finite data monoids. Finally, we consider another variant of the logic that can be interpreted over generic structures with data. The data languages defined in this variant are also recognized by unambiguous finite memory automata.

# 2013

• [CD13] , . “Approximate Comparison of Distance Automata”. In: STACS 2013: 30th International Symposium on Theoretical Aspects of Computer Science. Edited by , . Volume 20. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pages 574–585. -pdf--
Abstract: Distance automata are automata weighted over the tropical semiring $\left(ℕ\cup \left\{\infty \right\},min,+\right)$. Such automata compute functions from words to $\left(ℕ\cup \left\{\infty \right\}$. It is known that testing $f is an undecidable problem for $f$ and $g$ computed by distance automata. The main contribution of this paper is to show that an approximation of this problem becomes decidable. We present an algorithm which given $ϵ>0$ and $f$, $g$ computed by distance automata answers ”yes” if $f<\left(1-ϵ\right)g$, ”no” if there is a word w such that $f\left(w\right)>g\left(w\right)$, and may answer ”yes” or ”no” in all other cases. This result highly refines previously known decidability results of the same type. The core argument behind this quasi-decision procedure is an algorithm which is able to provide an approximated finite presentation to the closure under products of sets of matrices over the tropical semiring. We also provide another theorem of affine domination which shows that previously known decision procedures for cost-automata have an improved precision when used over distance automata.
• [Col13a] . “Composition with algebra at the background”. In: CSR 2013: 8th International Computer Science Symposium in Russia. Lecture Notes in Computer Science. Springer, 2013, pages 391–404. -pdf--
Abstract: Gurevich and Rabinovich raised the following question: given a property of a set of rational numbers definable in the real line by a monadic second-order formula, is it possible to define it directly in the rational line? In other words, is it true that the presence of reals at the background do not increase the expressive power of monadic second-order logic? In this paper, we answer positively this question. The proof in itself is a simple application of classical and more recent techniques. This question will guide us in a tour of results and ideas related to monadic theories of linear orderings.
• [Col13b] . “Cost Functions with Several Orders of Magnitudes and the use of Relative Internal Set Theory”. In: LICS 2013: 28th Annual ACM/IEEE Symposium on Logic in Computer Science. 2013, page 123. -pdf--
Abstract: Cost monadic logic extends monadic second-order logic with the ability to measure the cardinal of sets. In particular, it allows to decide problems related to boundedness questions. In this paper, we provide new decidability results allowing the systematic investigation of questions involving “relative boundedness”. The first contribution in this work is to introduce a suitable logic for such questions. The second is to show the decidability of this logic over finite words. The third contribution is the use of non-standard analysis: we advacate that developing the proofs in the axiomatic system of “relative internal set theory” entails a significant simplification of the proofs.
• [CLKB13] , , , . “Deciding the weak definability of Büchi definable tree languages”. In: CSL 2013: 22nd Annual Conference on Computer Science Logic. 2013, pages 215–230. -pdf--
Abstract: Weakly definable languages of infinite trees are an expressive subclass of regular tree languages definable in terms of weak monadic second-order logic, or equivalently weak alternating automata. Our main result is that given a Büchi automaton, it is decidable whether the language is weakly definable. We also show that given a parity automaton, it is decidable whether the language is recognizable by a nondeterministic co-Büchi automaton. The decidability proofs build on recent results about cost automata over infinite trees. These automata use counters to define functions from infinite trees to the natural numbers extended with infinity. We reduce to testing whether the functions defined by certain ”quasi-weak” cost automata are bounded by a finite value.
• [Col13c] . “Fonctions Régulières de Coût”. Habilitation thesis, in french. PhD thesis. Université Paris Diderot — Paris VII, 2013. -pdf-slides--
Abstract: This thesis gives a broad picture of the theory of regular cost functions. Regular cost functions are quantitative extensions to regular languages. A cost function is a function from words (or trees. . .) to the non-negative integers or infinity. These functions are considered modulo an equivalence relation that allows some distortion of the exact values, but preserves the existence of bounds. Regular cost functions form a sub-class that admits many effectively equivalent charac- terisations in terms of logic, automata, algebra and regular expressions. Some decidability results are deduced. These results extend on the one hand the classical results on regular languages, and on the other hand the works of Hashiguchi, Simon, Leung, and Kirsten concerning distance automata, the tropical semiring and the star-height problem. This document describes the current knowledge about regular cost functions for finite words, infinite words, finite trees and infinite trees.
• [Col13d] . “Regular cost functions, Part I: logic and algebra over words”. In: Logical Methods in Computer Science 9.3 (2013), page 47. -pdf--
Abstract: The theory of regular cost functions is a quantitative extension to the classical notion of regularity. A cost function associates to each input a non-negative integer value (or infinity), as opposed to languages which only associate to each input the two values ‘inside’ and ‘outside’. This theory is a continuation of the work on distance automata and similar models. These models of automata have been successfully used for solving the star-height problem, the finite power property, the finite substitution problem, the relative inclusion star-height problem and the boundedness problem for monadic-second order logic over words. Our notion of regularity can be – as in the classical theory of regular languages – equivalently defined in terms of automata, expressions, algebraic recognisability, and by a variant of the monadic second-order logic. Those equivalences are strict extensions of the corresponding classical results. The present paper introduces the cost monadic logic, the quantitative extension to the notion of monadic second-order logic we use, and show that some problems of existence of bounds are decidable for this logic. This is achieved by introducing the corresponding algebraic formalism: stabilisation monoids.

# 2012

• [Col12] . “Forms of Determinism for Automata”. In: STACS 2012: 29th International Symposium on Theoretical Aspects of Computer Science. Edited by , . Volume 14. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pages 1–23. -pdf-slides--
Abstract: We survey in this paper some variants of the notion of determinism, refining the spectrum between non-determinism and determinism. We present unambiguous automata, strongly unambiguous automata, prophetic automata, guidable automata, and history-deterministic automata. We instantiate these various notions for finite words, infinite words, finite trees, infinite trees, data languages, and cost functions. The main results are underlined and some open problems proposed.

# 2011

• [Col11] . “Green’s Relations and their Use in Automata Theory”. In: LATA 2011: Language and Automata Theory and Applications - 5th International Conference. Edited by , , . Volume 6638. Lecture Notes in Computer Science. Invited lecture. Springer, 2011, pages 1–21. -pdf-slides--
Abstract: The objective of this survey is to present the ideal theory of monoids, the so-called Green’s relations, and to illustrate the usefulness of this tool for solving automata related questions. We use Green’s relations for proving four classical results related to automata theory: The result of Schutzenberger characterizing star-free languages, the theorem of factorization forests of Simon, the characterization of infinite words of decidable monadic theory due to Semenov, and the result of determinization of automata over infinite words of Mc-Naughton.
• [CLP11] , , . “On the Use of Guards for Logics with Data”. In: MFCS 2011: Mathematical Foundations of Computer Science. Edited by , . Volume 6907. Lecture Notes in Computer Science. Journal version in Logical Methods in Computer Science, 2015. Springer, 2011, pages 243–255. -pdf--
Abstract: The notion of orbit finite data monoid was recently introduced by Bojanczyk as an algebraic object for defining recognizable languages of data words. In this paper, following Buchi’s approach, we introduce the new logic ”rigidly guarded MSO” and show that the languages of data words definable in this logic are exactly the languages recognizable by orbit finite data monoids. We also establish, following this time the approach of Schutzenberger, McNaughton and Papert, that the first-order variant of this logic exactly defines the languages recognizable by aperiodic orbit finite data monoids.
• [CCP11] , , . “Regular Languages of Words over Countable Linear Orderings”. In: ICALP 2011 (2): Automata, Languages and Programming - 38th International Colloquium. Edited by , , . Volume 6756. Lecture Notes in Computer Science. Springer, 2011, pages 125–136. -pdf--
Abstract: We develop an algebraic model suitable for recognizing languages of words indexed by countable linear orderings. We prove that this notion of recognizability is effectively equivalent to definability in monadic second-order (MSO) logic. This reproves in particular the decidability of MSO logic over the rationals with order. Our proof also implies the first known collapse result for MSO logic over countable linear orderings.

# 2010

• [Col10] . “Factorisation Forests for Infinite Words and applications to countable scattered linear orderings”. In: Theoretical Computer Science 411 (4-5 2010). Selected papers of FCT 07, pages 751–764. -pdf--
Abstract: The theorem of factorization forests of Imre Simon shows the existence of nested factorizations — à la Ramsey — for finite words. This theorem has important applications in semigroup theory, and beyond. We provide two improvements to the standard result. First we improve on all previously known bounds. Second, we extend it to ‘every linear ordering’. We use this last variant in a simplified proof of the translation of recognisable languages over countable scattered linear orderings to languages accepted by automata.
• [CL10] , . “Regular cost functions over finite trees”. In: LICS 2010: 5th Annual IEEE Symposium on Logic in Computer Science. IEEE, 2010, pages 70–79. -pdf--
Abstract: We develop the theory of regular cost functions over finite trees: a quantitative extension to the notion of regular languages of trees: Cost functions map each input (tree) to a value in omega + 1, and are considered modulo an equivalence relation which forgets about specific values, but preserves boundedness of functions on all subsets of the domain. We introduce nondeterministic and alternating finite tree cost automata for describing cost functions. We show that all these forms of automata are effectively equivalent. We also provide decision procedures for them. Finally, follow- ing Büchi’s seminal idea, we use cost automata for provid- ing decision procedures for cost monadic logic, a quantita- tive extension of monadic second order logic.
• [CKL10] , , . “Regular Temporal Cost Functions”. In: ICALP 2010 (2): Automata, Languages and Programming, 37th International Colloquium. Edited by , , , , . Volume 6199. Lecture Notes in Computer Science. Springer, 2010, pages 563–574. -pdf--
Abstract: Regular cost functions have been introduced recently as an extension to the notion of regular languages with counting capabilities, which retains strong closure, equivalence, and decidability properties. The specificity of cost functions is that exact values are not considered, but only estimated. In this paper, we study the strict subclass of regular temporal cost functions. In such cost functions, it is only allowed to count the number of occurrences of consecutive events. For this reason, this model intends to measure the length of intervals, i.e., a discrete notion of time. We provide various equivalent representations for functions in this class, using automata, and ‘clock based’ reduction to regular language. We show that the conversions are much simpler to obtain, and much more efficient than in the general case of regular cost functions. Our second aim in this paper is to use temporal cost function as a test-case for exploring the algebraic nature of regular cost functions. Following the seminal ideas of Schutzenberger, this results in a decidable algebraic characterization of regular temporal cost functions inside the class of regular cost functions.

# 2009

• [CZ09] , . “A tight lower bound for determinization of transition labeled Büchi automata”. In: ICALP 2009 (2): Automata, Languages and Programming, 36th International Colloquium. Edited by , , , , . Volume 5556. Lecture Notes in Computer Science. Springer, 2009, pages 151–162. -pdf-slides--
Abstract: In this paper we establish a lower bound $\Omega \left(\left(1.64n\right)n\right)$ for the problem of translating a Büchi word automaton of size $n$ into a deterministic Rabin word automaton when both the Büchi and the Rabin condition label transitions rather than states. This lower bound exactly matches the known upper bound to this problem, namely $\Omega \left(\left(1.64n\right)n\right)$. Our result entails a lower bound when the input Büchi automaton has (as it is usual) its Büchi acceptance condition labeling states. Those lower bounds remain when the output deterministic Rabin automaton has its Rabin acceptance condition labeling states. Hence, in the standard setting, our result establishes a lower bound of $\Omega \left(\left(1.64n\right)n\right)$, while the best known lower bound was $\Omega \left(\left(0.76n\right)n\right)$. A known upper bound in the standard setting is $o\left(\left(2.66n\right)n\right)$.
• [Col09a] . “Regular cost functions over words (draft)”. This is a draft, not reviewed. All the algebra part can be found with a better presentation in the submitted ’Regular cost functions, Part I: logic and algebra over words’. 2009. -pdf--
Abstract: We introduce and develop the notion of regular cost functions: a quantitative extension to the standard theory of regular languages. This work is a continuation of the works on distance automata and similar models. These models of automata have been successfully used for solving the star-height problem, the finite power property, the finite substitution problem, the relative inclusion star-height problem or the boundedness problem for monadic-second order logic over words. Our notion of regularity can be – as in the classical theory of regular languages – equivalently defined in terms of automata, of algebraic recognisability, and by a variant of the monadic second-order logic. Those equivalences are strict extensions of the corresponding classical results. The decidability of the limitedness problem of distance automata, as well as all its known variants can be deduced from our results.
• [Col09b] . “The theory of stabilisation monoids and regular cost functions”. In: ICALP 2009 (2): Automata, Languages and Programming, 36th International Colloquium. Edited by , , , , . Volume 5556. Lecture Notes in Computer Science. Springer, 2009, pages 139–150. -pdf-slides--
Abstract: We introduce the notion of regular cost functions: a quantitative extension to the standard theory of regular languages. We provide equivalent characterisations of this notion by means of automata (extending the nested distance desert automata of Kirsten), of history-deterministic automata (history-determinism is a weakening of the standard notion of determinism, that replaces it in this context), and a suitable notion of recognisability by stabilisation monoids. We also provide closure and decidability results.

# 2008

• [BCL08] , , . “Logical theories and compatible operations”. In: Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas]. Edited by , , . Volume 2. Texts in Logic and Games. Amsterdam University Press, 2008, pages 73–106. --
Abstract: We survey operations on (possibly infinite) relational structures that are compatible with logical theories in the sense that, if we apply the operation to given structures then we can compute the theory of the resulting structure from the theories of the arguments (the logics under consideration for the result and the arguments might differ). Besides general compatibility results for these operations we also present several results on restricted classes of structures, and their use for obtaining classes of infinite structures with decidable theories.
• [CL08a] , . “The nesting-depth of disjunctive $\mu$-calculus for tree languages and the limitedness problem”. In: CSL 2008: 17th EACSL Annual Conference on Computer Science Logic. Edited by , . Volume 5213. Lecture Notes in Computer Science. Springer, 2008, pages 416–430. -pdf--
Abstract: This chapter is devoted to the presentation of the factorisation forest theorem, a deep result due to Simon, which provides advanced Ramsey-like arguments in the context of algebra, au- tomata, and logic. We present several proofs and several variants the result, as well as applications.
• [CL08b] , . “The non-deterministic Mostowski hierarchy and distance-parity automata”. In: ICALP 2008 (2): Automata, Languages and Programming, 35th International Colloquium. Edited by , , , , , . Volume 5126. Lecture Notes in Computer Science. Springer, 2008, pages 398–409. -pdf--
Abstract: Given a Rabin tree-language and natural numbers i, j, the language is said to be i,j-feasible if it is accepted by a parity automaton using priorities i,i+1,...,j. The i,j-feasibility induces a hierarchy over the Rabin-tree languages called the Mostowski hierarchy. In this paper we prove that the problem of deciding if a language is i,j-feasible is reducible to the uniform universality problem for distanceparity automata. Distance-parity automata form a new model of automata extending both the nested distance desert automata introduced by Kirsten in his proof of decidability of the star-height problem, and parity automata over infinite trees. Distance-parity automata, instead of accepting a language, attach to each tree a cost in omega+1. The uniform universality problem consists in determining if this cost function is bounded by a finite value.
• [BC08] , . “Tree-walking automata do not recognize all regular languages”. In: SIAM J. Comput. 38.2 (2008), pages 658–701. --
Abstract: Tree-walking automata are a natural sequential model for recognizing tree languages. It is well known that every tree language recognized by a tree-walking automaton is regular. We show that the converse does not hold.

# 2007

• [Col07a] . “A combinatorial theorem for trees: applications to monadic logic and infinite structures”. In: ICALP 2007: Automata, Languages and Programming, 34th International Colloquium. Edited by , , , . Volume 4596. Lecture Notes in Computer Science. Springer, 2007, pages 901–912. -pdf--
Abstract: Following the idea developed by I. Simon in his theorem of Ramseyan factorisation forests, we develop a result of ‘deterministic factorisations’. This extra determinism property makes it usable on trees (finite or infinite). We apply our result for proving that, over trees, every monadic interpretation is equivalent to the composition of a first-order interpretation (with access to the ancestor relation) and a monadic marking. Using this remark, we give new characterisations for prefix-recognisable structures and for the Caucal hierarchy. Furthermore, we believe that this approach has other potential applications.
• [Col07b] . “Factorisation forests for infinite words”. In: FCT 2007: Fundamentals of Computation Theory, 16th International Symposium. Edited by , . Volume 4639. Lecture Notes in Computer Science. Springer, 2007, pages 226–237. -pdf--
Abstract: The theorem of factorisation forests shows the existence of nested factorisations — a la Ramsey — for finite words. This theorem has important applications in semigroup theory, and beyond. We provide two improvements to the standard result. First we improve on all previously known bounds for the standard theorem. Second, we extend it to every ‘complete linear ordering’. We use this variant in a simplified proof of complementation of automata over words of countable scattered domain.
• [Col07c] . On Factorization Forests. Technical report hal-00125047. Irisa Rennes, 2007. -pdf--
Abstract: The theorem of factorisation forests shows the existence of nested factorisations — a la Ramsey — for finite words. This theorem has important applications in semigroup theory, and beyond. The purpose of this paper is to illustrate the importance of this approach in the context of automata over infinite words and trees. We extend the theorem of factorisation forest in two directions: we show that it is still valid for any word indexed by a linear ordering; and we show that it admits a deterministic variant for words indexed by well-orderings. A byproduct of this work is also an improvement on the known bounds for the original result. We apply the first variant for giving a simplified proof of the closure under complementation of rational sets of words indexed by countable scattered linear orderings. We apply the second variant in the analysis of monadic second-order logic over trees, yielding new results on monadic interpretations over trees. Consequences of it are new caracterisations of prefix-recognizable structures and of the Caucal hierarchy.
• [CL07] , . “Transforming structures by set interpretations”. In: Logical Methods in Computer Science 3.2 (2007), 2:4, 36 pp. (electronic). -pdf--
Abstract: We consider a new kind of interpretation over relational structures: finite sets interpretations. Those interpretations are defined by weak monadic second-order (WMSO) formulas with free set variables. They transform a given structure into a structure with a domain consisting of finite sets of elements of the orignal structure. The definition of these interpretations directly implies that they send structures with a decidable WMSO theory to structures with a decidable first-order theory. In this paper, we investigate the expressive power of such interpretations applied to infinite deterministic trees. The results can be used in the study of automatic and tree-automatic structures.

# 2006

• [BC06a] , . “Bounds in $\omega$-regularity”. In: LICS 06: 21th IEEE Symposium on Logic in Computer Science. IEEE, 2006, pages 285–296. -pdf--
Abstract: We consider an extension of $\omega$-regular expressions where two new variants of the Kleene star $L*$ are added: $LB$ and $LS$. These exponents act as the standard star, but restrict the number of iterations to be bounded (for $LB$) or to tend toward infinity (for $LS$). These expressions can define languages that are not omega-regular. We develop a theory for these languages. We study the decidability and closure questions. We also define an equivalent automaton model, extending Büchi automata. This culminates with a — partial — complementation result.
• [CN06] , . “On the positional determinacy of edge-labeled games”. In: Theoretical Computer Science 352.1-3 (2006), pages 190–196. -pdf--
Abstract: It is well known that games with the parity winning condition admit positional determinacy : the winner has always a positional (memoryless) strategy. This property continues to hold if edges rather than vertices are labeled. We show that in this latter case the converse is also true. That is, a winning condition over arbitrary set of colors admits positional determinacy in all games if and only if it can be reduced to a parity condition with some finite number of priorities.
• [CL06] , . Transforming structures by set interpretations. Technical report AIB-2006-07. RWTH Aachen, 2006. -pdf--
Abstract: We consider a new kind of interpretation over relational structures: finite sets interpretations. Those interpretations are defined by weak monadic second-order (WMSO) formulas with free set variables. They transform a given structure into a structure with a domain consisting of finite sets of elements of the orignal structure. The definition of these interpretations directly implies that they send structures with a decidable WMSO theory to structures with a decidable first-order theory. In this paper, we investigate the expressive power of such interpretations applied to infinite deterministic trees. The results can be used in the study of automatic and tree-automatic structures.
• [BC06b] , . “Tree-walking automata cannot be determinized”. In: Theoretical Computer Science 350.2-3 (2006), pages 164–173. -pdf--
Abstract: Tree-walking automata are a natural sequential model for recognizing languages of finite trees. Such automata walk around the tree and may decide in the end to accept it. It is shown that deterministic tree-walking automata are weaker than nondeterministic tree-walking automata.

# 2005

• [BC05] , . “Tree-walking automata do not recognize all regular languages”. In: STOC 2005: 37th Annual ACM Symposium on Theory of Computing. ACM, 2005, pages 234–243. -pdf--
Abstract: Tree-walking automata are a natural sequential model for recognizing tree languages. Every tree language recognized by a tree-walking automaton is regular. In this paper, we present a tree language which is regular but not recognized by any (nondeterministic) tree-walking automaton. This settles a conjecture of Engelfriet, Hoogeboom and Van Best. Moreover, the separating tree language is definable already in first-order logic over a signature containing the left-son, right-son and ancestor relations.

# 2004

• [Col04a] . “Propriétés et représentation de structures infinies (properties and representation of infinite structures)”. PhD thesis. Université Rennes I, Mar. 2004. -pdf--
Abstract: This work is dedicated to the study of infinite structures and graphs which admit a finite representation, to their geometrical properties as well as decidability properties concerning them. Following Courcelle’s work, we focus our study on their representation as solution of equational systems. We first introduce deterministic transducers (top-down with lookahead for infinite trees). This tool allows us to deal with infinite equational systems, thus extending some previous results, originally stated for finite equational systems. We then study the stack based families of structures and concentrate ourselves on prefix recognizable ones. We establish various equivalent representations for them, and study their restriction to bounded tree-width. We finally consider the enrichment of those equational systems by an extra operator of fusion. We then study structures admitting term-automatic presentations. We show once more that those structures admit various equivalent representations. Finally, we study the family of graphs definable by ground term rewriting and establish some equivalences of representations. We conclude by a study of the nature of those graphs when restricted to bounded tree or clique width.
• [Col04b] . “Equational presentations of tree-automatic structures”. In: WASL 04. 2004. -pdf--.
• [CL04] , . “On the expressiveness of deterministic transducers over infinite trees”. In: STACS 2004: 21st International Symposium on Theoretical Aspects of Computer Science. Edited by , . Volume 2996. Lecture Notes in Computer Science. Springer, 2004, pages 428–439. -pdf--
Abstract: We introduce top-down deterministic transducers with rational lookahead (transducer for short) working on infinite terms. We show that for such a transducer $\stackrel{̃}{T}$, there exists an MSO-transduction $T$ such that for any graph $G$, $\mathit{unfold}\left(T\left(G\right)\right)=\stackrel{̃}{T}\left(\mathit{unfold}\left(G\right)\right)$. Reciprocally, we show that if an MSO-transduction $T$ “preserves bisimilarity”, then there is a transducer $\stackrel{̃}{T}$ such that for any graph $G$, $\mathit{unfold}\left(T\left(G\right)\right)=\stackrel{̃}{T}\left(\mathit{unfold}\left(G\right)\right)$. According to this, transducers can be seen as a complete method of implementation of MSO-transductions that preserve bisimilarity. One application is for transformations of equational systems.
• [BC04] , . “Tree-walking automata cannot be determinized”. In: ICALP 2004: Automata, Languages and Programming: 31st International Colloquium. Edited by , , , . Volume 3142. Lecture Notes in Computer Science. Springer, 2004, pages 246–256. -pdf--
Abstract: Tree-walking automata are a natural sequential model for recognizing tree languages. It is shown that deterministic tree-walking automata are weaker than nondeterministic tree-walking automata.

# 2003

• [CC03] , . “On equivalent representations of infinite structures”. In: ICALP 2003: Automata, Languages and Programming, 30th International Colloquium. Edited by , , , . Volume 2719. Lecture Notes in Comput. Sci. Springer, 2003, pages 599–610. -pdf--
Abstract: According to Barthelman and Blumensath, the following families of infinite graphs are isomorphic: (1) prefix-recognisable graphs, (2) graph solutions of VR equational systems and (3) MS interpretations of regular trees. In this paper, we consider the extension of prefix-recognisable graphs to prefix-recognisable structures and of graphs solutions of VR equational systems to structures solutions of positive quantifier free definable (PQFD) equational systems. We extend Barthelman and Blumensath’s result to structures parameterised by infinite graphs by proving that the following families of structures are equivalent: (1) prefix-recognisable structures restricted by a language accepted by an infinite deterministic automaton, (2) solutions of infinite PQFD equational systems and (3) MS interpretations of the unfoldings of infinite deterministic graphs. Furthermore, we show that the addition of a fuse operator, that merges several vertices together, to PQFD equational systems does not increase their expressive power.

# 2002

• [Col02a] . “On Families of Graphs Having a Decidable First Order Theory with Reachability”. In: Automata, Languages and Programming, 29th International Colloquium, ICALP 2002. Edited by , , , , , . Volume 2380. Lecture Notes in Computer Science 2380. Malaga: Springer, 2002, pages 98–109. -pdf--
Abstract: We consider a new class of infinite graphs defined as the smallest solution of equational systems with vertex replacement operators and unsynchronised product. We show that those graphs have an equivalent internal representation as graphs of recognizable ground term rewriting systems. Furthermore, we show that, when restricted to bounded tree-width, those graphs are isomorphic to hyperedge replacement equational graphs. Finally, we prove that on a wider family of graphs — interpretations of trees having a decidable monadic theory — the first order theory with reachability is decidable.
• [Col02b] . “Rewriting in the partial algebra of typed terms modulo AC”. In: Electronic Notes in Theoretical Computer Science 68.6 (2002). Edited by , . -pdf--
Abstract: We study the partial algebra of typed terms with an associative commutative and idempotent operator (typed AC-terms). The originality lies in the representation of the typing policy by a graph which has a decidable monadic theory. In this paper we show on two examples that some results on AC-terms can be raised to the level of typed AC-terms. The examples are the results on rational languages (in particular their closure by complement) and the property reachability problem for ground rewrite systems (equivalently process rewrite systems).

# 2000

• [CF00] , . “Enforcing Trace Properties by Program Transformation”. In: POPL 00: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Edited by , . ACM, 2000, pages 54–66. -pdf--
Abstract: We propose an automatic method to enforce trace properties on programs. The programmer specifies the property separately from the program; a program transformer takes the program and the property and automatically produces another “equivalent” pogram satisfying the property. This separation of concerns makes the program easier to develop and maintain. Our approach is both static and dynamic. It integrates static analyses in order to avoid useless transformations. On the other hand, it never rejects programs but adds dynamic checks when necessary. An important challenge is to make this dynamic enforcement as inexpensive as possible. The most obvious application domain is the enforcement of security policies. In particular, a potential use of the method is the securization of mobile code upon receipt.