Search

Your search keyword '"Jacquemard, Florent"' showing total 46 results
Start Over Author "Jacquemard, Florent" Search Limiters Full Text
46 results on '"Jacquemard, Florent"'

1. Engraving Oriented Joint Estimation of Pitch Spelling and Local and Global Keys

Author

Bouquillard, Augustin and Jacquemard, Florent

Subjects
Computer Science - Sound, Computer Science - Information Retrieval, Electrical Engineering and Systems Science - Audio and Speech Processing
Abstract

We revisit the problems of pitch spelling and tonality guessing with a new algorithm for their joint estimation from a MIDI file including information about the measure boundaries. Our algorithm does not only identify a global key but also local ones all along the analyzed piece. It uses Dynamic Programming techniques to search for an optimal spelling in term, roughly, of the number of accidental symbols that would be displayed in the engraved score. The evaluation of this number is coupled with an estimation of the global key and some local keys, one for each measure. Each of the three informations is used for the estimation of the other, in a multi-steps procedure. An evaluation conducted on a monophonic and a piano dataset, comprising 216 464 notes in total, shows a high degree of accuracy, both for pitch spelling (99.5% on average on the Bach corpus and 98.2% on the whole dataset) and global key signature estimation (93.0% on average, 95.58% on the piano dataset). Designed originally as a backend tool in a music transcription framework, this method should also be useful in other tasks related to music notation processing., Comment: International Conference on Technologies for Music Notation and Representation (TENOR), Apr 2024, Zurich (CH), Switzerland

Published
2024

2. 8+8=4: Formalizing Time Units to Handle Symbolic Music Durations

Author

Karystinaios, Emmanouil, Foscarin, Francesco, Jacquemard, Florent, Sakai, Masahiko, Tojo, Satoshi, and Widmer, Gerhard

Subjects
Computer Science - Sound, Electrical Engineering and Systems Science - Audio and Speech Processing
Abstract

This paper focuses on the nominal durations of musical events (notes and rests) in a symbolic musical score, and on how to conveniently handle these in computer applications. We propose the usage of a temporal unit that is directly related to the graphical symbols in musical scores and pair this with a set of operations that cover typical computations in music applications. We formalize this time unit and the more commonly used approach in a single mathematical framework, as semirings, algebraic structures that enable an abstract description of algorithms/processing pipelines. We then discuss some practical use cases and highlight when our system can improve such pipelines by making them more efficient in terms of data type used and the number of computations., Comment: In Proceedings of the International Symposium on Computer Music Multidisciplinary Research (CMMR 2023), Tokyo, Japan

Published
2023

4. FO2(<,+1,~) on data trees, data tree automata and branching vector addition systems

Author

Jacquemard, Florent, Segoufin, Luc, and Dimino, Jerémie

Subjects
Computer Science - Formal Languages and Automata Theory
Abstract

A 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.

Published
2016
Full Text
View/download PDF

5. Antescofo Intermediate Representation

Author

Jacquemard, Florent and Sanchez, Clément Poncelet

Subjects
Computer Science - Multimedia, Computer Science - Programming Languages
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)., Comment: RR-8520 (2014)

Published
2014

6. Decidable Classes of Tree Automata Mixing Local and Global Constraints Modulo Flat Theories

Author

Barguñó, Luis, Creus, Carles, Godoy, Guillem, Jacquemard, Florent, and Vacher, Camille

Subjects
Computer Science - Logic in Computer Science, Computer Science - Formal Languages and Automata Theory
Abstract

We define a class of ranked tree automata TABG generalizing both the tree automata with local tests between brothers 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 the 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., Comment: 39 pages, to appear in LMCS journal

Published
2013
Full Text
View/download PDF

7. Rewrite Closure and CF Hedge Automata

Author

Jacquemard, Florent and Rusinowitch, Michael

Subjects
Computer Science - Logic in Computer Science, Computer Science - Databases, Computer Science - Formal Languages and Automata Theory
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.

Published
2012

8. Rewrite based Verification of XML Updates

Author

Jacquemard, Florent and Rusinowitch, Michael

Subjects
Computer Science - Logic in Computer Science
Abstract

We consider problems of access control for update of XML documents. In the context of XML programming, types can be viewed as hedge automata, and static type checking amounts to verify that a program always converts valid source documents into also valid output documents. Given a set of update operations we are particularly interested by checking safety properties such as preservation of document types along any sequence of updates. We are also interested by the related policy consistency problem, that is detecting whether a sequence of authorized operations can simulate a forbidden one. We reduce these questions to type checking problems, solved by computing variants of hedge automata characterizing the set of ancestors and descendants of the initial document type for the closure of parameterized rewrite rules.

Published
2009

9. Automated Induction for Complex Data Structures

Author

Bouhoula, Adel and Jacquemard, Florent

Subjects
Computer Science - Logic in Computer Science, Computer Science - Symbolic Computation, F.4.1, F.4.2, F.4.3
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 to specify and carry on automatically with related induction procedures., Comment: This is the long version of a paper which appeared in IJCAR 2008. 38 pages

Published
2008

10. Visibly Tree Automata with Memory and Constraints

Author

Comon-Lundh, Hubert, Jacquemard, Florent, and Perrin, Nicolas

Subjects
Computer Science - Logic in Computer Science, F.1.1, F.1.2, I.2.2, I.2.3
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 comparing brother subtrees in the tree in input. 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., Comment: 36 pages including an appendix

Published
2008
Full Text
View/download PDF

14. ASAP: A dataset of aligned scores and performances for piano transcription

Author

Foscarin, Francesco, Mcleod, Andrew, Rigaux, Philippe, Jacquemard, Florent, Sakai, Masahiko, CEDRIC. Données complexes, apprentissage et représentations (CEDRIC - VERTIGO), Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM)-Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), Ecole Polytechnique Fédérale de Lausanne (EPFL), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), Nagoya University, HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), and HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)

Subjects
MIR tasks, Novel datasets and use cases, Evaluation, datasets, and reproducibility, [INFO.INFO-DL]Computer Science [cs]/Digital Libraries [cs.DL], Annotation protocols, Music transcription and annotation
Abstract

International audience; In this paper we present Aligned Scores and Performances (ASAP): a new dataset of 222 digital musical scores aligned with 1068 performances (more than 92 hours) of Western classical piano music. The scores are provided as paired MusicXML files and quantized MIDI files, and the performances as paired MIDI files and partially as audio recordings. Scores and performances are aligned with downbeat, beat, time signature, and key signature annotations. ASAP has been obtained thanks to a new annotation workflow that combines score analysis and alignment algorithms, with the goal of reducing the time for manual annotation. The dataset itself is, to our knowledge, the largest that includes an alignment of music scores to MIDI and audio performance data. As such, it is a useful resource for a wide variety of MIR applications, from those that target the complete audio-to-score Automatic Music Transcription task, to others that target more specific aspects (e.g., key signature estimation and beat or downbeat tracking from both MIDI and audio representations).

Published
2020
Full Text
View/download PDF

17. Gioqoso, an online Quality Assessment Tool for Music Notation

Author

Foscarin, Francesco, Fiala, David, Jacquemard, Florent, Rigaux, Philippe, Thion, Virginie, Centre d'études et de recherche en informatique et communications (CEDRIC), Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM), Centre d'études supérieures de la Renaissance UMR 7323 (CESR), Ministère de la Culture et de la Communication (MCC)-Université de Tours (UT)-Centre National de la Recherche Scientifique (CNRS), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), CEDRIC. Données complexes, apprentissage et représentations (CEDRIC - VERTIGO), HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-HESAM Université - Communauté d'universités et d'établissements Hautes écoles Sorbonne Arts et métiers université (HESAM)-Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), Symbolic and Human-centric view of dAta MANagement (SHAMAN), GESTION DES DONNÉES ET DE LA CONNAISSANCE (IRISA-D7), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Sandeep Bhagwati and Jean Bresson, Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM)-Ecole Nationale Supérieure d'Informatique pour l'Industrie et l'Entreprise (ENSIIE)-Conservatoire National des Arts et Métiers [CNAM] (CNAM), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Jacquemard, Florent, Ministère de la Culture et de la Communication (MCC)-Université de Tours-Centre National de la Recherche Scientifique (CNRS), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), and Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)

Subjects
[INFO.INFO-TT]Computer Science [cs]/Document and Text Processing, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], [INFO.INFO-DB] Computer Science [cs]/Databases [cs.DB], [INFO.INFO-TT] Computer Science [cs]/Document and Text Processing, [INFO.INFO-DL]Computer Science [cs]/Digital Libraries [cs.DL], [INFO.INFO-DL] Computer Science [cs]/Digital Libraries [cs.DL], ComputingMilieux_MISCELLANEOUS
Abstract

International audience

Published
2018

20. Some results on confluence: decision and what to do without

Author

Jacquemard, Florent, Représentations musicales (Repmus), Sciences et Technologies de la Musique et du Son (STMS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Synchronous Realtime Processing and Programming of Music Signals (MuTant), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Beniamino Accattoli, Ashish Tiwari, ANR-13-JS02-0004,EFFICACe,Environnement de contrôle 'en temps' pour la composition assistée par ordinateur(2013), Jacquemard, Florent, and Jeunes Chercheuses et Jeunes Chercheurs - Environnement de contrôle 'en temps' pour la composition assistée par ordinateur - - EFFICACe2013 - ANR-13-JS02-0004 - JC - VALID

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Computer Science::Programming Languages, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

International audience; We recall first some decidability results on the confluence of TRS, and related properties 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.

Published
2016

21. Generating equivalent rhythmic notations based on rhythm tree languages

Author

Jacquemard, Florent, Ycart, Adrien, Sakai, Masahiko, Lopez Palma, Helena, Solomon, Mike, Tucci, Emilianae, Lage, Carmen, Synchronous Realtime Processing and Programming of Music Signals (MuTant), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Sciences et Technologies de la Musique et du Son (STMS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Nagoya University, Helena Lopez Palma and Mike Solomon, Inria de Paris, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Centre National de la Recherche Scientifique (CNRS)

Subjects
[INFO.INFO-TT]Computer Science [cs]/Document and Text Processing, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], ComputingMilieux_PERSONALCOMPUTING
Abstract

International audience; 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.

Published
2017
Full Text
View/download PDF

22. Model-Based Testing for Building Reliable Realtime Interactive Music Systems

Author

Poncelet, Clement, Jacquemard, Florent, Synchronous Realtime Processing and Programming of Music Signals (MuTant), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Représentations musicales (Repmus), Sciences et Technologies de la Musique et du Son (STMS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), DGA-MRIS scholarship N° 2013 - 126272 /DGA/DS/MRIS, ANR-12-CORD-0009,INEDIT,INteractivité dans l'Ecriture De l'Interaction et du Temps(2012), Poncelet Sanchez, Clément, and Contenus et Interactions - INteractivité dans l'Ecriture De l'Interaction et du Temps - - INEDIT2012 - ANR-12-CORD-0009 - CONTINT - VALID

Subjects
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], [INFO.INFO-SE] Computer Science [cs]/Software Engineering [cs.SE], [INFO.INFO-SD]Computer Science [cs]/Sound [cs.SD], [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Timed Automata, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Model Based Testing, [INFO.INFO-SD] Computer Science [cs]/Sound [cs.SD], Interactive Music Systems, [INFO.INFO-ES] Computer Science [cs]/Embedded Systems, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]
Abstract

International audience; 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.

Published
2016

23. An Automatic Test Framework for Interactive Music Systems

Author

Jacquemard, Florent, Poncelet, Clément, Poncelet Sanchez, Clément, Contenus et Interactions - INteractivité dans l'Ecriture De l'Interaction et du Temps - - INEDIT2012 - ANR-12-CORD-0009 - CONTINT - VALID, Représentations musicales (Repmus), Sciences et Technologies de la Musique et du Son (STMS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Synchronous Realtime Processing and Programming of Music Signals (MuTant), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), DGA-MRIS scholarship N° 2013 - 126272 /DGA/DS/MRIS, and ANR-12-CORD-0009,INEDIT,INteractivité dans l'Ecriture De l'Interaction et du Temps(2012)

Subjects
[INFO.INFO-OH] Computer Science [cs]/Other [cs.OH], Score Based Interactive Music Systems, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], Realtime Systems, Generation of Artificial Music Performances, Model Based Testing
Abstract

International audience; 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 require- ments 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.

Published
2016
Full Text
View/download PDF

24. Unranked Tree Rewriting and Effective Closures of Languages

Author

Jacquemard, Florent, Rusinowitch, Michaël, Représentations musicales (Repmus), Sciences et Technologies de la Musique et du Son (STMS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Synchronous Realtime Processing and Programming of Music Signals (MuTant), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Centre National de la Recherche Scientifique (CNRS), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), and Jacquemard, Florent

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [INFO.INFO-WB] Computer Science [cs]/Web, [INFO.INFO-CL] Computer Science [cs]/Computation and Language [cs.CL], [INFO.INFO-WB]Computer Science [cs]/Web, XML Updates, Tree Automata, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Term Rewriting
Abstract

International audience; We consider rewriting systems for unranked ordered trees, where the number of chil- dren 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, ap- plications to static type checking for XML transformations and to the verification of read/write access control policies for XML updates are mentioned.

Published
2013

25. Tree Automata with Constraints: a brief survey

Author

Filiot, Emmanuel, Jacquemard, Florent, Tison, Sophie, Laboratoire d'Algorithmique Complexité et Logique (LACL), Université Paris-Est Créteil Val-de-Marne - Paris 12 (UPEC UP12)-Centre National de la Recherche Scientifique (CNRS), Sciences et Technologies de la Musique et du Son (STMS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Synchronous Realtime Processing and Programming of Music Signals (MuTant), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique Fondamentale de Lille (LIFL), Université de Lille, Sciences et Technologies-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lille, Sciences Humaines et Sociales-Centre National de la Recherche Scientifique (CNRS), Linking Dynamic Data (LINKS ), Université de Lille, Sciences et Technologies-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lille, Sciences Humaines et Sociales-Centre National de la Recherche Scientifique (CNRS)-Université de Lille, Sciences et Technologies-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lille, Sciences Humaines et Sociales-Centre National de la Recherche Scientifique (CNRS)-Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria), Sebastian Maneth and Helmut Seidl, Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Centre National de la Recherche Scientifique (CNRS), and Jacquemard, Florent

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Nonlinear Sciences::Cellular Automata and Lattice Gases, Computer Science::Formal Languages and Automata Theory
Abstract

International audience; It is well-known that tree automata define exactly regular languages of trees. However for some problems one sometimes needs to test for equalities and disequalities of subtrees. For instance, ranges of non-linear tree transducers cannot be represented by tree automata. To overcome this problem some extensions of tree automata with tree (dis)equality constraints have been proposed. This talk surveys some of the most important models and their applications. Two families of automata are presented. First, we consider automata with local constraints. They have been used to solve problems related to pattern-matching, tree rewriting and more recently the tree homomorphism problem. Then, motivated by applications to XML processing and security protocols verification, we present a more recent model of tree automata with global constraints.

Published
2013

26. From Authored to Produced Time in Computer-Musician Interactions

Author

Cont, Arshia, Giavitto, Jean-Louis, Jacquemard, Florent, Synchronous Realtime Processing and Programming of Music Signals (MuTant), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Représentations musicales (Repmus), Sciences et Technologies de la Musique et du Son (STMS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), John Thomas, Yue Pan, Thomas Erickson, Eli Blevis, Catherine Letondal, Aurélien Tabard, ANR-12-CORD-0009,INEDIT,INteractivité dans l'Ecriture De l'Interaction et du Temps(2012), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Centre National de la Recherche Scientifique (CNRS), Jacquemard, Florent, and Contenus et Interactions - INteractivité dans l'Ecriture De l'Interaction et du Temps - - INEDIT2012 - ANR-12-CORD-0009 - CONTINT - VALID

Subjects
ACM: H.: Information Systems/H.5: INFORMATION INTERFACES AND PRESENTATION (e.g., HCI)/H.5.5: Sound and Music Computing/H.5.5.0: Methodologies and techniques, InformationSystems_INFORMATIONINTERFACESANDPRESENTATION(e.g.,HCI), ACM: H.: Information Systems/H.5: INFORMATION INTERFACES AND PRESENTATION (e.g., HCI)/H.5.5: Sound and Music Computing/H.5.5.3: Systems, [INFO.INFO-HC]Computer Science [cs]/Human-Computer Interaction [cs.HC], [INFO.INFO-HC] Computer Science [cs]/Human-Computer Interaction [cs.HC]
Abstract

International audience; 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.

Published
2013

27. Formal Timing Analysis of Mixed Music Scores

Author

Fanchon, Léa, Jacquemard, Florent, Synchronous Realtime Processing and Programming of Music Signals (MuTant), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Centre National de la Recherche Scientifique (CNRS), Sciences et Technologies de la Musique et du Son (STMS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), ANR-12-CORD-0009,INEDIT,INteractivité dans l'Ecriture De l'Interaction et du Temps(2012), Jacquemard, Florent, and Contenus et Interactions - INteractivité dans l'Ecriture De l'Interaction et du Temps - - INEDIT2012 - ANR-12-CORD-0009 - CONTINT - VALID

Subjects
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], antescofo, Languages for Computer Music, Verification, [INFO.INFO-MM]Computer Science [cs]/Multimedia [cs.MM], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Realtime Systems, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems, Timed Automata, Formal Methods, Interactive Music Systems, Representation and Models for Computer Music
Abstract

International audience; 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.

Published
2013

29. Formalisation des relations temporelles dans un contexte d'accompagnement musical automatique

Author

Echeveste, José, Cont, Arshia, Giavitto, Jean-Louis, Jacquemard, Florent, Jacquemard, Florent, Hermès, Synchronous Realtime Processing and Programming of Music Signals (MuTant), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Représentations musicales (Repmus), Sciences et Technologies de la Musique et du Son (STMS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Verification in databases (DAHU), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Étienne Craye and Abdoulaye Gamalié, Inria Paris-Rocquencourt, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Centre National de la Recherche Scientifique (CNRS)

Subjects
antescofo, Error Handling, Computer Music, [INFO.INFO-DC] Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], Synchronous Language, Automatic Musical Accompaniment, Synchronous Programming, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], Score Following
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., Nous présentons les problématiques temps réel de l'accompagnement musical automatique vu comme un système réactif. Nous introduisons un modèle de datation prenant en compte les différentes échelles de temps spécifiques à la musique, et nous proposons plusieurs stratégies de synchronisation et de rattrapage d'erreurs effectivement utilisées dans diverses compositions musicales.

Published
2011

30. Test methods for Score-Based Interactive Music Systems Toward a formal Specification

Author

Poncelet, Clément, Jacquemard, Florent, Synchronous Realtime Processing and Programming of Music Signals (MuTant), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Représentations musicales (Repmus), Sciences et Technologies de la Musique et du Son (STMS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Poncelet Sanchez, Clément, Inria Paris-Rocquencourt, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Centre National de la Recherche Scientifique (CNRS)

Subjects
[INFO.INFO-OH] Computer Science [cs]/Other [cs.OH], [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH]
Abstract

International audience; Time Line How be sure of a Score-Based Interactive Music System's behavior during shows ? Ensuring a " guarantee " on the behavior of a complex real-time system is not trivial and requires formal method. Today, Antescofo's behavior is " manually " checked by the compositor during rehearsals. Since rehearsal performances represent just a few set of all possible interpretations of a score, this method is not rigorous. The poster depicts another rigorous method.

Published
2014

32. A Synchronous Embedding of Antescofo, a Domain-Specific Language for Interactive Mixed Music

Author

Baudart, Guillaume, Mandel, Louis, Jacquemard, Florent, Pouzet, Marc, Parallélisme de Kahn Synchrone (Parkas ), Département d'informatique - ENS Paris (DI-ENS), École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Synchronous Realtime Processing and Programming of Music Signals (MuTant), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Sciences et Technologies de la Musique et du Son (STMS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Université Paris sciences et lettres (PSL), Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Inria Paris-Rocquencourt, Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Centre National de la Recherche Scientifique (CNRS), École normale supérieure - Paris (ENS Paris), Mandel, Louis, Département d'informatique de l'École normale supérieure (DI-ENS), and Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS Paris)

Subjects
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL]
Abstract

International audience; 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.

Published
2013

33. Sufficient Completeness Verification for Conditional and Constrained Term Rewriting Systems

Author

Bouhoula, Adel, Jacquemard, Florent, Ecole supérieure des communications de Tunis (SUP'COM [TUNIS]), Synchronous Realtime Processing and Programming of Music Signals (MuTant), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), projet INRIA-DGRSRT STIC Tunisie STIC-TU1001, Inria Paris-Rocquencourt, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Sufficient Completeness, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Tree Grammars, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Conditional and Constrained Term Rewriting, Narrowing
Abstract

International audience; 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.

Published
2012
Full Text
View/download PDF

34. Tree Automata Techniques and Applications

Author

Comon, Hubert, Dauchet, Max, Gilleron, Rémi, Jacquemard, Florent, Lugiez, Denis, Löding, Christof, Tison, Sophie, Tommasi, Marc, Security of information systems (SECSI), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire d'Informatique Fondamentale de Lille (LIFL), Université de Lille, Sciences et Technologies-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lille, Sciences Humaines et Sociales-Centre National de la Recherche Scientifique (CNRS), Modeling Tree Structures, Machine Learning, and Information Extraction (MOSTRARE), Université de Lille, Sciences et Technologies-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lille, Sciences Humaines et Sociales-Centre National de la Recherche Scientifique (CNRS)-Université de Lille, Sciences et Technologies-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lille, Sciences Humaines et Sociales-Centre National de la Recherche Scientifique (CNRS)-Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria), Verification in databases (DAHU), Laboratoire d'informatique Fondamentale de Marseille - UMR 6166 (LIF), Université de la Méditerranée - Aix-Marseille 2-Université de Provence - Aix-Marseille 1-Centre National de la Recherche Scientifique (CNRS), Rheinisch-Westfälische Technische Hochschule Aachen University (RWTH), Tommasi, Marc, and RWTH Aachen University

Subjects
[INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], ComputingMilieux_MISCELLANEOUS, [INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]
Abstract

International audience

Published
2008

35. Decidable classes of tree automata mixing local and global constraints modulo flat theories

Author

Universitat Politècnica de Catalunya. Departament de Llenguatges i Sistemes Informàtics, Universitat Politècnica de Catalunya. ALBCOM - Algorismia, Bioinformàtica, Complexitat i Mètodes Formals, Barguño, Luis, Creus López, Carles, Godoy Balil, Guillem, Jacquemard, Florent, Vacher, Camile, Universitat Politècnica de Catalunya. Departament de Llenguatges i Sistemes Informàtics, Universitat Politècnica de Catalunya. ALBCOM - Algorismia, Bioinformàtica, Complexitat i Mètodes Formals, Barguño, Luis, Creus López, Carles, Godoy Balil, Guillem, Jacquemard, Florent, and Vacher, Camile

Abstract

We define a class of ranked tree automata TABG generalizing both the tree automata with local tests between brothers 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 the 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., Peer Reviewed, Postprint (published version)

Published
2013

36. Rigid Reachability

Author

Ganzinger, Harald, Jacquemard, Florent, Veanes, Margus, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)

Subjects
reachability, TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], accessibilité, unification du second ordre, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, unification rigide, rigid unification, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, term rewriting, Computer Science::Formal Languages and Automata Theory, second order unification, réécriture de termes
Abstract

Rapport interne.; We show that rigid reachability, the non-symmetric form of rigid E-unification, is undecidable already in the case of a single constraint. From this we infer the undecidability of a new rather restricted kind of second-order unification. We also show that certain decidable subclasses of the problem which are PTIME-complete in the equational case become EXPTIME-complete when symmetry is absent. By applying automata-theoretic methods, simultaneous monadic rigid reachability with ground rules is shown to be in EXPTIME.

Published
1998

37. Unification in Extensions of Shallow Equational Theories

Author

Jacquemard, Florent, Meyer, Christoph, Weidenbach, Christoph, Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), and Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)

Subjects
automates d'arbres, théories monadiques, superposition, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], e-unification, décidabilité, monadic theories, decidability, Physics::Atmospheric and Oceanic Physics, tree automata
Abstract

Rapport interne.; We show that unification in certain extensions of shallow equational theories is decidable. Our extensions generalize the known classes of shallow or standard equational theories. In order to prove decidability of unification in the extensions, a class of Horn clause sets called sorted shallow equational theories is introduced. This class is a natural extension of tree automata with equality constraints between brother subterms as well as shallow sort theories. We show that saturation under sorted superposition is effective on sorted shallow equational theories. So called semi-linear equational theories can be effectively transformed into equivalent sorted shallow equational theories and generalize the classes of shallow and standard equational theories.

Published
1998

39. FO2(<,+1,~) ON DATA TREES, DATA TREE AUTOMATA AND BRANCHING VECTOR ADDITION SYSTEMS.

Author

JACQUEMARD, FLORENT, SEGOUFIN, LUC, and DIMINO, JÉRÉMIE

Subjects
BRANCHING processes, VECTORS (Calculus), ADDITION (Mathematics), MATHEMATICAL variables, MATHEMATICAL domains
Abstract

A 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 DTA#, that is more expressive than FO2(<,+1,~) but such that emptiness of DTA# 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 DTA# are equivalent. [ABSTRACT FROM AUTHOR]

Published
2016
Full Text
View/download PDF

42. Contribution à la théorie des langages de tuiles

Author

Dubourg, Etienne, Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Université de Bordeaux, David Janin, Janin, David, Lawson, Mark V., Zeitoun, Marc, Senizergues, Géraud, Serre, Olivier, Jacquemard, Florent, and STAR, ABES

Subjects
Tiles, Premorphisms, Monoïdes d’Ehresmann, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], Monoïdes inversifs, Inverse monoids, Tuiles, Automates de tuiles, [INFO.INFO-OH] Computer Science [cs]/Other [cs.OH], Birooted trees, Tile automata, Arbres à deux racines, Languages, Ehresmann monoids, Prémorphismes, Langages
Abstract

Tiles are finite, linear or tree-like structures, with a notion of overlapping.In computer science, they offer a useful way to represent musical objects,as studied by Janin [2016]. We will study the sets of tiles, especially asrepresentations of algebraic objects, based on the theory of inverse semigroups.Our main focus will be languages of tiles, and the appropriate recognizers,than can be defined by the adaptation to tiles of well-known notions over languagesof words. We will look into the recognition by automata, by presentingautomata over linear and tree-like tiles. We will remark the limits of the powerof such automata.While the notion of recognizability by morphisms is unsuitable to languagesof tiles, we will define recognizability by premorphisms, or quasi-recognizability.We will study the links between quasi-recognizability and recognizability bytile automata.We will finally look into the closure properties of the set of tile languages recognizedby automata, and of the set of quasi-recognizable languages. The lastpart will be dedicated to linear tiles, and will present the monoid of restricteddecompositions, a tool for the product of linear tile languages., Les tuiles sont des structures finies, linéaires ou arborescentes, possédantune notion de chevauchement. Elles sont utiles en informatique pourreprésenter des objets musicaux, comme étudié par Janin [2016]. Nous étudieronsles ensembles de tuiles, en particulier comme représentations d’objetsalgébriques, en se basant sur la théorie des semigroupes inversifs.Nos principaux objets d’étude seront les langages de tuiles, et les reconnaisseursappropriés, que l’on peut définir en adaptant aux tuiles des notionsbien connues sur les langages de mots. Nous nous intéresserons à la reconnaissancepar automate, en présentant des automates sur les tuiles linéaires etarborescentes. Nous remarquerons les limites de la puissance de tels automates.Tandis que la notion de reconnaissance par morphisme de monoïdes estinadaptée aux langages de tuiles, nous définirons celle de reconnaissabilité parprémorphisme, ou quasi-reconnaissabilité. Nous étudierons les liens entre quasireconnaissabilitéet reconnaissabilité par automate de tuile.Nous explorerons enfin les propriétés de clôtures de l’ensemble de langagesde tuiles reconnus par automate, et de ceux reconnus par prémorphisme. Ladernière partie sera essentiellement consacrée aux tuiles linéaires, et présenterale monoïde des décompositions restreintes, un outil pour le produit de langagesde tuiles linéaires.

Published
2016

43. A Structural Theory of Rhythm Notation based on Tree Representations and Term Rewriting

Author

Jean Bresson, Pierre Donat-Bouillud, Florent Jacquemard, Synchronous Realtime Processing and Programming of Music Signals (MuTant), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Représentations musicales (Repmus), Sciences et Technologies de la Musique et du Son (STMS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), École normale supérieure - Rennes (ENS Rennes), Oscar Bandtlow and Elaine Chew, Tom Collins, David Meredith and Anja Volk, ANR-13-JS02-0004,EFFICACe,Environnement de contrôle 'en temps' pour la composition assistée par ordinateur(2013), Jacquemard, Florent, Jeunes Chercheuses et Jeunes Chercheurs - Environnement de contrôle 'en temps' pour la composition assistée par ordinateur - - EFFICACe2013 - ANR-13-JS02-0004 - JC - VALID, Inria Paris-Rocquencourt, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Centre National de la Recherche Scientifique (CNRS)

Subjects
Set-builder notation, Theoretical computer science, Abuse of notation, Programming language, 05 social sciences, Term (logic), computer.software_genre, Notation, 01 natural sciences, 010305 fluids & plasmas, Set (abstract data type), Tree (descriptive set theory), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, antescofo, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 0103 physical sciences, Rewriting, 0509 other social sciences, 050904 information & library sciences, Representation (mathematics), computer, Mathematics, [INFO.INFO-FL] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL]
Abstract

International audience; 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.

Published
2015

44. Ground reducibility is EXPTIME-complete

Author

Hubert Comon, Florent Jacquemard, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Verification in databases (DAHU), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Constraints, automatic deduction and software properties proofs (PROTHEO), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), INRIA, and Jacquemard, Florent

Subjects
Polynomial, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES, Computational complexity theory, 2-EXPTIME, Deterministic algorithm, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], EXPTIME, 0102 computer and information sciences, 02 engineering and technology, computational complexity, 01 natural sciences, tree automata, Theoretical Computer Science, Combinatorics, Deterministic automaton, term rewriting, 0202 electrical engineering, electronic engineering, information engineering, Two-way deterministic finite automaton, Tree automaton, Mathematics, Discrete mathematics, Linear bounded automaton, ground reducbility, Pushdown automaton, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 16. Peace & justice, Computer theorem-proving, Computer Science Applications, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, 010201 computation theory & mathematics, 020201 artificial intelligence & image processing, Tree (set theory), inductive theorem proving, complexity, Alternating Turing machine, Computer Science::Formal Languages and Automata Theory, rewriting systems, Information Systems
Abstract

We prove that ground reducibility is EXPTIME-complete in the general case. EXPTIME-hardness is proved by encoding the computations of an alternating Turing machine whose space is polynomially bounded. It is more difficult to show that ground reducibility belongs to DEXPTIME. We associate first an automaton with disequality constraints A/sub R,t/ to a rewrite system R and a term t. This automaton is deterministic and accepts a term u if and only if t is not ground reducible by R. The number of states of A/sub R,t/ is O(2/sup /spl par/R/spl par//spl times//spl par/t/spl par//) and the size of the constraints are polynomial in the size of R,t. Then we prove some new pumping lemmas, using a total ordering on the computations of the automaton. Thanks to these lemmas, we can give an upper bound to the number of distinct subtrees of a minimal successful computation of an automaton with disequality constraints. It follows that emptiness of such an automaton can be decided in time polynomial in the number of its states and exponential in the size of its constraints. Altogether, we get a simply exponential deterministic algorithm for ground reducibility.

Published
2003
Full Text
View/download PDF

45. Decidable Classes of Tree Automata Mixing Local and Global Constraints Modulo Flat Theories

Author

Camille Vacher, Guillem Godoy, Luis Barguñó, Carles Creus, Florent Jacquemard, Universitat Politècnica de Catalunya [Barcelona] (UPC), Synchronous Realtime Processing and Programming of Music Signals (MuTant), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Sciences et Technologies de la Musique et du Son (STMS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Modeling Tree Structures, Machine Learning, and Information Extraction (MOSTRARE), Laboratoire d'Informatique Fondamentale de Lille (LIFL), Université de Lille, Sciences et Technologies-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lille, Sciences Humaines et Sociales-Centre National de la Recherche Scientifique (CNRS)-Université de Lille, Sciences et Technologies-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lille, Sciences Humaines et Sociales-Centre National de la Recherche Scientifique (CNRS)-Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria), Université de Lille, Sciences et Technologies-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lille, Sciences Humaines et Sociales-Centre National de la Recherche Scientifique (CNRS), Universitat Politècnica de Catalunya. Departament de Llenguatges i Sistemes Informàtics, Universitat Politècnica de Catalunya. ALBCOM - Algorismia, Bioinformàtica, Complexitat i Mètodes Formals, Jacquemard, Florent, Inria Paris-Rocquencourt, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Centre National de la Recherche Scientifique (CNRS)

Subjects
FOS: Computer and information sciences, Class (set theory), Computer Science - Logic in Computer Science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], General Computer Science, Formal Languages and Automata Theory (cs.FL), Modulo, Computer Science - Formal Languages and Automata Theory, Equivalence classes, 0102 computer and information sciences, 02 engineering and technology, Type (model theory), 01 natural sciences, Computability and decidability, Tree automata, Theoretical Computer Science, Cardinality, Fragment (logic), Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Automata theory, Mathematics, Discrete mathematics, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.3: Formal Languages/F.4.3.1: Classes defined by grammars or automata (e.g., context-free languages, regular sets, recursive sets), [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Forestry, XML, 16. Peace & justice, Logic in Computer Science (cs.LO), Decidability, Informàtica::Informàtica teòrica [Àrees temàtiques de la UPC], 010201 computation theory & mathematics, 020201 artificial intelligence & image processing, Tree (set theory), State (computer science), Problema de decisió, Computer Science::Formal Languages and Automata Theory
Abstract

We define a class of ranked tree automata TABG generalizing both the tree automata with local tests between brothers 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 the 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., 39 pages, to appear in LMCS journal

Published
2013

46. Rewrite Closure and CF Hedge Automata

Author

Florent Jacquemard, Michaël Rusinowitch, Synchronous Realtime Processing and Programming of Music Signals (MuTant), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Sciences et Technologies de la Musique et du Son (STMS), Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Jacquemard, Florent, Inria Paris-Rocquencourt, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Institut de Recherche et Coordination Acoustique/Musique (IRCAM)-Centre National de la Recherche Scientifique (CNRS)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Theoretical computer science, Nested word, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Rewrite closure, Formal Languages and Automata Theory (cs.FL), Computer science, XQuery Update Facility, Computer Science - Formal Languages and Automata Theory, 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, 01 natural sciences, Tree automata, XML processing, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Regular language, Computer Science - Databases, Hedge automata, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Static typechecking, Tree automaton, Context-free tree languages, Access Control Policies Verification, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Programming language, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Databases (cs.DB), 020207 software engineering, Hedge (linguistics), Logic in Computer Science (cs.LO), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Closure (mathematics), 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Programming Languages, Tree (set theory), Rewriting, computer, Computer Science::Formal Languages and Automata Theory
Abstract

We introduce an extension of hedge automata called bidimensional context-free hedge automata, proposing a new uniform representation of vertical and horizontal computation steps in unranked ordered trees. The class recognized languages 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.

Published
2012

Catalog

Books, media, physical & digital resources
See catalog results