Some Selected Publications (Since 2007)

Interactive Music Transcription based on Rhythm Tree Languages.
Florent Jacquemard and Adrien Ycart.
16th Rhythm Production and Perception Workshop (RPPW 2017), Birmingham, United Kingdom.
bibTeX | abstract We consider symbolic rhythm transcription, also called quantization: the problem of the conversion of a sequence of timestamped notes, e.g. a MIDI file, into conventional Western music notation. The fitness of a notation to a given a MIDI input is an intrinsically ambiguous notion, as it depends strongly on the the musical context. We propose a system available as a graphical component of the assisted composition environment OpenMusic, which privileges user interactions in order to search for an appropriate balance between different criteria, in particular the precision of the transcription and the readability of the musical scores produced. For the development of this system, we followed a uniform approach based on a set of preferred rhythm notations, specified a priori as a formal weighted tree language. Using efficient dynamic programming algorithms, we propose a on-the-fly enumeration of ranked solutions of quantization in this language, allow the user to explore and visualize the solution space, select rhythms and edit them.

Generating equivalent rhythmic notations based on rhythm tree languages.
Florent Jacquemard and Adrien Ycart and Masahiko Sakai.
Third International Conference on Technologies for Music Notation and Representation (TENOR 2017).
bibTeX | pdf | abstract We propose a compact presentation of languages of preferred rhythms notation as formal grammars. It is based on a standard structure of rhythm trees capturing a wide range of rhythms in Western notation. As an application, we then describe a dynamic programming algorithm for the lazy enumeration of equivalent rhythm notations (i.e. notations defining the same durations), from the simplest to the most complex. This procedure, based on the notion of rhythm grammars has been implemented and may be useful in the context of automated music transcription and computer-assistance to composition.

One-Variable Context-Free Hedge Automata.
Florent Jacquemard and Michael Rusinowitch.
Journal of Computer and System Sciences, in press 2016.
bibTeX | pdf | DOI: 10.1016/j.jcss.2016.10.006 | abstract We introduce an extension of hedge automata called One-Variable Context-Free Hedge Automata. The class of unranked ordered tree languages they recognize has polynomial membership problem and is preserved by rewrite closure with inverse-monadic rules. We also propose a modeling of primitives of the W3C XQuery Update Facility by mean of parameterized rewriting rules, and show that the rewrite closure of a context-free hedge language with these extended rewriting systems is a context-free hedge language. This result is applied to static analysis of XML access control policies expressed with update primitives.

Some results on confluence: decision and what to do without.
Florent Jacquemard.
5th International Workshop on Confluence (invited talk) 2016.
bibTex | pdf | slides | abstract We recall first some decidability results on the confluence of TRS, and related prop- erties about unicity of normal forms. In particular we put it in perspective old proofs of undecidability of confluence for the class of flat systems with more recent results, in order to discuss the importance of linearity wrt these decision problems. Second, we describe a case study on musical rhythm notation involving modeling rewrite systems which are not confluent. In this case, instead of applying rewrite rules directly, we enumerate the equivalence class of a given term using automata-based representations and dynamic programming.

Model-Based Testing for Building Reliable Realtime Interactive Music Systems.
Clement Poncelet and Florent Jacquemard.
Science of Computer Programming 132(2) pages 143–172. Elsevier, 2016.
bibTeX | pdf | DOI:10.1016/j.scico.2016.08.002 | abstract The role of an Interactive Music System (IMS) is to accompany musicians during live performances, acting like a real musician. It must react in realtime to audio signals from musicians, according to a timed high-level requirement called mixed score, written in a domain specific language. Such goals imply strong requirements of temporal reliability and robustness to unforeseen errors in input, yet not much addressed by the computer music community. We present the application of Model-Based Testing techniques and tools to a state-of-the-art IMS, including in particular: offline and on-the-fly approaches for the generation of relevant input data for testing (including timing values), with coverage criteria, the computation of the corresponding expected output, according to the semantics of a given mixed score, the black-box execution of the test data on the System Under Test and the production of a verdict. Our method is based on formal models in a dedicated intermediate representation, compiled directly from mixed scores (high-level requirements), and either passed, to the model-checker Uppaal (after conversion to Timed Automata) in the offline approach, or executed by a virtual machine in the online approach. Our fully automatic framework has been applied to real mixed scores used in concerts and the results obtained have permitted to identify bugs in the target IMS.

A Supervised Approach for Rhythm Transcription Based on Tree Series Enumeration.
Adrien Ycart, Florent Jacquemard, Jean Bresson and Slawomir Staworko.
Proceedings of the 42nd International Computer Music Conference (ICMC'16), Utrecht, Netherlands, Sept 2016.
bibTeX | pdf | abstract We present a rhythm transcription system integrated in the computer-assisted composition environment OpenMusic. Rhythm transcription consists in translating a series of dated events into traditional music notation's pulsed and structured representation. As transcription is equivocal, our system favors interactions with the user to reach a satisfactory compromise between various criteria, in particular the precision of the transcription and the readability of the output score. It is based on a uniform approach, using a hierarchical representation of duration notation in the form of rhythm trees, and an efficient dynamic-programming algorithm that lazily evaluates the transcription solutions. It is run through a dedicated user interface allowing to interactively explore the solution set, visualize the solutions and locally edit them.

An Automatic Test Framework for Interactive Music Systems.
Clement Poncelet and Florent Jacquemard.
Journal of New Music Research, Volume 45, issue 2, 2016.
bibTex | pdf | JNMR link | abstract Score-Based Interactive Music Systems are involved in live performances with human musicians, reacting in realtime to audio signals and asynchronous incoming events according to a pre-specified timed scenario called mixed score. Building such a system is a difficult challenge implying strong requirements of reliability and robustness to unforeseen errors in input. We present the application to an automatic accompaniment system of formal methods for conformance testing of critical embedded systems. Our approach is fully automatic and based on formal models constructed directly from mixed scores, specifying the behavior expected from the system when playing with musicians. It has been applied to real mixed scores and the results obtained have permitted to identify bugs in the tested system.

Une approche interactive pour la transcription rythmique dans OpenMusic.
Adrien Ycart, Jean Bresson, Florent Jacquemard, Sławek Staworko.
Journées d'Informatique Musicale (JIM'16), Albi, France. Mar 2016.
bibTeX | pdf

FO2(<, +1, ~) on data trees, data tree automata and branching vector addition systems.
Florent Jacquemard and Luc Segoufin and Jerémie Dimino.
Logical Methods in Computer Science, 12(2) 2016.
bibTeX | pdf | LMCS link | DOI:10.2168/LMCS-12(2:3)2016 | HAL | abstractA data tree is an unranked ordered tree where each node carries a label from a finite alphabet and a datum from some infinite domain. We consider the two variable first order logic FO2(<,+1,~) over data trees. Here +1 refers to the child and the next sibling relations while < refers to the descendant and following sibling relations. Moreover, ~ is a binary predicate testing data equality. We exhibit an automata model, denoted DAD# that is more expressive than FO2(<,+1,~) but such that emptiness of DAD# and satisfiability of FO2(<,+1,~) are inter-reducible. This is proved via a model of counter tree automata, denoted EBVASS, that extends Branching Vector Addition Systems with States (BVASS) with extra features for merging counters. We show that, as decision problems, reachability for EBVASS, satisfiability of FO2(<,+1,~) and emptiness of DAD# are equivalent.

A Structural Theory of Rhythm Notation based on Tree Representations and Term Rewriting.
Florent Jacquemard, Pierre Donat-Bouillud, Jean Bresson.
5th International Conference on Mathematics and Computation in Music (MCM). Lecture Notes in Artificial Intelligence vol. 9110, Springer, 2015.
bibTeX | pdf | slides | Springer's link | abstract We present a tree-based symbolic representation of rhythm notation suitable for processing with purely syntactic theoretical tools such as term rewriting systems or tree automata. Then we propose an equational theory, defined as a set of rewrite rules for transforming these representations. This theory is complete in the sense that from a given rhythm notation the rules permit to generate all notations of equivalent durations.

Towards an Equational Theory of Rhythm Notation.
Pierre Donat-Bouillud, Florent Jacquemard, Masahiko Sakai.
Music Encoding Conference, 2015.
bibTex | pdf | abstract Trees are classical representations of hierarchical structures in symbolic music, in particular for rhythm notations, where the durations are defined by a hierarchy of subdivisions. Structures called rhythm trees have been integrated since a long time into Computer Aided Composition environments such as Patchwork and OpenMusic , for programming rhythmic objects. Term rewriting and tree automata and transducers are well established formalisms for transforming and reasoning on trees. With solid theoretical foundations, they are used in a wide range of applications including automatic reasoning, natural language processing, and foundations of web data processing. In this work, we consider a tree structured representation of rhythm suitable for defining a set of rewrite rules (i.e. oriented equations) preserving rhythms, while enabling the simplification of notations. This set can be seen as an axiomatization of rhythm notation which can be applied to reasoning on equivalent notations in assisted composition.

Model Based Testing of an Interactive Music System.
Clément Poncelet, Florent Jacquemard.
Proceedings of the 30th ACM/SIGAPP Symposium On Applied Computing (ACM SAC), track SVT. ACM, 2015.
bibTex | pdf | DOI:10.1145/2695664.2695804 | abstractThe role of an interactive music system (IMS) is to accom-pany musicians during live performances, like a real musi-cian. It reacts in realtime to audio signals from musicians, according to a timed specification called mixed score, writ-ten in a domain specific language. Such goals imply strong requirements of temporal reliability and robustness to un-foreseen errors in input, yet not so much studied in the computer music community. We present the application of model-based testing tech-niques and tools to a state-of-the-art IMS, including the fol-lowing tasks: generation of relevant input data for testing (including timing values) following coverage criteria, com-putation of the corresponding expected output, according to the semantics of a given mixed score, black-box execution of the test data and verdict. Our method is based on formal models compiled directly from mixed scores, and passed, after conversion to timed automata, to the model-checker Uppaal. This fully automatic approach has been applied to real mixed scores used in concerts and the results obtained have permitted to identify bugs in the target IMS.

Term Rewriting with Prefix Context Constraints and Bottom-Up Strategies.
Florent Jacquemard, Yoshiharu Kojima, Masahiko Sakai.
Proceedings of the 25th International Conference on Automated Deduction (CADE’15), Springer's LNAI vol. 9195. 2015.
bibTex | pdf | slides | abstract We consider the extension of term rewriting rules with context constraints restricting the application of rewriting to positions whose prefix (i.e. the sequence of symbols from the rewrite position up to the root) belongs to a given regular language. This approach, well studied in the case of string rewriting, is similar to node selection mechanisms in XML transformation languages, and also generalizes the context-sensitive rewriting. The systems defined this way are called prefix constrained TRS (pCTRS), and we study the decidability of reachability of regular tree model checking and the preservation of regularity for some subclasses. The two latter properties hold for linear and right-shallow standard TRS but not any-more when adding context constraints. We show that these properties can be restored by restricting derivations to bottom-up ones, and moreover that it implies that left-linear and right-ground pCTRS preserve regularity and have a decidable regular model checking problem.

Projet EFFICACE : Développements et perspectives en composition assistée par ordinateur.
Jean Bresson, Dimitri Bouche, Jérémie Garcia, Thibaut Carpentier, Florent Jacquemard, John Maccallum, Diemo Schwarz. Journées d'Informatique Musicale, 2015.
bibTex | pdf | abstract EFFICACe est un projet de recherche centré sur les outils de composition assistée par ordinateur (CAO), explorant les rapports entre calcul, temps et interactions dans les processus de composition musicale. Nous présentons différents travaux en cours dans le cadre de ce projet, concernant l'application de processus interactifs pour le traitement et l'ordonnancement des séquences temporelles, le traitement et la spatialisation sonore, ou encore les interfaces homme-machine.

Test Methods for Score-Based Interactive Music Systems.
Clément Poncelet Sanchez, Florent Jacquemard. International Computer Music Conference, 2014.
bibTex | pdf | abstract Score-Based Interactive Music Systems (SBIMS) are involved in live performances with human musicians, reacting in realtime to audio signals and asynchronous incoming events according to a pre-specified timed scenario called a mixed score. This implies strong requirements of reliability and robustness to unforeseen errors in input. In this paper, we present the application of formal methods for black-box conformance testing of embedded systems to SBIMS's. We describe how we have handled the 3 main problems in automatic testing reactive and realtime software like SBIMS: (i) the generation of relevant input data for testing, including delay values, with the sake of exhaustiveness, (ii) the computation of the corresponding expected output, according to a given mixed score, (iii) the test execution on input and verdict. The results obtained from this formal test method have permitted to identify bugs in the SBIMS Antescofo.

Rhythm Tree Rewriting.
Florent Jacquemard, Jean Bresson, Pierre Donat-Bouillud.
Meeting of the IFIP WG 1.6 on Term Rewriting (invited talk). 2014.
bibTex | abstract | slides | abstract In traditional western music notation, the durations of notes are expressed hier-archically by recursive subdivisions. This led naturally to a tree representation of melodies widespread in systems for assistance to music authoring. We will see how term rewriting techniques can be applied to computer music problems, in particular to the problem of rhythm quantization: the transcription of a sequence of dates (real time values) into a music score. Besides the question of rhythm representation, an interesting problem in this context is the design and concise description of large rewrite rule sets and decision problems for these descriptions.

Antescofo Intermediate Representation.
Florent Jacquemard, Clément Poncelet Sanchez. INRIA Research Report RR-8520, 2014.
bibTex | pdf | abstract We describe an intermediate language designed as a medium-level internal representation of programs of the interactive music system Antescofo. This representation is independent both of the Antescofo source language and of the architecture of the execution platform. It is used in tasks such as verification of timings, model-based conformance testing, static control-flow analysis or simulation. This language is essentially a flat representation of Antescofo's code, as a finite state machine extended with local and global variables, with delays and with concurrent threads creation. It features a small number of simple instructions which are either blocking (wait for external event, signal or duration) or not (variable assignment, message emission and control).

Operational semantics of a domain specific language for real time musician-computer interaction.
José Echeveste, Arshia Cont, Jean-Louis Giavitto, Florent Jacquemard.
Journal of Discrete Event Dynamic Systems 23(4), Springer. 2013.
bibTeX | pdf | DOI 10.1007/s10626-013-0166-2 | abstract With the advent and availability of powerful personal computing, the computer music research and industry have been focusing on real-time musical interactions between musicians and computers; delegating human-like actions to computers who interact with a musical environment. One common use-case of this kind is Automatic Accompaniment where the system is comprised of a real-time machine listening system that in reaction to recognition of events in a score from a human performer, launches necessary actions for the accompaniment section. While the real-time detection of score events out of live musicians' performance has been widely addressed in the literature, score accompaniment (or the reactive part of the process) has been rarely discussed. This paper deals with this missing component in the literature from a formal language perspective. We show how language considerations would enable better authoring of time and interaction during programming/composing and how it addresses critical aspects of a musical performance (such as errors) in real-time. We sketch the real-time features required by automatic musical accompaniment seen as a reactive system. We formalize the timing strategies for musical events taking into account the various temporal scales used in music. Various strategies for the handling of synchronization constraints and the handling of errors are presented. We give a formal semantics to model the possible behaviors of the system in terms of Parametric Timed Automata.

Decidable Classes of Tree Automata Mixing Local and Global Constraints Modulo Flat Theories.
Luis Barguño, Carlos Creus, Guillem, Godoy, Florent Jacquemard, Camille Vacher.
Logical Methods in Computer Science 9(2). IfCoLog 2013.
bibTex | pdf | abstract We define a class of ranked tree automata TABG generalizing both the tree automata with local brother tests of Bogaert and Tison (1992) and with global equality and disequality constraints (TAGED) of Filiot et al. (2007). TABG can test for equality and disequality modulo a given flat equational theory between brother subterms and between subterms whose positions are defined by the states reached during a computation. In particular, TABG can check that all the subterms reaching a given state are distinct. This constraint is related to monadic key constraints for XML documents, meaning that every two distinct positions of a given type have different values. We prove decidability of the emptiness problem for TABG. This solves, in particular, the open question of decidability of emptiness for TAGED. We further extend our result by allowing global arithmetic constraints for counting the number of occurrences of some state or the number of different equivalence classes of subterms (modulo a given flat equational theory) reaching some state during a computation. We also adapt the model to unranked ordered terms. As a consequence of our results for TABG, we prove the decidability of a fragment of the monadic second order logic on trees extended with predicates for equality and disequality between subtrees, and cardinality.

Unranked tree rewriting and effective closures of languages.
Florent Jacquemard, Michaël Rusinowitch.
Meeting of the IFIP WG 1.6 on Term Rewriting (invited talk). 2013.
bibTex | abstract | slides | abstract We consider rewriting systems for unranked ordered trees, where the number of children of a node is not determined by its label, and is not a priori bounded. The rewriting systems are defined such that variables in the rewrite rules can be substituted by hedges (sequences of trees) instead of just trees. Consequently, this notion of rewriting subsumes both standard term rewriting and word rewriting. We present some properties of preservation for classes of unranked tree languages, including hedge automata languages and various context-free extensions. Finally, applications to static type checking for XML transformations and to the verification of read/write access control policies for XML updates are mentioned.

A Synchronous Embedding of Antescofo, a Domain-Specific Language for Interactive Mixed Music.
Guillaume Baudart, Louis Mandel, Florent Jacquemard, Marc Pouzet.
13th International Conference on Embedded Software (EMSOFT) 2013.
bibTeX | pdf | code and demos | abstract Antescofo is recently developed software for musical score following and mixed music: it automatically, and in real-time, synchronizes electronic instruments with a musician playing on a classical instrument. Therefore, it faces some of the same major challenges as embedded systems. The system provides a programming language used by composers to specify musical pieces that mix interacting electronic and classical instruments. This language is developed with and for musicians and it continues to evolve according to their needs. Yet its semantics has only recently been formally defined. This paper presents a synchronous semantics for the core language of Antescofo and an alternative implementation based on an embedding inside an existing synchronous language, namely ReactiveML. The semantics reduces to a few rules, is mathematically precise and leads to an interpretor of only a few hundred lines. The efficiency of this interpretor compares well with that of the actual implementation: on all musical pieces we have tested, response times have been less than the reaction time of the human ear. Moreover, this embedding permitted the prototyping of several new programming constructs, some of which are described in this paper.

From Authored to Produced Time in Computer-Musician Interactions.
Arshia Cont, Jean-Louis Giavitto, Florent Jacquemard.
ACM CHI Workshop on Avec le Temps! Time, Tempo, and Turns in Human-Computer Interaction (2013).
bibTeX | pdf | abstract Human musicians have since long developed methods and formalisms for ensemble authoring and real-time coordination and synchronization of their actions. Bringing such capabilities to computers and providing them with the ability to take part in musical interactions with human musicians, poses interesting challenges for authoring of time and interaction and real-time coordination that we address in this paper in the context of Mixed Music and the Antescofo project.

Formal Timing Analysis Of Mixed Music Scores.
Léa Fanchon, Florent Jacquemard.
International Computer Music Conference (ICMC) 2013.
bibTeX | pdf | slides | abstract Interactive music systems coordinate in real-time an artificial perception of dynamics of human musicians with timely execution of machine reactions. As every human performance will differ from another, it is a challenging task to be able to predict the behavior or such systems in response to any possible performance, and prevent unwanted outcomes. We present here the application of formal models and methods from the real-time systems verification literature to the static analysis of interactive music systems. We consider in particular the good parameters problem, which consists in synthesizing a set of timing parameter valuations (representing performances here) guarantying a good behavior of the system analyzed. The methods presented have been applied to the system Antescofo, and are general enough to apply to other interactive music systems.

Rewrite Closure and CF Hedge Automata.
Florent Jacquemard and Michael Rusinowitch.
7th International Conference on Language and Automata Theory and Application (LATA). Bilbao, Spain. Lecture Notes in Computer Science, Springer. 2013.
bibTeX | pdf | slides | abstract We introduce an extension of hedge automata called bidimensional context-free hedge automata. The class of unranked ordered tree languages they recognize is shown to be preserved by rewrite closure with inverse-monadic rules. We also extend the parameterized rewriting rules used for modeling the W3C XQuery Update Facility in previous works, by the possibility to insert a new parent node above a given node. We show that the rewrite closure of hedge automata languages with these extended rewriting systems are context-free hedge languages.

Correct Automatic Accompaniment Despite Machine Listening or Human Errors in Antescofo.
Arshia Cont, José Echeveste, Jean-Louis Giavitto, Florent Jacquemard.
International Computer Music Conference (ICMC) 2012.
bibTeX | pdf | abstract Automatic accompaniment systems are comprised of realtime score following systems that in reaction to recognition of events in a score from a human performer, launch necessary actions for the accompaniment section. While the realtime detection of score events out of live musicians' performance has been widely studied in the literature, score accompaniment (or the reactive part of the process) has been rarely addressed. In this paper, we expose the respective literature concerning this missing consideration. We show how its explicit design considerations would allow correct accompaniment despite machine listening or human errors introduced during score following, and furthermore how it enables a more elaborate authoring of time and interaction for mixed live electronic pieces.

Sufficient Completeness Verification for Conditional and Constrained Term Rewriting Systems.
Adel Bouhoula, Florent Jacquemard.
Journal of Applied Logic, 10(1):127 – 143, Elsevier, 2012.
bibTeX | pdf | DOI:10.1016/j.jal.2011.09.001 | abstract We present a procedure for checking sufficient completeness of conditional and constrained term rewriting systems containing axioms for constructors which may be constrained (by e.g. equalities, disequalities, ordering, membership…). Such axioms allow to specify complex data structures like e.g. sets, sorted lists or powerlists. Our approach is integrated into a framework for inductive theorem proving based on tree grammars with constraints, a formalism which permits an exact representation of languages of ground constructor terms in normal form. The procedure is presented by an inference system which is shown sound and complete. A precondition of one inference of this system refers to a (undecidable) property called strong ground reducibility which is discharged to the above inductive theorem proving system. We have successfully applied our method to several examples, yielding readable proofs and, in case of negative answer, a counter-example suggesting how to complete the specification. Moreover, we show that it is a decision procedure when the TRS is unconditional but constrained, for an expressive class of constrained constructor axioms.

Rigid Tree Automata and Applications.
Florent Jacquemard, Francis Klay, Camille Vacher.
Information and Computation, Elsevier, 2011, 209 (3), pages 486-512.
bibTeX | pdf | DOI:10.1016/j.ic.2010.11.015 | abstract We introduce the class of Rigid Tree Automata (RTA), an extension of standard bottom-up automata on ranked trees with distinguished states called rigid. Rigid states define a restriction on the computation of RTA on trees: RTA can test for equality in subtrees reaching the same rigid state. RTA are able to perform local and global tests of equality between subtrees, non-linear tree pattern matching, and some inequality and disequality tests as well. Properties like determinism, pumping lemma, Boolean closure, and several decision problems are studied in detail. In particular, the emptiness problem is shown decidable in linear time for RTA whereas membership of a given tree to the language of a given RTA is NP-complete. Our main result is the decidability of whether a given tree belongs to the rewrite closure of an RTA language under a restricted family of term rewriting systems, whereas this closure is not an RTA language. This result, one of the first on rewrite closure of languages of tree automata with constraints, is enabling the extension of model checking procedures based on finite tree automata techniques, in particular for the verification of communicating processes with several local non rewritable memories, like security protocols. Finally, a comparison of RTA with several classes of tree automata with local and global equality tests, with dag automata and Horn clause formalisms is also provided.

Formalisation des relations temporelles dans un contexte d'accompagnement musical automatique.
José Echeveste, Arshia Cont, Jean-Louis Giavitto, Florent Jacquemard.
Hermès. 8e Colloque sur la Modélisation des Systèmes Réactifs (MSR'11), Nov 2011, Lille, France. Modélisation des Systèmes Réactifs : MSR 2011, 45, pages 109-124, n° spécial du Journal Européen des Systèmes Automatisés (JESA).
bibTeX | pdf | abstract We sketch the real-time features required by automatic musical accompaniment seen as a reactive system. We formalize the datation of musical event taking into account the various temporal scales used in music. Various strategies for the handling of synchronization constraints and the handling of errors are presented.

Controlled Term Rewriting.
Florent Jacquemard, Yoshiharu Kojima, Masahiko Sakai.
8th International Symposium Frontiers of Combining Systems (FroCoS 2011) Lecture Notes in Artificial Intelligence vol. 6989, pages 179-194, Springer, 2011.
bibTeX | pdf | abstract Motivated by the problem of verification of imperative tree transformation programs, we study the combination, called controlled term rewriting systems (CntTRS), of term rewriting rules with con- straints selecting the possible rewrite positions. These constraints are specified, for each rewrite rule, by a selection automaton which defines a set of positions in a term based on tree automata computations. We show that reachability is PSPACE-complete for so-called monotonic CntTRS, such that the size of every left-hand-side of every rewrite rule is larger or equal to the size of the corresponding right-hand-side, and also for the class of context-free non-collapsing CntTRS,…

Multiple Congruence Relations, First-Order Theories on Terms, and the Frames of the Applied Pi-Calculus.
Florent Jacquemard, Etienne Lozes, Ralf Treinen, Jules Villard.
Theory of Security and Applications (TOSCA, affiliated to ETAPS), Mar 2011, Saarbrücken, Germany. Springer, Lecture Notes in Computer Science.
bibTeX | pdf | abstract We investigate the problem of deciding first-order theories of finite trees with several distinguished congruence relations, each of them given by some equational axioms. We give an automata-based solution for the case where the different equational axiom systems are linear and variable-disjoint (this includes the case where all axioms are ground), and where the logic does not permit to express tree relations x=f(y,z). We show that the problem is undecidable when these restrictions are relaxed. As motivation and application, we show how to translate the model-checking problem of Apil, a spatial equational logic for the applied pi-calculus, to the validity …

Modèles d'automates d'arbres étendus pour la vérification de systèmes infinis.
Florent Jacquemard.
HDR École normale supérieure de Cachan - ENS Cachan, Nov. 2011.
bibTeX | pdf | slides-hdr.pdf | slides-hdr-long-version.pdf | abstract We present a study of several models of state machines, all of them extending the same formalism: the classical tree automata, and their application in various reasoning tasks, such as static analysis of programs or systems, typing, verification of the consistency of specifications, model checking…
Trees are a natural data structure, widespread in computer science, for instance for the representation of hierarchical or nested data structures, e.g. filesystems, for specific algorithms (binary search trees, distributed algorithms), for an abstract model for semi-structured data used for information exchange in the Web, for an algebraic presentation of recursive processes, as terms in logic.
When it comes to reasoning on systems manipulating trees, or modeled by trees, it is crucial to have finite representation of infinite sets of trees. Tree automata are finite state machines providing such a representation, acknowledged as suitable for a use in reasoning tasks: they are a well established theoretical model, in close relationship with logic, they enjoy good compositional properties and efficient decision algorithms. In particular, tree automata are used at the core of systems for software and hardware verification and theorem proving.
However, tree automata have also some severe limitations in expressiveness. For instance, they are unable of non-linear pattern matching or of expressing integrity constraints such as keys. Some extensions have been proposed in order to improve the model while trying to preserve good properties. We present in this document several such extensions, their properties and the advents of their use in symbolic verification of systems and programs. | keywords Tree Automata Theory; System and Software Verification; Automated Deduction; Model checking; Symbolic Constraint Solving; Term Rewriting.

The Emptiness Problem for Tree Automata with Global Constraints.
Luis Barguño, Carlos Creus, Guillem Godoy, Florent Jacquemard, Camille Vacher.
Jean-Pierre Jouannaud. 25th Annual IEEE Symposium on Logic in Computer Science (LICS), July 2010, Edinburgh, Scotland, United Kingdom. IEEE Computer Society Press, pages 263-272.
bibTeX | pdf | DOI:10.1109/LICS.2010.28 | abstract We define tree automata with global constraints (TAGC), generalizing the class of tree automata with global equality and disequality constraints of Filiot, Talbot and Tison 2008 (TAGED). TAGC can test for equality and disequality between subterms whose positions are defined by the states reached during a computation. In particular, TAGC can check that all the subterms reaching a given state are distinct. This constraint is related to monadic key constraints for XML documents, meaning that every two distinct positions of a given type have different values. We prove decidability of the emptiness problem for TAGC. This solves, in particular, the open question of decidability of emptiness for TAGED. We further extend our result by allowing global arithmetic constraints for counting the number of occurrences of some state or the number of different subterms reaching some state during a computation. We also allow local equality and disequality tests between sibling positions and the extension to unranked ordered trees. As a consequence of our results for TAGC, we prove the decidability of a fragment of the monadic second order logic on trees extended with predicates for equality and disequality between subtrees, and cardinality..

Rewrite-Based Verification of XML Updates.
Florent Jacquemard and Michael Rusinowitch.
12th international ACM SIGPLAN symposium on Principles and practice of declarative programming (PPDP), July 2010, Hagenberg, Austria. Kutsia, Temur and Schreiner, Wolfgang and Fernández, Maribel Eds. ACM.
bibTeX | pdf | DOI:10.1145/1836089.1836105 | abstract We propose a model for XML update primitives of the W3C XQuery Update Facility as parameterized rewriting rules of the form: "insert an unranked tree from a regular tree language L as the first child of a node labeled by a". For these rules, we give type inference algorithms, considering types defined by several classes of unranked tree automata. These type inference algorithms are directly applicable to XML static typechecking, which is the problem of verifying whether, a given document transformation always converts source documents of a given input type into documents of a given output type. We show that typechecking for arbitrary sequences of XML update primitives can be done in polynomial time when the unranked tree automaton defining the output type is deterministic and complete, and that it is EXPTIME-complete otherwise. We then apply the results to the verification of access control policies for XML updates. We propose in particular a polynomial time algorithm for the problem of local consistency of a policy, that is, for deciding the non-existence of a sequence of authorized update operations starting from a given document that simulates a forbidden update operation.

XML Access Control: from XACML to Annotated Schemas.
Ryma Abassi, Florent Jacquemard, Michael Rusinowitch, El Fatmi Sihem Guemara.
Second International Conference on Communications and Networking (ComNet), November 2010, Tozeur, Tunisia. IEEE Computer Society Press, pages 1-8.
bibTeX | DOI:10.1109/COMNET.2010.5699810 | abstract XML became the de facto standard for the data representation and exchange on the internet. Regarding XML documents access control policy definition, OASIS ratified the XACML standard. It is a declarative language allowing the specification of authorizations as rules. Furthermore, it is common to formally represent XML documents as labeled trees and to handle secure requests through “user views”. A user view is the part of the document accessible to a given user according to the existing policy. Moreover, control access polices can be depicted as annotated rules where annotations define for each document node whether it is accessible. Hence, an annotated schema is a formal representation of “user views”. Our main contribution in this paper is then three folds. First, we compare XACML policies and annotated schemas. Second, we identify a significant fragment of XACML since this latter is very expressive and consequently complex. Third, we define adequate translation algorithms from XACML policies to annotated schemas.

Unique Normalization for Shallow TRS.
Guillem Godoy, Florent Jacquemard.
20th International Conference on Rewriting Techniques and Applications (RTA), June 2009, Brazilia, Brazil. pages 63-77, Lecture Notes in Computer Science, 5595, Springer. 2009.
bibTeX | pdf | DOI:10.1007/978-3-642-02348-4_5 | abstract Computation with a term rewrite system (TRS) consists in the application of its rules from a given starting term until a normal form is reached, which is considered the result of the computation. The unique normalization (UN) property for a TRS R states that any starting term can reach at most one normal form when R is used, i.e. that the computation with R is unique. We study the decidability of this property for classes of TRS defined by syntactic restrictions such as linearity (variables can occur only once in each side of the rules), flatness (sides of the rules have height at most one) and shallowness (variables occur at depth at most one in the rules). We prove that UN is decidable in polynomial time for shallow and linear TRS, using tree automata techniques. This result is very near to the limits of decidability, since this property is known undecidable even for very restricted classes like right-ground TRS, flat TRS and also right-flat and linear TRS. We also show that UN is even undecidable for flat and right-linear TRS. The latter result is in contrast with the fact that many other natural properties like reachability, termination, confluence, weak normalization, etc. are decidable for this class of TRS.

Rigid Tree Automata.
Florent Jacquemard, Francis Klay, Camille Vacher.
Third International Conference on Language and Automata Theory and Applications (LATA), April 2009, Tarragona, Spain. pages 446-457, Lecture Notes in Computer Science vol. 5457, Adrian Horia Dediu and Armand Mihai Ionescu and Carlos Martín-Vide Eds, Springer. 2009.
bibTeX | pdf | DOI:10.1007/978-3-642-00982-2_38 | abstract We introduce the class of Rigid Tree Automata (RTA), an extension of standard bottom-up automata on ranked trees with distinguished states called rigid. Rigid states define a restriction on the computation of RTA on trees: RTA can test for equality in subtrees reaching the same rigid state. RTA are able to perform local and global tests of equality between subtrees, non-linear tree pattern matching, and restricted disequality tests as well. Properties like determinism, boolean closure, and several decision problems are studied in detail. In particular, the emptiness problem is shown decidable in linear time for RTA whereas membership of a given tree to the language of a given RTA is NP-complete. Our main result is the decidability of whether a given tree belongs to the rewrite closure of a RTA language under a restricted family of term rewriting systems, whereas this closure is not a RTA language. This result, one of the first on rewrite closure of languages of tree automata with constraints, is enabling the extension of model checking procedures based on finite tree automata techniques. Finally, a comparison of RTA with several classes of tree automata with local and global equality tests, and with dag automata is also provided.

Automatic Verification of Conformance of Firewall Configurations to Security Policies.
Nihel Ben Youssef, Bouhoula Adel, Jacquemard Florent.
IEEE Symposium on Computers and Communications (ISCC), July 2009, Sousse, Tunisia. IEEE Computer Society Press, pages 526-531.
bibTeX | pdf | DOI:10.1109/ISCC.2009.5202309 | abstract The configuration of firewalls is highly error prone and automated solution are needed in order to analyze its correctness. We propose a formal and automatic method for checking whether a firewall reacts correctly wrt a security policy given in an high level declarative language. When errors are detected, some feedback is returned to the user in order to correct the firewall configuration. Furthermore, the procedure verifies that no conflicts exist within the security policy. We show that our method is both correct and complete. Finally, it has been implemented in a prototype of verifier based on a satisfiability solver modulo theories (SMT). Experiment conducted on relevant case studies demonstrate the efficiency and scalability of the approach.

Visibly Tree Automata with Memory and Constraints.
Hubert Comon-Lundh, Florent Jacquemard, Nicolas Perrin.
Logical Methods in Computer Science (LMCS), Thompson ISI and SCOPUS and Mathematical Reviews and Zentralblatt, 2008, 4 (2).
bibTeX | pdf | DOI:10.2168/LMCS-4(2:8)2008 | abstract Tree automata with one memory have been introduced in 2001. They generalize both pushdown (word) automata and the tree automata with constraints of equality between brothers of Bogaert and Tison. Though it has a decidable emptiness problem, the main weakness of this model is its lack of good closure properties. We propose a generalization of the visibly pushdown automata of Alur and Madhusudan to a family of tree recognizers which carry along their (bottom-up) computation an auxiliary unbounded memory with a tree structure (instead of a symbol stack). In other words, these recognizers, called Visibly Tree Automata with Memory (VTAM) define a subclass of tree automata with one memory enjoying Boolean closure properties. We show in particular that they can be determinized and the problems like emptiness, membership, inclusion and universality are decidable for VTAM. Moreover, we propose several extensions of VTAM whose transitions may be constrained by different kinds of tests between memories and also constraints a la Bogaert and Tison. We show that some of these classes of constrained VTAM keep the good closure and decidability properties, and we demonstrate their expressiveness with relevant examples of tree languages.

Tree automata with equality constraints modulo equational theories.
Florent Jacquemard, Michael Rusinowitch, Laurent Vigneron.
Journal of Logic and Algebraic Programming, Elsevier, 2008, 75 (2), pages 182-208.
bibTeX | pdf | DOI:10.1016/j.jlap.2007.10.006 | abstract This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that these classes have a good potential for application in e.g. software verification. These tree automata are obtained by extending the standard Horn clause representations with equational conditions and rewrite systems. We show in particular that a generalized membership problem (extending the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodulation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formula.

Closure of Hedge-Automata Languages by Hedge Rewriting.
Florent Jacquemard, Michael Rusinowitch.
19th International Conference on Rewriting Techniques and Applications - RTA 2008 A. Voronkov Ed. Hagenberg, Austria. Lecture Notes in Computer Science, 5117, pages 157-171, Springer, 2008
bibTeX | pdf | DOI:10.1007/978-3-540-70590-1_11 | abstract We consider rewriting systems for unranked ordered terms, i.e. trees where the number of successors of a node is not determined by its label, and is not a priori bounded. The rewriting systems are defined such that variables in the rewrite rules can be substituted by hedges (sequences of terms) instead of just terms. Consequently, this notion of rewriting subsumes both standard term rewriting and word rewriting. We investigate some preservation properties for two classes of languages of unranked ordered terms under this generalization of term rewriting. The considered classes include languages of hedge automata (HA) and some extension (called CF-HA) with context-free languages in transitions, instead of regular languages. In particular, we show that the set of unranked terms reachable from a given HA language, using a so called inverse context-free rewrite system, is a HA language. The proof, based on a HA completion procedure, reuses and combines known techniques with non-trivial adaptations. Moreover, we prove, with different techniques, that the closure of CF-HA languages with respect to restricted context-free rewrite systems, the symmetric case of the above rewrite systems, is a CF-HA language. As a consequence, the problems of ground reachability and regular hedge model checking are decidable in both cases. We give several counter examples showing that we cannot relax the restrictions.

Closure of Tree Automata Languages under Innermost Rewriting.
Adria Gascon, Guillem Godoy, Florent Jacquemard.
8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS), July 2008, Hagenberg, Austria. Elsevier, Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2008), 237, pages 23-38, Electronic Notes in Theoretical Computer Science Aart Middeldorp (Ed).
bibTeX | pdf | DOI:10.1016/j.entcs.2009.03.033 | abstract Preservation of regularity by a term rewriting system (TRS) states that the set of reachable terms from a tree automata (TA) language (aka regular term set) is also a TA language. It is an important and useful property, and there have been many works on identifying classes of TRS ensuring it; unfortunately, regularity is not preserved for restricted classes of TRS like shallow TRS. Nevertheless, this property has not been studied for important strategies of rewriting like the innermost strategy – which corresponds to the {\em call by value} computation of programming languages. We prove that the set of innermost-reachable terms from a TA language by a shallow TRS is not necessarily regular, but it can be recognized by a TA with equality and disequality constraints between brothers. As a consequence we conclude decidability of regularity of the reachable set of terms from a TA language by innermost rewriting and shallow TRS. This result is in contrast with plain (not necessarily innermost) rewriting for which we prove undecidability. We also show that, like for plain rewriting, innermost rewriting with linear and right-shallow TRS preserves regularity.

Automated Induction with Constrained Tree Automata.
Adel Bouhoula, Florent Jacquemard.
4th International Joint Conference on Automated Reasoning (IJCAR), August 2008, Sydney, Australia. Lecture Notes in Computer Science 5195, pages 539-554, Alessandro Armando and Peter Baumgartner and Gilles Dowek (Eds.) Springer, 2008.
bibTeX | pdf | DOI:10.1007/978-3-540-71070-7_44 | abstract We propose a procedure for automated implicit inductive theorem proving for equational specifications made of rewrite rules with conditions and constraints. The constraints are interpreted over constructor terms (representing data values), and may express syntactic equality, disequality, ordering and also membership in a fixed tree language. Constrained equational axioms between constructor terms are supported and can be used in order to specify complex data structures like sets, sorted lists, trees, powerlists… Our procedure is based on tree grammars with constraints, a formalism which can describe exactly the initial model of the given specification (when it is sufficiently complete and terminating). They are used in the inductive proofs first as an induction scheme for the generation of subgoals at induction steps, second for checking validity and redundancy criteria by reduction to an emptiness problem, and third for defining and solving membership constraints. We show that the procedure is sound and refutationally complete. It generalizes former test set induction techniques and yields natural proofs for several non-trivial examples presented in the paper, these examples are difficult (if not impossible) to specify and carry on automatically with other induction procedures.

Tree Automata with Memory, Visibility and Structural Constraints.
Hubert Comon-Lundh, Florent Jacquemard, Nicolas Perrin.
10th International Conference on Foundations of Software Science and Computation Structures (FOSSACS), Mar 2007, Braga, Portugal. Springer, 10th International Conference on Foundations of Software Science and Computation Structures (FOSSACS), 4423, pages 168-182, Lecture Notes in Computer Science, Helmut Seidl (Ed).
bibTeX | pdf | DOI:10.1007/978-3-540-71389-0_13 | abstract Tree automata with one memory have been introduced in 2001. They generalize both pushdown (word) automata and the tree automata with constraints of equality between brothers of Bogaert and Tison. Though it has a decidable emptiness problem, the main weakness of this model is its lack of good closure properties. We propose a generalization of the visibly pushdown automata of Alur and Madhusudan to a family of tree recognizers which carry along their (bottom-up) computation an auxiliary unbounded memory with a tree structure (instead of a symbol stack). In other words, these recognizers, called visibly Tree Automata with Memory (VTAM) define a subclass of tree automata with one memory enjoying Boolean closure properties. We show in particular that they can be determinized and the problems like emptiness, inclusion and universality are decidable for VTAM. Moreover, we propose an extension of VTAM whose transitions may be constrained by structural equality and disequality tests between memories, and show that this extension preserves the good closure and decidability properties.

Verifying Regular Trace Properties of Security Protocols with Explicit Destructors and Implicit Induction.
Adel Bouhoula, Florent Jacquemard.
Pierpaolo Degano, Ralf Küsters, Luca Vigano and Steve Zdancewic. Proceedings of the Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA), pages 27-44, Jul 2007, Poland.
bibTeX | pdf | abstract We present a procedure for the verification of cryptographic protocols based on a new method for automatic implicit induction theorem proving for specifications made of conditional and constrained rewrite rules. The method handles axioms between constructor terms which are used to introduce explicit destructor symbols for the specification of cryptographic operators. Moreover, it can deal with non-confluent rewrite systems. This is required in the context of the verification of security protocols because of the non-deterministic behavior of attackers. Our induction method makes an intensive use of constrained tree grammars, which are used in proofs both as induction schemes and as oracles for checking validity and redundancy criteria by reduction to an emptiness problem. The grammars make possible the development of a generic framework for the specification and verification of protocols, where the specifications can be parametrized with (possibly infinite) regular sets of user names or attacker’s initial knowledge and complex security properties can be expressed, referring to some fixed regular sets of bad traces representing potential vulnerabilities. We present some case studies giving very promising results, for the detection of attacks (our procedure is complete for refutation), and also for the validation of protocols.

Tree Automata Techniques and Applications.
Hubert Comon-Lundh, Max Dauchet, Rémi Gilleron, Cristof Löding, Florent Jacquemard, Denis Lugiez, Sophie Tison, Marc Tommasi.
Online book available on: http://tata.gforge.inria.fr
bibTeX | pdf