Author: "Verification in databases (DAHU)" - Searchworks@Jio Institute Digital Library Search Results

Your search keyword '"Verification in databases (DAHU)"' showing total 156 results

Start Over Author "Verification in databases (DAHU)"

156 results on '"Verification in databases (DAHU)"'

1. Bottom-up automata on data trees and vertical XPath

Author: Diego Figueira, Luc Segoufin, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS), 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), 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), Value from Data (VALDA ), Département d'informatique de l'École normale supérieure (DI-ENS), École normale supérieure - Paris (ENS Paris), 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), 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 de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), 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 ), Value from Data ( VALDA ), Département d'informatique de l'École normale supérieure ( DI-ENS ), École normale supérieure - Paris ( ENS Paris ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -Centre National de la Recherche Scientifique ( CNRS ) -École normale supérieure - Paris ( ENS Paris ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -Centre National de la Recherche Scientifique ( CNRS ) -Inria de Paris, Institut National de Recherche en Informatique et en Automatique ( Inria ), Département d'informatique - ENS Paris (DI-ENS), 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 de Paris, Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-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)-École normale supérieure - Paris (ENS-PSL), and Dürr, Christoph
Subjects: FOS: Computer and information sciences, [INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC], Data processing Computer science, [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], [INFO.INFO-DS] Computer Science [cs]/Data Structures and Algorithms [cs.DS], 0102 computer and information sciences, 02 engineering and technology, Decidability, 01 natural sciences, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Computer Science - Databases, Bottom-up tree automata, 0202 electrical engineering, electronic engineering, information engineering, XPath, [ INFO.INFO-CL ] Computer Science [cs]/Computation and Language [cs.CL], [ INFO.INFO-DS ] Computer Science [cs]/Data Structures and Algorithms [cs.DS], Computer Science::Databases, 000 Computer science, knowledge, general works, Databases (cs.DB), Data trees, [ INFO.INFO-CC ] Computer Science [cs]/Computational Complexity [cs.CC], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, Decidability, XPath, Data trees, Bottom-up tree automata, Computer Science, [INFO.INFO-CC] Computer Science [cs]/Computational Complexity [cs.CC], 020201 artificial intelligence & image processing, ddc:004, Computer Science::Formal Languages and Automata Theory
Abstract: A data tree is a finite tree whose every node carries a label from a finite alphabet and a datum from some infinite domain. We introduce a new model of automata over unranked data trees with a decidable emptiness problem. It is essentially a bottom-up alternating automaton with one register that can store one data value and can be used to perform equality tests with the data values occurring within the subtree of the current node. We show that it captures the expressive power of the vertical fragment of XPath - containing the child, descendant, parent and ancestor axes - obtaining thus a decision procedure for its satisfiability problem., Logical Methods in Computer Science ; Volume 13, Issue 4 ; 1860-5974
Published: 2017
Full Text: View/download PDF

2. Ambition numérique

Author: Abiteboul, Serge, Andrieux, Nathalie, Balagué, Christine, Beauvallet, Godefroy, Blecher, Ludovic, Bloch-Pujo, Nathalie, Briand, Michel, Cruz, Virginia, Daloz, Pascal, Delbourg-Delphis, Marylène, Distinguin, Stéphane, Ekeland, Marie, Fauvel, Virginie, Garcia, Cyril, Harris, Audrey, Jutand, Francis, Kaplan, Daniel, Le Ny, Florence, Nitot, Tristan, Pène, Sophie, Peugeot, Valérie, Rouyrès, Lara, Rudelle, Jean-Baptiste, Russeil, Cécile, Stiegler, Bernard, Thieulin, Benoît, Tessier, Marc, Vallée, Brigitte, 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), Lagardère SCA [Paris], Institut Mines-Télécom [Paris] (IMT), Télécom ParisTech, Fonds Google–AIPG pour l’Innovation Numérique de la presse – FINP (Google-AIPG - FINP), Hachette Tourisme [Vanves], Télécom Bretagne - Brest, Télécom Bretagne, Interaction Design Sight & lab [Paris] (IDSL), École polytechnique (X), Dassault Systèmes, Talent Circles, Fabernovel [Paris], Daphni [Paris], Allianz, Capgemini Consulting [Paris], Soubis [Paris], Fondation internet nouvelle génération [Paris] (FING), Telecom Orange, Cozy Cloud, Conseil National du Numerique [Paris] (CNNum), Université Paris Descartes - Paris 5 (UPD5), Orange Labs [Issy les Moulineaux], France Télécom, Auteur indépendant, Criteo [Paris], Ubisoft, Institut de Recherche et d'Innovation (IRI), Centre Pompidou, La Netscouade [Paris], Forum des images [Paris], Equipe AMACC - Laboratoire GREYC - UMR6072, Groupe de Recherche en Informatique, Image, Automatique et Instrumentation de Caen (GREYC), Université de Caen Normandie (UNICAEN), Normandie Université (NU)-Normandie Université (NU)-École Nationale Supérieure d'Ingénieurs de Caen (ENSICAEN), Normandie Université (NU)-Centre National de la Recherche Scientifique (CNRS)-Université de Caen Normandie (UNICAEN), Normandie Université (NU)-Centre National de la Recherche Scientifique (CNRS), Conseil national du Numérique, Groupe de Recherche en Informatique, Image et Instrumentation de Caen (GREYC), Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Ingénieurs de Caen (ENSICAEN), Normandie Université (NU)-Normandie Université (NU)-Université de Caen Normandie (UNICAEN), Normandie Université (NU)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Ingénieurs de Caen (ENSICAEN), Normandie Université (NU), 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 ), Institut Mines-Télécom [Paris], Fonds Google–AIPG pour l’Innovation Numérique de la presse – FINP ( Google-AIPG - FINP ), Interaction Design Sight & lab [Paris] ( IDSL ), École polytechnique ( X ), Fondation internet nouvelle génération [Paris] ( FING ), Conseil National du Numerique [Paris] ( CNNum ), Université Paris Descartes - Paris 5 ( UPD5 ), Institut de Recherche et d'Innovation ( IRI ), Groupe de Recherche en Informatique, Image, Automatique et Instrumentation de Caen ( GREYC ), Université de Caen Normandie ( UNICAEN ), Normandie Université ( NU ) -Normandie Université ( NU ) -Ecole Nationale Supérieure d'Ingénieurs de Caen ( ENSICAEN ), Normandie Université ( NU ) -Centre National de la Recherche Scientifique ( CNRS ) -Université de Caen Normandie ( UNICAEN ), and Normandie Université ( NU ) -Centre National de la Recherche Scientifique ( CNRS )
Subjects: InformationSystems_GENERAL, InformationSystems_MODELSANDPRINCIPLES, GeneralLiterature_INTRODUCTORYANDSURVEY, [SHS.INFO]Humanities and Social Sciences/Library and information sciences, [ SHS.INFO ] Humanities and Social Sciences/Library and information sciences, ComputingMilieux_PERSONALCOMPUTING, Conseil national du numérique, Ambition numérique, GeneralLiterature_MISCELLANEOUS
Abstract: Rapport remis au premier ministre
Published: 2015

3. Decidability of Downward XPath

Author: Diego Figueira, Laboratoire Spécification et Vérification [Cachan] ( LSV ), École normale supérieure - Cachan ( ENS Cachan ) -Centre National de la Recherche Scientifique ( CNRS ), Laboratory for the Foundations of Computer Science [Edinburgh] ( LFCS ), University of Edinburgh, 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 ), The author acknowledges the financial support of the Future and Emerging Technologies (FET) programmewithin the Seventh Framework Programme for Research of the European Commission, under the FET-Opengrant agreement FOX, number FP7-ICT-233599., Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Laboratory for the Foundations of Computer Science [Edinburgh] (LFCS), 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, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES, General Computer Science, Logic, EXPTIME, 0102 computer and information sciences, 02 engineering and technology, [INFO.INFO-DM]Computer Science [cs]/Discrete Mathematics [cs.DM], 01 natural sciences, data values, Theoretical Computer Science, Combinatorics, emptiness, Fragment (logic), [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 020204 information systems, Kleene star, 0202 electrical engineering, electronic engineering, information engineering, XPath, Computer Science::Databases, downward data automata, Mathematics, Discrete mathematics, infinite alphabet, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], InformationSystems_DATABASEMANAGEMENT, [ INFO.INFO-DM ] Computer Science [cs]/Discrete Mathematics [cs.DM], XML, Path expression, Satisfiability, Decidability, Computational Mathematics, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, [ INFO.INFO-DB ] Computer Science [cs]/Databases [cs.DB], Closure (mathematics), 010201 computation theory & mathematics, satisfiability, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, DD automata, [ INFO.INFO-FL ] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], ComputingMethodologies_DOCUMENTANDTEXTPROCESSING, data tree, [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO], Boolean satisfiability problem, Computer Science::Formal Languages and Automata Theory
Abstract: International audience; We investigate the satisfiability problem for downward-XPath, the fragment of XPath that includes the child and descendant axes, and tests for (in)equality of attributes' values. We prove that this problem is decidable, ExpTime-complete. These bounds also hold when path expressions allow closure under the Kleene star operator. To obtain these results, we introduce a Downward Data automata model (DD automata) over trees with data, which has a decidable emptiness problem. Satisfiability of downward-XPath can be reduced to the emptiness problem of DD automata and hence its decidability follows. Although downward-XPath does not include any horizontal axis, DD automata are more expressive and can perform some horizontal tests. Thus, we show that the satisfiability remains in ExpTime even in the presence of the regular constraints expressible by DD automata. However, the same problem in the presence of any regular constraint is known to have a non-primitive recursive complexity. Finally, we give the exact complexity of the satisfiability problem for several fragments of downward-XPath.
Published: 2012
Full Text: View/download PDF

4. Alternating register automata on finite words and trees

Author: Joseph Y. Halpern, Riccardo Pucella, Laboratory for the Foundations of Computer Science [Edinburgh] ( LFCS ), University of Edinburgh, 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 ), Work supported by the Future and Emerging Technologies (FET) programme within the Seventh FrameworkProgramme for Research of the European Commission, under the FET-Open grant agreement FOX,number FP7-ICT-233599., Laboratory for the Foundations of Computer Science [Edinburgh] (LFCS), 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, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: FOS: Computer and information sciences, TheoryofComputation_MISCELLANEOUS, Computer Science - Logic in Computer Science, General Computer Science, Formal Languages and Automata Theory (cs.FL), Computer science, Security protocol analysis, Computer Science - Formal Languages and Automata Theory, 0102 computer and information sciences, 02 engineering and technology, [INFO.INFO-DM]Computer Science [cs]/Discrete Mathematics [cs.DM], Computer security, computer.software_genre, 01 natural sciences, I.7.2, H.2.3, H.2.3, Theoretical Computer Science, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Computer Science - Databases, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Abstraction (linguistics), [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Probabilistic logic, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Databases (cs.DB), [ INFO.INFO-DM ] Computer Science [cs]/Discrete Mathematics [cs.DM], Cryptographic protocol, Adversary, 16. Peace & justice, Logic in Computer Science (cs.LO), [ INFO.INFO-DB ] Computer Science [cs]/Databases [cs.DB], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, [ INFO.INFO-FL ] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO], computer, Adversary model, Computer Science::Formal Languages and Automata Theory
Abstract: International audience; We study alternating register automata on data words and data trees in relation to logics. A data word (resp. data tree) is a word (resp. tree) whose every position carries a label from a finite alphabet and a data value from an infinite domain. We investigate one-way automata with alternating control over data words or trees, with one register for storing data and comparing them for equality. This is a continuation of the study started by Demri, Lazi´cLazi´c and Jurdzi´nskiJurdzi´nski. From the standpoint of register automata models, this work aims at two objectives: (1) simplifying the existent decidability proofs for the emptiness problem for alternating register automata; and (2) exhibiting decidable extensions for these models. From the logical perspective, we show that (a) in the case of data words, satisfiability of LTL with one register and quantification over data values is decidable; and (b) the satisfiability problem for the so-called forward fragment of XPath on xml documents is decidable, even in the presence of DTDs and even of key constraints. The decidability is obtained through a reduction to the automata model introduced. This fragment contains the child, descendant, next-sibling and following-sibling axes, as well as data equality and inequality tests.
Published: 2012
Full Text: View/download PDF

5. Nondeterminism and An Abstract Formulation of Nečiporuk’s Lower Bound Method

Author: Nathan Grosshans, Pierre McKenzie, Luc Segoufin, Paul Beame, University of Washington [Seattle], École normale supérieure - Cachan (ENS Cachan), Université de Montréal (UdeM), 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), NSF grants CCF-1217099 and CCF-1524246., Grants from Digiteo France., NSERC of Canada., and 'Chaire DIGITEO, ENS Cachan - École Polytechnique'.
Subjects: [INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC], Discrete mathematics, Branching programs, Sublinear function, Computation, 1. No poverty, binary formulas, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Upper and lower bounds, Theoretical Computer Science, Nondeterministic algorithm, Computer Science - Computational Complexity, Computational Theory and Mathematics, 010201 computation theory & mathematics, 0202 electrical engineering, electronic engineering, information engineering, ACM: F.: Theory of Computation/F.1: COMPUTATION BY ABSTRACT DEVICES/F.1.1: Models of Computation/F.1.1.5: Unbounded-action devices (e.g., cellular automata, circuits, networks of machines), limited nondeterminism, 020201 artificial intelligence & image processing, Parity (mathematics), Mathematics
Abstract: A formulation of Nečiporuk’s lower bound method slightly more inclusive than the usual complexity-measure-specific formulation is presented. Using this general formulation, limitations to lower bounds achievable by the method are obtained for several computation models, such as branching programs and Boolean formulas having access to a sublinear number of nondeterministic bits. In particular, it is shown that any lower bound achievable by the method of Nečiporuk for the size of nondeterministic and parity branching programs is at most O ( n 3/2 /log n ).
Published: 2016
Full Text: View/download PDF

6. Nonelementary Complexities for Branching VASS, MELL, and Extensions

Author: Ranko Lazić, Sylvain Schmitz, University of Warwick [Coventry], 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), and ANR-11-BS02-0001,REACHARD,Problèmes d'accessiblité difficiles pour les systèmes à compteurs(2011)
Subjects: FOS: Computer and information sciences, Computer Science - Logic in Computer Science, General Computer Science, Logic, Zeroth-order logic, vector addition systems, Intermediate logic, Intuitionistic logic, fast-growing complexity, Upper and lower bounds, QA76, Theoretical Computer Science, Combinatorics, Branching (linguistics), F.2.2, F.4.1, Linear temporal logic, Fragment (logic), Reachability, Computer Science::Logic in Computer Science, linear logic, QA, Autoepistemic logic, Mathematics, Propositional variable, Discrete mathematics, Second-order logic, Multiplicative function, Modal μ-calculus, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic, 16. Peace & justice, Linear logic, Logic in Computer Science (cs.LO), Exponential function, Computational Mathematics, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, ACM: F.: Theory of Computation/F.2: ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY/F.2.2: Nonnumerical Algorithms and Problems, Affine transformation
Abstract: We study the complexity of reachability problems on branching extensions of vector addition systems, which allows us to derive new non-elementary complexity bounds for fragments and variants of propositional linear logic. We show that provability in the multiplicative exponential fragment is Tower-hard already in the affine case -- and hence non-elementary. We match this lower bound for the full propositional affine linear logic, proving its Tower-completeness. We also show that provability in propositional contractive linear logic is Ackermann-complete., Comment: Fixed Fig. 3 thanks to Hiromi Tanaka
Published: 2015
Full Text: View/download PDF

7. Highly Expressive Query Languages for Unordered Data Trees

Author: Serge Abiteboul, Victor Vianu, Pierre Bourhis, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Linking Dynamic Data (LINKS), Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-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), Department of Computer Science and Engineering [San Diego] (CSE-UCSD), University of California [San Diego] (UC San Diego), University of California-University of California, Université Paris-Sud - Paris 11 (UP11), University of California (UC), European Project: 226513,EC:FP7:ERC,ERC-2008-AdG,WEBDAM(2008), University of California, Department of Computer Science and Engineering [Univ California San Diego] (CSE - UC San Diego), and University of California (UC)-University of California (UC)
Subjects: Theoretical computer science, computer.internet_protocol, Computer science, 0102 computer and information sciences, 02 engineering and technology, Query language, computer.software_genre, 01 natural sciences, Computation Theory & Mathematics, Theoretical Computer Science, Set (abstract data type), symbols.namesake, Turing completeness, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Programming language, Applied Mathematics, Expressiveness, Abstract family of languages, Computation Theory and Mathematics, Data trees, XML, Ontology language, Object (computer science), Cone (formal languages), Nondeterministic algorithm, Computational Theory and Mathematics, 010201 computation theory & mathematics, Theory of computation, Query languages, symbols, 020201 artificial intelligence & image processing, Distributed Computing, computer
Abstract: International audience; We study highly expressive query languages for unordered data trees, using as formal vehicles Active XML and extensions of languages in the while family. All languages may be seen as adding some form of control on top of a set of basic pattern queries. The results highlight the impact and interplay of different factors: the expressive power of basic queries, the embedding of computation into data (as in Active XML), and the use of deterministic vs. nondeterministic control. All languages are Turing complete, but not necessarily query complete in the sense of Chandra and Harel. Indeed, we show that some combinations of features yield serious limitations, analogous to FO-k definability in the relational context. On the other hand, the limitations come with benefits such as the existence of powerful normal forms providing opportunities for optimization. Other languages are ``almost'' complete, but fall short because of subtle limitations reminiscent of the copy elimination problem in object databases.
Published: 2015
Full Text: View/download PDF

8. The Complexity of Diagnosability and Opacity Verification for Petri Nets

Author: Béatrice Bérard, Stefan Haar, Sylvain Schmitz, Stefan Schwoon, Modélisation et Vérification (MoVe), Laboratoire d'Informatique de Paris 6 (LIP6), Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Modeling and Exploitation of Interaction and Concurrency (MEXICO), É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), Verification in databases (DAHU), Wil van der Aalst, Eike Best, LIP6, and Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Opacity, 0209 industrial biotechnology, Theoretical computer science, Computer science, Reachability problem, Distributed computing, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.3: Formal Languages/F.4.3.3: Decision problems, Petri nets, 02 engineering and technology, Fault (power engineering), Diagnosability, Theoretical Computer Science, 020901 industrial engineering & automation, Reachability, ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.3: Formal methods, 0202 electrical engineering, electronic engineering, information engineering, Mathematics, Algebra and Number Theory, Verification, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Complexity, Petri net, ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs, 020202 computer hardware & architecture, Undecidable problem, Computational Theory and Mathematics, 020201 artificial intelligence & image processing, Finite state systems, Information Systems
Abstract: International audience; Diagnosability and opacity are two well-studied problems in discrete-event systems. We revisit these two problems with respect to expressiveness and complexity issues. We first relate different notions of diagnosability and opacity. We consider in particular fairness issues and extend the definition of Germanos et al. [ACM TECS, 2015] of weakly fair diagnosability for safe Petri nets to general Petri nets and to opacity questions. Second, we provide a global picture of complexity results for the verification of diagnosability and opacity. We show that diagnosability is NL-complete for finite state systems, PSPACE-complete for safe Petri nets (even with fairness), and EXPSPACE-complete for general Petri nets without fairness, while non diagnosability is inter-reducible with reachability when fault events are not weakly fair. Opacity is ESPACE-complete for safe Petri nets (even with fairness) and undecidable for general Petri nets already without fairness.
Published: 2017
Full Text: View/download PDF

9. A survey on guarded negation

Author: Luc Segoufin, 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, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: Microbiology (medical), Discrete mathematics, Immunology, 0102 computer and information sciences, 02 engineering and technology, Fixed point, Computer Science::Computational Geometry, 16. Peace & justice, 01 natural sciences, Expressive power, Existentialism, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Logical framework, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Negation, 010201 computation theory & mathematics, 020204 information systems, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Free variables and bound variables, 0202 electrical engineering, electronic engineering, information engineering, Calculus, Immunology and Allergy, Mathematics
Abstract: International audience; We consider a logical framework building on existential positive formulas and then adding guarded negations and guarded fixpoints, where the guards are atomic formulas containing all free variables. The resulting first-order and fixpoint logics turn out to have nice algorithmic properties and nice expressive power. We survey some of them.
Published: 2017

10. Constant Delay Enumeration for FO Queries over Databases with Local Bounded Expansion

Author: Segoufin, Luc, Vigny, Alexandre, Segoufin, Luc, Value from Data (VALDA ), Département d'informatique - ENS Paris (DI-ENS), 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 de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), 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), É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 de Paris, Département d'informatique de l'École normale supérieure (DI-ENS), École normale supérieure - Paris (ENS Paris), 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: 000 Computer science, knowledge, general works, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], enumeration, 010201 computation theory & mathematics, [INFO.INFO-CL] Computer Science [cs]/Computation and Language [cs.CL], 020204 information systems, Computer Science, 0202 electrical engineering, electronic engineering, information engineering, first-order queries, constant delay, Computer Science::Databases
Abstract: International audience; We consider the evaluation of first-order queries over classes of databases with local bounded expansion. This class was introduced by Nesetril and Ossona de Mendez and generalizes many well known classes of databases, such as bounded degree, bounded tree width or bounded expansion. It is known that over classes of databases with local bounded expansion, first-order sentences can be evaluated in pseudo-linear time (pseudo-linear time means that for all epsilon there exists an algorithm working in time O(n^{1+epsilon)). Here, we investigate other scenarios, where queries are not sentences. We show that first-order queries can be enumerated with constant delay after a pseudo-linear preprocessing over any class of databases having locally bounded expansion. We also show that, in this context, counting the number of solutions can be done in pseudo-linear time.
Published: 2017

11. Thymeflow, An Open-Source Personal Knowledge Base System

Author: Montoya, David, Pellissier Tanon, Thomas, Abiteboul, Serge, Senellart, Pierre, Suchanek, Fabian, 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), École normale supérieure de Lyon (ENS de Lyon), Value from Data (VALDA ), 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 de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), 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), Laboratoire Traitement et Communication de l'Information (LTCI), Télécom ParisTech-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS), Thymeflow, École normale supérieure - Lyon (ENS Lyon), 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 de Paris, Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), Département d'informatique de l'École normale supérieure (DI-ENS), École normale supérieure - Paris (ENS Paris), 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-DB]Computer Science [cs]/Databases [cs.DB]
Abstract: The typical Internet user has data spread over several devices and across several online systems. In this paper, we introduce a novel framework for integrating a user's data from different sources into a single Knowledge Base. Our framework integrates data of different kinds into a coherent whole, starting with email messages, calendar, contacts, and location history. We show how event periods in the user's location data can be detected, how they can be aligned with events from the calendar, and how they can be linked to relevant emails. This allows users to query their personal information within and across different dimensions, and to perform analytics over their emails, events, and locations. To this end, our system extends the schema.org vocabulary and provides a SPARQL interface.
Published: 2016

12. Thymeflow, A Personal Knowledge Base with Spatio-Temporal Data

Author: David Montoya, Serge Abiteboul, Fabian M. Suchanek, Thomas Pellissier Tanon, ENGIE, 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), École normale supérieure de Lyon (ENS de Lyon), Télécom ParisTech, and École normale supérieure - Lyon (ENS Lyon)
Subjects: Information retrieval, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Computer science, business.industry, Event (computing), querying, 02 engineering and technology, computer.software_genre, Temporal database, Knowledge base, Analytics, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, The Internet, Personal knowledge base, business, personal information, computer, Personally identifiable information, data integration, open-source, Data integration
Abstract: International audience; The typical Internet user has data spread over several devices and across several online systems. We demonstrate an open-source system for integrating user's data from different sources into a single Knowledge Base. Our system integrates data of different kinds into a coherent whole, starting with email messages, calendar, contacts, and location history. It is able to detect event periods in the user's location data and align them with calendar events. We will demonstrate how to query the system within and across different dimensions, and perform analytics over emails, events, and locations.
Published: 2016
Full Text: View/download PDF

13. A Sequent Calculus for a Modal Logic on Finite Data Trees

Author: Baelde, David, Lunel, Simon, Schmitz, Sylvain, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Tim, Events and Architectures (TEA), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), 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)-Télécom Bretagne-CentraleSupélec-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), Leverhulme Trust visiting professorship VP1-2014-041, Jean-Marc Talbot, Laurent Regnier, ANR-14-CE28-0005,PRODAQ,Systèmes de preuves pour requêtes avec données(2014), 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), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-É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), and Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)
Subjects: 000 Computer science, knowledge, general works, ACM: F.: Theory of Computation/F.2: ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY/F.2.2: Nonnumerical Algorithms and Problems/F.2.2.0: Complexity of proof procedures, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.5: Modal logic, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, proof systems, Computer Science, 0202 electrical engineering, electronic engineering, information engineering, XPath, 020201 artificial intelligence & image processing, ACM: H.: Information Systems/H.2: DATABASE MANAGEMENT/H.2.3: Languages/H.2.3.3: Query languages, complexity, Computer Science::Formal Languages and Automata Theory, modal logic
Abstract: International audience; We investigate the proof theory of a modal fragment of XPath equipped with data (in)equality tests over finite data trees, i.e. over finite unranked trees where nodes are labelled with both a symbol from a finite alphabet and a single data value from an infinite domain. We present a sound and complete sequent calculus for this logic, which yields the optimal PSPACE complexity bound for its validity problem.
Published: 2016
Full Text: View/download PDF

14. Asymptotic Determinacy of Path Queries using Union-of-Paths Views

Author: Nadime Francis, 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), Arenas, Marcelo, and Ugarte, Martín
Subjects: Determinacy, Graph databases, Rewriting, ACM: H.: Information Systems/H.2: DATABASE MANAGEMENT/H.2.4: Systems/H.2.4.5: Query processing, Existential quantification, 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, 01 natural sciences, Theoretical Computer Science, Combinatorics, Set (abstract data type), 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Path queries, [INFO]Computer Science [cs], Computer Science::Databases, Mathematics, Discrete mathematics, 000 Computer science, knowledge, general works, Graph database, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Computer Science::Information Retrieval, InformationSystems_DATABASEMANAGEMENT, 16. Peace & justice, Computational Theory and Mathematics, 010201 computation theory & mathematics, Computer Science, Path (graph theory), Theory of computation, Graph (abstract data type), ACM: H.: Information Systems/H.2: DATABASE MANAGEMENT/H.2.3: Languages/H.2.3.3: Query languages, computer, Views
Abstract: International audience; We consider the view determinacy problem over graph databases for queries defined as (possibly infinite) unions of path queries. These queries select pairs of nodes in a graph that are connected through a path whose length falls in a given set. A view specification is a set of such queries. We say that a view specification V determines a query Q if, for all databases D, the answers to V on D contain enough information to answer Q. Our main result states that, given a view V, there exists an explicit bound that depends on V such that we can decide the determinacy problem for all queries that ask for a path longer than this bound, and provide first-order rewritings for the queries that are determined. We call this notion asymptotic determinacy. As a corollary, we can also compute the set of almost all path queries that are determined by V.
Published: 2016
Full Text: View/download PDF

15. The Complexity of Coverability in ν-Petri Nets

Author: Ranko Lazić, Sylvain Schmitz, Centre for Discrete Mathematics and its Applications [Warwick] (DIMAP), University of Warwick [Coventry], 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), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), EPSRC grant EP/M011801/1, Leverhulme Trust Visiting Professorship VP1-2014-041, and ANR-14-CE28-0005,PRODAQ,Systèmes de preuves pour requêtes avec données(2014)
Subjects: Discrete mathematics, Computer science, Semantics (computer science), [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, 02 engineering and technology, Petri net, 01 natural sciences, Ackermann function, Upper and lower bounds, Rotation formalisms in three dimensions, Well-quasi-order, Formal verification, ACM: F.: Theory of Computation/F.2: ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY/F.2.2: Nonnumerical Algorithms and Problems, Well-structured transition system, 010201 computation theory & mathematics, Completeness (order theory), 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, QA, Order ideal, Fast-growing complexity, Analysis of algorithms
Abstract: We show that the coverability problem in ν-Petri nets is complete for ‘double Ackermann’ time, thus closing an open complexity gap between an Ackermann lower bound and a hyper-Ackermann upper bound. The coverability problem captures the verification of safety properties in this nominal extension of Petri nets with name management and fresh name creation. Our completeness result establishes ν-Petri nets as a model of intermediate power among the formalisms of nets enriched with data, and relies on new algorithmic insights brought by the use of well-quasi-order ideals.Categories and Subject Descriptors F.2.2 [Analysis of Algorithms and Problem Complexity]: Nonnumerical Algorithms and Problems
Published: 2016
Full Text: View/download PDF

16. Verification of Hierarchical Artifact Systems

Author: Yuliang Li, Alin Deutsch, Victor Vianu, Department of Computer Science and Engineering [San Diego] (CSE-UCSD), University of California [San Diego] (UC San Diego), University of California-University of California, 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), NSF, ACM, Dahu, Department of Computer Science and Engineering [Univ California San Diego] (CSE - UC San Diego), and University of California (UC)-University of California (UC)
Subjects: FOS: Computer and information sciences, Hierarchy, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Theoretical computer science, Computer science, Concurrency, tem- poral logic, Databases (cs.DB), Context (language use), business process management, 02 engineering and technology, Artifact (software development), Static analysis, Computer Science - Databases, 020204 information systems, Quantifier elimination, data-centric workflows, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, IBM, verification, Information Systems, Foreign key
Abstract: Data-driven workflows, of which IBM's Business Artifacts are a prime exponent, have been successfully deployed in practice, adopted in industrial standards, and have spawned a rich body of research in academia, focused primarily on static analysis. The present work represents a significant advance on the problem of artifact verification, by considering a much richer and more realistic model than in previous work, incorporating core elements of IBM's successful Guard-Stage-Milestone model. In particular, the model features task hierarchy, concurrency, and richer artifact data. It also allows database key and foreign key dependencies, as well as arithmetic constraints. The results show decidability of verification and establish its complexity, making use of novel techniques including a hierarchy of Vector Addition Systems and a variant of quantifier elimination tailored to our context., Full version of the accepted PODS paper
Published: 2016
Full Text: View/download PDF

17. Data, Responsibly: Fairness, Neutrality and Transparency in Data Analysis

Author: Stoyanovich, Julia, Abiteboul, Serge, Miklau, Gerome, Drexel University, 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), Department of Computer Science [Amherst], University of Massachusetts [Amherst] (UMass Amherst), and University of Massachusetts System (UMASS)-University of Massachusetts System (UMASS)
Subjects: [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB]
Abstract: International audience; Big data technology holds incredible promise of improving people's lives, accelerating scientific discovery and innovation , and bringing about positive societal change. Yet, if not used responsibly, this technology can propel economic inequality , destabilize global markets and affirm systemic bias. While the potential benefits of big data are well-accepted, the importance of using these techniques in a fair and transparent manner is rarely considered. The primary goal of this tutorial is to draw the attention of the data management community to the important emerging subject of responsible data management and analysis. We will offer our perspective on the issue, will give an overview of existing technical work, primarily from the data mining and algorithms communities, and will motivate future research directions.
Published: 2016

18. A formal study of collaborative access control in distributed datalog

Author: Abiteboul, Serge, Bourhis, Pierre, Vianu, Victor, 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), Linking Dynamic Data (LINKS), Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Department of Computer Science and Engineering [Univ California San Diego] (CSE - UC San Diego), University of California [San Diego] (UC San Diego), University of California (UC)-University of California (UC), Wim Martens, Thomas Zeume, Department of Computer Science and Engineering [San Diego] (CSE-UCSD), and University of California-University of California
Subjects: 000 Computer science, knowledge, general works, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Computer Science, 0202 electrical engineering, electronic engineering, information engineering, 020206 networking & telecommunications, 020201 artificial intelligence & image processing, 02 engineering and technology, 16. Peace & justice
Abstract: International audience; We formalize and study a declaratively specified collaborative access control mechanism for data dissemination in a distributed environment. Data dissemination is specified using distributed datalog. Access control is also defined by datalog-style rules, at the relation level for extensional relations, and at the tuple level for intensional ones, based on the derivation of tuples. The model also includes a mechanism for " declassifying " data, that allows circumventing overly restrictive access control. We consider the complexity of determining whether a peer is allowed to access a given fact, and address the problem of achieving the goal of disseminating certain information under some access control policy. We also investigate the problem of information leakage, which occurs when a peer is able to infer facts to which the peer is not allowed access by the policy. Finally, we consider access control extended to facts equipped with provenance information, motivated by the many applications where such information is required. We provide semantics for access control with provenance, and establish the complexity of determining whether a peer may access a given fact together with its provenance. This work is motivated by the access control of the Webdamlog system, whose core features it formalizes.
Published: 2016

19. Coverability Trees for Petri Nets with Unordered Data

Author: Piotr Hofman, Ranko Lazić, Sylvain Schmitz, Jérôme Leroux, Patrick Totzke, Sławomir Lasota, Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Faculty of Mathematics, Informatics, and Mechanics [Warsaw] (MIMUW), University of Warsaw (UW), Centre for Discrete Mathematics and its Applications [Warwick] (DIMAP), University of Warwick [Coventry], Department of Computer Science [Warwick], Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-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), Polish National Science Centre grant 2013/09/B/ST6/01575, Labex Digicosme, Université Paris-Saclay, project VERICONISS, Polish National Science Centre grant 2012/07/B/ST6/01497, Leverhulme Trust Visiting Professorship VP1-2014-041, EPSRC grant EP/M011801/1, ANR-14-CE28-0005,PRODAQ,Systèmes de preuves pour requêtes avec données(2014), and Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)
Subjects: TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES, Theoretical computer science, Programming language, Computer science, Data domain, Carry (arithmetic), Limit ordinal, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, 02 engineering and technology, Extension (predicate logic), Petri net, 16. Peace & justice, computer.software_genre, 01 natural sciences, Data vector, QA76, 010201 computation theory & mathematics, 0202 electrical engineering, electronic engineering, information engineering, Countable set, 020201 artificial intelligence & image processing, computer
Abstract: International audience; We study an extension of classical Petri nets where tokens carry values from a countable data domain, that can be tested for equality upon firing transitions. These Unordered Data Petri Nets (UDPN) are well-structured and therefore allow generic decision procedures for several verification problems including coverability and boundedness. We show how to construct a finite representation of the coverability set in terms of its ideal decomposition. This not only provides an alternative method to decide coverability and boundedness, but is also an important step towards deciding the reachability problem. This also allows to answer more precise questions about the reachability set, for instance whether there is a bound on the number of tokens on a given place (place boundedness), or if such a bound exists for the number of different data values carried by tokens (place width boundedness). We provide matching Hyper-Ackermann bounds on the size of cover-ability trees and on the running time of the induced decision procedures.
Published: 2016
Full Text: View/download PDF

20. Analyse des données et choix de société

Author: Abiteboul, Serge, 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), and Abiteboul, Serge
Subjects: responsabilité, informatique, [INFO]Computer Science [cs], [SHS] Humanities and Social Sciences, [INFO] Computer Science [cs], [SHS]Humanities and Social Sciences
Abstract: National audience; Le programme informatique, de plus en plus au cœur de la gouvernance de notre société, est souvent mis au banc des accusés. Notre propos est ici d'expliquer qu’on est en droit d'attendre des algorithmes des transformations extrêmement positives de cette société, et qu’on est également en droit d'exiger d’eux qu'ils aient un comportement véritablement responsable.
Published: 2016

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

Author: Luc Segoufin, Jerémie Dimino, Florent Jacquemard, 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), 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, and École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)
Subjects: General Computer Science, 010102 general mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Computer Science - Formal Languages and Automata Theory, 02 engineering and technology, Decision problem, 01 natural sciences, Satisfiability, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Theoretical Computer Science, First-order logic, Automaton, Combinatorics, Branching (linguistics), Tree (data structure), Reachability, 0202 electrical engineering, electronic engineering, information engineering, 0101 mathematics, Test data, Mathematics
Abstract: International audience; 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 FO 2 (
Published: 2016
Full Text: View/download PDF

22. Automata Column: The Complexity of Reachability in Vector Addition Systems

Author: Schmitz, Sylvain, 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), and École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)
Subjects: ACM: F.: Theory of Computation/F.2: ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY/F.2.2: Nonnumerical Algorithms and Problems, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs
Abstract: International audience; The program of the 30th Symposium on Logic in Computer Science held in 2015 in Kyoto included two contributions on the computational complexity of the reachability problem for vector addition systems: Blondin, Finkel, Göller, Haase, and McKenzie [2015] attacked the problem by providing the first tight complexity bounds in the case of dimension 2 systems with states, while Leroux and Schmitz [2015] proved the first complexity upper bound in the general case. The purpose of this column is to present the main ideas behind these two results, and more generally survey the current state of affairs.
Published: 2016
Full Text: View/download PDF

23. Data, Responsibly (Dagstuhl Seminar 16291)

Author: Abiteboul, Serge, Miklau, Gerome, Stoyanovich, Julia, Weikum, Gerhard, 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), Department of Computer Science [Amherst], University of Massachusetts [Amherst] (UMass Amherst), University of Massachusetts System (UMASS)-University of Massachusetts System (UMASS), Drexel University, and Max Planck Institute for Informatics [Saarbrücken]
Subjects: Ethics, Diversity, Fairness, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], 000 Computer science, knowledge, general works, Personal information management, Data science education, 4. Education, Data analysis, 020206 networking & telecommunications, 02 engineering and technology, Machine bias, Responsible research, Transparency, Data management, Data responsibly, Big data, Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Accountability, Data mining, Responsible innovation
Abstract: International audience; Big data technology promises to improve people's lives, accelerate scientific discovery and innovation, and bring about positive societal change. Yet, if not used responsibly, large-scale data analysis and data-driven algorithmic decision-making can increase economic inequality, affirm systemic bias, and even destabilize global markets. While the potential benefits of data analysis techniques are well accepted, the importance of using them responsibly - that is, in accordance with ethical and moral norms, and with legal and policy considerations - is not yet part of the mainstream research agenda in computer science. Dagstuhl Seminar "Data, Responsibly" brought together academic and industry researchers from several areas of computer science, including a broad representation of data management, but also data mining, security/privacy, and computer networks, as well as social sciences researchers, data journalists, and those active in government think-tanks and policy initiatives. The goals of the seminar were to assess the state of data analysis in terms of fairness, transparency and diversity, identify new research challenges, and derive an agenda for computer science research and education efforts in responsible data analysis and use. While the topic of the seminar is transdisciplinary in nature, an important goal of the seminar was to identify opportunities for high-impact contributions to this important emergent area specifically from the data management community.
Published: 2016
Full Text: View/download PDF

24. Ideal Decompositions for Vector Addition Systems

Author: Leroux, Jérôme, Schmitz, Sylvain, 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), 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), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Nicolas Ollinger and Heribert Vollmer, and Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)
Subjects: well-quasi-order, ideal, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Petri net, verification, ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs, reachability
Abstract: International audience; Vector addition systems, or equivalently Petri nets, are one of the most popular formal models for the representation and the analysis of parallel processes. Many problems for vector addition systems are known to be decidable thanks to the theory of well-structured transition systems. Indeed, vector addition systems with configurations equipped with the classical point-wise ordering are well-structured transition systems. Based on this observation, problems like coverability or termination can be proven decidable. However, the theory of well-structured transition systems does not explain the decidability of the reachability problem. In this presentation, we show that runs of vector addition systems can also be equipped with a well quasi-order. This observation provides a unified understanding of the data structures involved in solving many problems for vector addition systems, including the central reachability problem.
Published: 2016
Full Text: View/download PDF

25. Deciding Piecewise Testable Separability for Regular Tree Languages

Author: Goubault-Larrecq, Jean, Schmitz, Sylvain, 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), Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi
Subjects: 000 Computer science, knowledge, general works, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.3: Formal Languages, ideal, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, 02 engineering and technology, tree languages, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic, 01 natural sciences, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 010201 computation theory & mathematics, Computer Science, well-quasi-order, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Computer Science::Formal Languages and Automata Theory, first-order logic
Abstract: International audience; The piecewise testable separability problem asks, given two input languages, whether there exists a piecewise testable language that contains the first input language and is disjoint from the second. We prove a general characterisation of piecewise testable separability on languages in a well-quasi-order, in terms of ideals of the ordering. This subsumes the known characterisations in the case of finite words. In the case of finite ranked trees ordered by homeomorphic embedding, we show using effective representations for tree ideals that it entails the decidability of piecewise testable separability when the input languages are regular. A final byproduct is a new proof of the decidability of whether an input regular language of ranked trees is piecewise testable, which was first shown in the ranked case for a coarser ordering by Place [CSL 2008], and in the unranked case for the homeomorphic embedding relation by Bojańczyk, Segoufin, and Straubing [Log. Meth. in Comput. Sci., 8(3:26), 2012].
Published: 2016
Full Text: View/download PDF

26. Capturing continuous data and answering aggregate queries in probabilistic XML

Author: Serge Abiteboul, Pierre Senellart, Werner Nutt, T.-H. Hubert Chan, Evgeny Kharlamov, Distributed and heterogeneous data and knowledge (LEO), Université Paris-Sud - Paris 11 (UP11)-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)-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), KRDB Research Centre (KRDB), Free University of Bozen-Bolzano, Department of Computer Science [HKU], City University of Hong Kong [Hong Kong] (CUHK), Laboratoire Traitement et Communication de l'Information (LTCI), Télécom ParisTech-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS), and Télécom Paristech, Admin
Subjects: [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Uncertain data, Computer science, Aggregate (data warehouse), Divergence-from-randomness model, Probabilistic logic, Probabilistic database, Context (language use), 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, 01 natural sciences, 010201 computation theory & mathematics, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, [INFO.INFO-DB] Computer Science [cs]/Databases [cs.DB], Probabilistic analysis of algorithms, Data mining, computer, Probabilistic relevance model, ComputingMilieux_MISCELLANEOUS, Information Systems
Abstract: Sources of data uncertainty and imprecision are numerous. A way to handle this uncertainty is to associate probabilistic annotations to data. Many such probabilistic database models have been proposed, both in the relational and in the semi-structured setting. The latter is particularly well adapted to the management of uncertain data coming from a variety of automatic processes. An important problem, in the context of probabilistic XML databases, is that of answering aggregate queries (count, sum, avg, etc.), which has received limited attention so far. In a model unifying the various (discrete) semi-structured probabilistic models studied up to now, we present algorithms to compute the distribution of the aggregation values (exploiting some regularity properties of the aggregate functions) and probabilistic moments (especially expectation and variance) of this distribution. We also prove the intractability of some of these problems and investigate approximation techniques. We finally extend the discrete model to a continuous one, in order to take into account continuous data values, such as measurements from sensor networks, and extend our algorithms and complexity results to the continuous case.
Published: 2011
Full Text: View/download PDF

27. Rigid tree automata and applications

Author: Florent Jacquemard, Camille Vacher, Francis Klay, 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), Orange Labs [Lannion], France Télécom, 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), This work has been partly supported by the INRIA ARC 2010 project ACCESS., ANR-07-SESU-0002,AVOTE,Analyse formelle de protocoles de vote électronique(2007), and European Project: 233599,EC:FP7:ICT,FP7-ICT-2007-C,FOX(2009)
Subjects: 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Tree automata, Theoretical Computer Science, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Tree automaton, Symbol constraints, Symbolic Constraints, Mathematics, Discrete mathematics, Finite-state machine, High Energy Physics::Phenomenology, Verification, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 16. Peace & justice, Pumping lemma for regular languages, Computer Science Applications, Decidability, Term rewriting, Tree (data structure), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, Closure (mathematics), 010201 computation theory & mathematics, Computer Science::Programming Languages, 020201 artificial intelligence & image processing, Rewriting, Language family, Computer Science::Formal Languages and Automata Theory, Information Systems
Abstract: International audience; 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.
Published: 2011
Full Text: View/download PDF

28. Relating timed and register automata

Author: Piotr Hofman, Diego Figueira, Sławomir Lasota, 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), University of Warsaw (UW), University of Edinburgh, Laboratoire Spécification et Vérification [Cachan] ( LSV ), École normale supérieure - Cachan ( ENS Cachan ) -Centre National de la Recherche Scientifique ( CNRS ), University of Warsaw ( UW ), Laboratoire Bordelais de Recherche en Informatique ( LaBRI ), Centre National de la Recherche Scientifique ( CNRS ) -École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Université Sciences et Technologies - Bordeaux 1-Université Bordeaux Segalen - Bordeaux 2, Laboratoire Bordelais de Recherche en Informatique (LaBRI), and Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)
Subjects: FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Theoretical computer science, TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES, Computer science, Formal Languages and Automata Theory (cs.FL), Timed automaton, Computer Science - Formal Languages and Automata Theory, 02 engineering and technology, 0102 computer and information sciences, [INFO.INFO-DM]Computer Science [cs]/Discrete Mathematics [cs.DM], 01 natural sciences, lcsh:QA75.5-76.95, Mathematics (miscellaneous), [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Transfer (computing), 0202 electrical engineering, electronic engineering, information engineering, 0101 mathematics, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Model of computation, lcsh:Mathematics, 010102 general mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [ INFO.INFO-DM ] Computer Science [cs]/Discrete Mathematics [cs.DM], Decision problem, lcsh:QA1-939, Computer Science Applications, Decidability, Automaton, Logic in Computer Science (cs.LO), [ INFO.INFO-DB ] Computer Science [cs]/Databases [cs.DB], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Register (music), 010201 computation theory & mathematics, [ INFO.INFO-FL ] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO], 020201 artificial intelligence & image processing, lcsh:Electronic computers. Computer science, Computer Science::Formal Languages and Automata Theory
Abstract: Timed automata and register automata are well-known models of computation over timed and data words respectively. The former has clocks that allow to test the lapse of time between two events, whilst the latter includes registers that can store data values for later comparison. Although these two models behave in appearance differently, several decision problems have the same (un)decidability and complexity results for both models. As a prominent example, emptiness is decidable for alternating automata with one clock or register, both with non-primitive recursive complexity. This is not by chance. This work confirms that there is indeed a tight relationship between the two models. We show that a run of a timed automaton can be simulated by a register automaton, and conversely that a run of a register automaton can be simulated by a timed automaton. Our results allow to transfer complexity and decidability results back and forth between these two kinds of models. We justify the usefulness of these reductions by obtaining new results on register automata., Comment: In Proceedings EXPRESS'10, arXiv:1011.6012
Published: 2010
Full Text: View/download PDF

29. Views and queries

Author: Luc Segoufin, Victor Vianu, Alan Nash, Aleph One LLC, 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), Department of Computer Science and Engineering [Univ California San Diego] (CSE - UC San Diego), University of California [San Diego] (UC San Diego), University of California (UC)-University of California (UC), and University of California (UC)
Subjects: Theory and algorithms for application domains, Determinacy, Theoretical computer science, Knowledge representation and reasoning, Computer science, Database theory, Query language, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Decidability, Algebra, Answer set programming, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Completeness (order theory), Query languages, Conjunctive query, Rewriting, Data management systems, Database query languages (principles), Theory of computation, Information Systems
Abstract: We investigate the question of whether a query Q can be answered using a set V of views. We first define the problem in information-theoretic terms: we say that V determines Q if V provides enough information to uniquely determine the answer to Q . Next, we look at the problem of rewriting Q in terms of V using a specific language. Given a view language V and query language Q , we say that a rewriting language R is complete for V -to- Q rewritings if every Q ∈ Q can be rewritten in terms of V ∈ V using a query in R , whenever V determines Q . While query rewriting using views has been extensively investigated for some specific languages, the connection to the information-theoretic notion of determinacy, and the question of completeness of a rewriting language have received little attention. In this article we investigate systematically the notion of determinacy and its connection to rewriting. The results concern decidability of determinacy for various view and query languages, as well as the power required of complete rewriting languages. We consider languages ranging from first-order to conjunctive queries.
Published: 2010
Full Text: View/download PDF

30. Transitive closure logic, nested tree walking automata, and XPath

Author: Luc Segoufin, Balder ten Cate, Intelligent Systems Lab. (ISLA), University of Amsterdam [Amsterdam] (UvA), 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), and The first author is supported by the Netherlands Organization for Scientific Research (NWO) grant 639.021.508, and partially by NSF grant IIS-0430994.
Subjects: Discrete mathematics, Unary operation, computer.internet_protocol, Transitive closure, Path expression, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Satisfiability, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Artificial Intelligence, Hardware and Architecture, Control and Systems Engineering, Kleene star, Temporal logic, Time complexity, computer, Software, Information Systems, Mathematics, XPath
Abstract: International audience; We study FO(MTC), first-order logic with monadic transitive closure, a logical formalism in between FO and MSO on trees. We characterize the expressive power of FO(MTC) in terms of nested tree-walking automata. Using the latter, we show that FO(MTC) is strictly less expressive than MSO, solving an open problem. We also present a temporal logic on trees that is expressively complete for FO(MTC), in the form of an extension of the XML document navigation language XPath with two operators: the Kleene star for taking the transitive closure of path expressions, and a subtree relativisation operator, allowing one to restrict attention to a specific subtree while evaluating a subexpression. We show that the expressive power of this XPath dialect equals that of FO(MTC) for Boolean, unary and binary queries. We also investigate the complexity of the automata model as well as the XPath dialect. We show that query evaluation be done in polynomial time (combined complexity), but that emptiness (or, satisfiability) is 2ExpTime-complete.
Published: 2010
Full Text: View/download PDF

31. Static analysis of active XML systems

Author: Victor Vianu, Serge Abiteboul, Luc Segoufin, Integration of data and knowledge distributed over the web (GEMO), Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-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), 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, Department of Computer Science and Engineering [Univ California San Diego] (CSE - UC San Diego), University of California [San Diego] (UC San Diego), University of California (UC)-University of California (UC), Work supported in part by the National Science Foundation under grant number IIS-0415257., and ANR-06-MDCA-0005,DocFlow,analysis, monitoring and optimization of Web documents and services(2006)
Subjects: Document Structure Description, XML Encryption, Computer science, Programming language, Efficient XML Interchange, XML Signature, XML validation, computer.file_format, computer.software_genre, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], XML Schema Editor, Streaming XML, XML schema, computer, Information Systems, computer.programming_language
Abstract: International audience; Active XML is a high-level specification language tailored to data-intensive, distributed, dynamic Web services. Active XML is based on XML documents with embedded function calls. The state of a document evolves depending on the result of internal function calls (local computations) or external ones (interactions with users or other services). Function calls return documents that may be active, and so may activate new subtasks. The focus of this article is on the verification of temporal properties of runs of Active XML systems, specified in a tree-pattern-based temporal logic, Tree-LTL, which allows expressing a rich class of semantic properties of the application. The main results establish the boundary of decidability and the complexity of automatic verification of Tree-LTL properties.
Published: 2009
Full Text: View/download PDF

32. Regular tree languages definable in FO and in FO mod

Author: Luc Segoufin, Michael Benedikt, Department of Computer Science [Oxford], University of Oxford, 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, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: Discrete mathematics, General Computer Science, Logic, Abstract family of languages, Computer Science::Computation and Language (Computational Linguistics and Natural Language and Speech Processing), Cone (formal languages), [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Pumping lemma for regular languages, Tree automata, Theoretical Computer Science, Combinatorics, Computational Mathematics, Regular language, Formal language, Regular tree grammar, Computer Science::Programming Languages, Nondeterministic finite automaton, Generalized star height problem, Mathematics
Abstract: International audience; We consider regular languages of labeled trees. We give an effective characterization of the regular languages over such trees that are definable in first-order logic in the language of labeled graphs. These languages are the analog on trees of the “locally threshold testable” languages on strings. We show that this characterization yields a decision procedure for determining whether a regular tree language is first-order definable: The procedure is polynomial time in the minimal automaton presenting the regular language. We also provide an algorithm for deciding whether a regular language is definable in first-order logic supplemented with modular quantifiers.
Published: 2009
Full Text: View/download PDF

33. On the expressiveness of probabilistic XML models

Author: Pierre Senellart, Yehoshua Sagiv, Serge Abiteboul, Benny Kimelfeld, 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), IBM Almaden Research Center [San Jose], IBM, Institute of Computer Science, The Hebrew University of Jerusalem (HUJ), Département Informatique et Réseaux (INFRES), and Télécom ParisTech
Subjects: Object-oriented programming, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Theoretical computer science, Computer science, computer.internet_protocol, Semantics (computer science), Value (computer science), 02 engineering and technology, computer.software_genre, Semantics, Object (computer science), Focus (linguistics), Closure (mathematics), Hardware and Architecture, 020204 information systems, ComputingMethodologies_DOCUMENTANDTEXTPROCESSING, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Data mining, computer, XML, Information Systems
Abstract: Various known models of probabilistic XML can be represented as instantiations of the abstract notion of p-documents. In addition to ordinary nodes, p-documents have distributional nodes that specify the possible worlds and their probabilistic distribution. Particular families of p-documents are determined by the types of distributional nodes that can be used as well as by the structural constraints on the placement of those nodes in a p-document. Some of the resulting families provide natural extensions and combinations of previously studied probabilistic XML models. The focus of the paper is on the expressive power of families of p-documents. In particular, two main issues are studied. The first is the ability to (efficiently) translate a given p-document of one family into another family. The second is closure under updates, namely, the ability to (efficiently) represent the result of updating the instances of a p-document of a given family as another p-document of that family. For both issues, we distinguish two variants corresponding to value-based and object-based semantics of p-documents.
Published: 2009
Full Text: View/download PDF

34. Closure of Tree Automata Languages under Innermost Rewriting

Author: Florent Jacquemard, Adrià Gascón, Guillem Godoy, Universitat Politècnica de Catalunya [Barcelona] (UPC), 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), The first two authors were supported by Spanish Min. of Educ. and Science by the FORMALISM project (TIN2007-66523) and by the LOGICTOOLS-2 project (TIN2007-68093-C02-01)., and Middeldorp, Aart
Subjects: General Computer Science, Tree Automata, 0102 computer and information sciences, 01 natural sciences, Theoretical Computer Science, Set (abstract data type), ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, 0101 mathematics, Term Rewriting, Mathematics, Discrete mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Rewrite Strategies, Term (logic), 16. Peace & justice, Automaton, Decidability, 010101 applied mathematics, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Closure (mathematics), 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Confluence, Tree (set theory), Rewriting, Computer Science(all)
Abstract: International audience; 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.
Published: 2009
Full Text: View/download PDF

35. View-based query determinacy and rewritings over graph databases

Author: Francis, Nadime, 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), Université Paris-Saclay, and Luc Segoufin
Subjects: Déterminabilité, Graphes de données, Graph databases, Rewriting, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Determinacy, Path queries, Réécriture, Requêtes de chemin, Vues, Views
Abstract: Graph databases appear naturally in various scenarios, such as social networks and the semantic Web. In these cases, the information contained in the database lies as much in the data itself as in the topology of the graph, that is, in how the data points are linked together. This leads to considering traditional database theory questions for query languages that return data nodes based on the paths of the graph connecting them. We focus our attention on the view-based query determinacy and rewriting problems. They ask the question whether a view of the database contains enough information to fully answer a query without accessing the database directly. If so, we then want to express the answer to the query directly with regards to the view. This setting occurs in many applications, such as data integration and query optimization. We start by comparing these two tasks to other common task in this setting: computing certain answers, checking consistency of a view instance and updating it. We then build on these results in two specific cases. First, we show that for regular path queries, the existence of a monotone rewriting coincides with the existence of a rewriting expressible in Datalog. Then, we show that for views that only consider the lengths of the path in the graph, we can decide a weaker form of determinacy, called asymptotic determinacy, and produce first-order rewritings for the queries that are asymptotically determined.; Les graphes de données sont naturellement utilisés dans de nombreux contextes incluant par exemple les réseaux sociaux ou le Web sémantique. L'information contenue dans la base de données se trouve alors aussi bien dans les données mêmes que dans la topologie du graphe, c'est-à-dire dans la manière dont les données sont connectées. Cela implique donc de considérer les questions traditionnelles en théorie des bases de données pour des langages de requêtes capables de parler des chemins connectant les nœuds du graphe. Nous nous intéressons en particulier aux problèmes de la déterminabilité et de la réécriture d'une requête à l'aide de vues. Il s'agit alors de décider si une vue de la base de données contient suffisamment d'information pour répondre entièrement à une requête sans consulter la base de données directement, et dans ce cas, d'exprimer explicitement la réponse à la requête à partir de la vue. Ce cadre rencontre de nombreuses applications, notamment pour l'intégration de données et l'optimisation de requêtes. Nous commençons par comparer ces deux questions aux autres problèmes de décision classiques dans ce contexte : calcul des réponses certaines, test de cohérence et mise à jour d'une instance de vue. Nous améliorons ensuite ces résultats dans deux cas spécifiques. Tout d'abord, nous montrons que pour les requêtes régulières de chemin, l'existence d'une réécriture monotone coïncide avec l'existence d'une réécriture dans Datalog. Puis, nous montrons que pour des vues s'intéressant uniquement aux longueurs des chemins du graphe, une notion plus faible de déterminabilité, appelée déterminabilité asymptotique, est décidable et résulte en des réécritures du premier ordre.
Published: 2015

36. Vues et requêtes sur les graphes de données : déterminabilité et réécritures

Author: Francis, Nadime, 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), Université Paris-Saclay, Luc Segoufin, and Université Paris Saclay (COmUE)
Subjects: Déterminabilité, Graphes de données, Graph databases, Rewriting, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Determinacy, Path queries, Réécriture, Requêtes de chemin, Vues, Views
Abstract: Graph databases appear naturally in various scenarios, such as social networks and the semantic Web. In these cases, the information contained in the database lies as much in the data itself as in the topology of the graph, that is, in how the data points are linked together. This leads to considering traditional database theory questions for query languages that return data nodes based on the paths of the graph connecting them. We focus our attention on the view-based query determinacy and rewriting problems. They ask the question whether a view of the database contains enough information to fully answer a query without accessing the database directly. If so, we then want to express the answer to the query directly with regards to the view. This setting occurs in many applications, such as data integration and query optimization. We start by comparing these two tasks to other common task in this setting: computing certain answers, checking consistency of a view instance and updating it. We then build on these results in two specific cases. First, we show that for regular path queries, the existence of a monotone rewriting coincides with the existence of a rewriting expressible in Datalog. Then, we show that for views that only consider the lengths of the path in the graph, we can decide a weaker form of determinacy, called asymptotic determinacy, and produce first-order rewritings for the queries that are asymptotically determined.; Les graphes de données sont naturellement utilisés dans de nombreux contextes incluant par exemple les réseaux sociaux ou le Web sémantique. L'information contenue dans la base de données se trouve alors aussi bien dans les données mêmes que dans la topologie du graphe, c'est-à-dire dans la manière dont les données sont connectées. Cela implique donc de considérer les questions traditionnelles en théorie des bases de données pour des langages de requêtes capables de parler des chemins connectant les nœuds du graphe. Nous nous intéressons en particulier aux problèmes de la déterminabilité et de la réécriture d'une requête à l'aide de vues. Il s'agit alors de décider si une vue de la base de données contient suffisamment d'information pour répondre entièrement à une requête sans consulter la base de données directement, et dans ce cas, d'exprimer explicitement la réponse à la requête à partir de la vue. Ce cadre rencontre de nombreuses applications, notamment pour l'intégration de données et l'optimisation de requêtes. Nous commençons par comparer ces deux questions aux autres problèmes de décision classiques dans ce contexte : calcul des réponses certaines, test de cohérence et mise à jour d'une instance de vue. Nous améliorons ensuite ces résultats dans deux cas spécifiques. Tout d'abord, nous montrons que pour les requêtes régulières de chemin, l'existence d'une réécriture monotone coïncide avec l'existence d'une réécriture dans Datalog. Puis, nous montrons que pour des vues s'intéressant uniquement aux longueurs des chemins du graphe, une notion plus faible de déterminabilité, appelée déterminabilité asymptotique, est décidable et résulte en des réécritures du premier ordre.
Published: 2015

37. Transforming Wikipedia into an Ontology-based Information Retrieval Search Engine for Local Experts using a Third-Party Taxonomy

Author: Grefenstette, Gregory, Rafes , Karima, Machine Learning and Optimisation (TAO), 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)-Université Paris-Sud - Paris 11 (UP11)-Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec, 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), BorderCloud [Issy-les-Moulineaux], Laboratoire de Recherche en Informatique (LRI), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Advanced Researcher Grant Inria, ANR-11-IDEX-0003,IPS,Idex Paris-Saclay(2011), and Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France
Subjects: FOS: Computer and information sciences, Computer Science - Computation and Language, local search, ACM: I.: Computing Methodologies/I.7: DOCUMENT AND TEXT PROCESSING/I.7.2: Document Preparation/I.7.2.2: Hypertext/hypermedia, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], ACM: H.: Information Systems/H.3: INFORMATION STORAGE AND RETRIEVAL/H.3.1: Content Analysis and Indexing/H.3.1.4: Thesauruses, Computer Science - Information Retrieval, ACM: H.: Information Systems/H.3: INFORMATION STORAGE AND RETRIEVAL/H.3.3: Information Search and Retrieval, ACM: I.: Computing Methodologies/I.7: DOCUMENT AND TEXT PROCESSING/I.7.2: Document Preparation/I.7.2.3: Index generation, ontology, Computation and Language (cs.CL), ACM: H.: Information Systems/H.3: INFORMATION STORAGE AND RETRIEVAL/H.3.1: Content Analysis and Indexing, GeneralLiterature_REFERENCE(e.g.,dictionaries,encyclopedias,glossaries), Information Retrieval (cs.IR), pivot ontology, Wikipedia
Abstract: Wikipedia is widely used for finding general information about a wide variety of topics. Its vocation is not to provide local information. For example, it provides plot, cast, and production information about a given movie, but not showing times in your local movie theatre. Here we describe how we can connect local information to Wikipedia, without altering its content. The case study we present involves finding local scientific experts. Using a third-party taxonomy, independent from Wikipedia's category hierarchy, we index information connected to our local experts, present in their activity reports, and we re-index Wikipedia content using the same taxonomy. The connections between Wikipedia pages and local expert reports are stored in a relational database, accessible through as public SPARQL endpoint. A Wikipedia gadget (or plugin) activated by the interested user, accesses the endpoint as each Wikipedia page is accessed. An additional tab on the Wikipedia page allows the user to open up a list of teams of local experts associated with the subject matter in the Wikipedia page. The technique, though presented here as a way to identify local experts, is generic, in that any third party taxonomy, can be used in this to connect Wikipedia to any non-Wikipedia data source., Joint Second Workshop on Language and Ontology \& Terminology and Knowledge Structures (LangOnto2 + TermiKS) LO2TKS, May 2016, Portoroz, Slovenia. 2016
Published: 2015

38. Hup-Me: Inferring and Reconciling a Timeline of User Activity from Rich Smartphone Data

Author: Serge Abiteboul, David Montoya, Pierre Senellart, 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), ENGIE Ineo - Safran RPAS Chair, SAFRAN Group-Aéroports de Paris-Ecole Nationale de l'Aviation Civile (ENAC), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Laboratoire Traitement et Communication de l'Information (LTCI), Télécom ParisTech-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS), and Abiteboul, Serge
Subjects: [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Multimodal Transport Networks, business.industry, Computer science, Transport network, Probabilistic logic, Timeline, Flow network, Computer security, computer.software_genre, Activity Recognition, Itinerary Recognition, Activity recognition, Transport engineering, Public transport, Global Positioning System, [INFO.INFO-DB] Computer Science [cs]/Databases [cs.DB], Dynamic Bayesian Networks, business, computer, Smartphone sensors, Dynamic Bayesian network
Abstract: International audience; We designed a system to infer multimodal itineraries traveled by a user from a combination of smartphone sensor data (e.g., GPS, Wi-Fi, accelerometer) and knowledge of the transport network infrastructure (e.g., road and rail maps, public transportation timetables). The system uses a Transportation network that captures the set of possible paths of this network for the modes, e.g., foot, bicycle, road_vehicle, and rail. This Transportation network is constructed from OpenStreetMap data and public transportation routes published online by transportation agencies in GTFS format. Thesystem infers itineraries from a sequence of smartphone observations in two phases. The first phase uses a dynamic Bayesian network that models the probabilistic relationship between paths in Transportation network and sensor data. The second phase attempts to match portions recognized as road_vehicle or rail with possible public transportation routes of type bus, train, metro, or tram extracted from the GTFS source. We evaluated the performance of our systemwith data from users traveling over the Paris area who were asked to record data for different trips via an Android application. Itineraries were annotated with modes and public transportation routes taken and we report on the results of the recognition.
Published: 2015

39. Demystifying Reachability in Vector Addition Systems

Author: Jérôme Leroux, Sylvain Schmitz, 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), 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), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), ANR-14-CE28-0005,PRODAQ,Systèmes de preuves pour requêtes avec données(2014), ANR-11-BS02-0001,REACHARD,Problèmes d'accessiblité difficiles pour les systèmes à compteurs(2011), and Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Discrete mathematics, Computer Science - Logic in Computer Science, Ideal (set theory), Well-quasi-ordering, ideal, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], fast-growing complexity, Mathematical proof, well quasi order, Ackermann function, Upper and lower bounds, Decidability, Reachability, Embedding, vector addition system, reachability, Mathematics
Abstract: More than 30 years after their inception, the decidability proofs for reachability in vector addition systems (VAS) still retain much of their mystery. These proofs rely crucially on a decomposition of runs successively refined by Mayr, Kosaraju, and Lambert, which appears rather magical, and for which no complexity upper bound is known. We first offer a justification for this decomposition technique, by showing that it computes the ideal decomposition of the set of runs, using the natural embedding relation between runs as well quasi ordering. In a second part, we apply recent results on the complexity of termination thanks to well quasi orders and well orders to obtain a cubic Ackermann upper bound for the decomposition algorithms, thus providing the first known upper bounds for general VAS reachability., Comment: To appear in the Proceedings of LICS 2015
Published: 2015
Full Text: View/download PDF

40. Humanités numériques

Author: Abiteboul, Serge, Hachez-Leroy, Florence, 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), Centre de Recherches Historiques (CRH) _ Unité Mixte de Recherches (UMR 8558 CNRS / EHESS) (CRH (UMR 8558 CNRS / EHESS)), École des hautes études en sciences sociales (EHESS)-Centre National de la Recherche Scientifique (CNRS), Université d'Artois (UA), Centre de Recherches Historiques (CRH), and Centre National de la Recherche Scientifique (CNRS)-École des hautes études en sciences sociales (EHESS)
Subjects: numérique, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], humanité, informatique, [INFO]Computer Science [cs], [SHS]Humanities and Social Sciences
Abstract: National audience; The digital humanities, also known as humanities computing , , is a field of study, research, teaching, and invention concerned with the intersection of computing and the disciplines of the humanities. It is methodological by nature and interdisciplinary in scope. It involves investigation, analysis, synthesis and presentation of information in electronic form. It studies how these media affect the disciplines in which they are used, and what these disciplines have to contribute to our knowledge of computing. Wikipedia, http://en.wikipedia.org, 2014.
Published: 2015

41. Collaborative Access Control in WebdamLog

Author: Serge Abiteboul, Gerome Miklau, Julia Stoyanovich, Vera Zaychik Moffitt, Drexel University, 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), Department of Computer Science [Amherst], University of Massachusetts [Amherst] (UMass Amherst), and University of Massachusetts System (UMASS)-University of Massachusetts System (UMASS)
Subjects: [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Computer access control, business.industry, Computer science, Data management, distributed datalog, provenance, access control, personal information management, Access control, Datalog, World Wide Web, collaborative access control, Data access, Formal specification, Role-based access control, Personal information management, business, Personally identifiable information, computer, computer.programming_language
Abstract: International audience; The management of Web users' personal information is increasingly distributed across a broad array of applications and systems, including online social networks and cloud-based services. Users wish to share data using these systems, but avoiding the risks of unintended disclosures or unauthorized access by applications has become a major challenge. We propose a novel access control model that operates within a distributed data management framework based on datalog. Using this model, users can control access to data they own and control applications they run. They can conveniently specify access control policies providing flexible tuple-level control derived using provenance information. We present a formal specification of the model, an implementation built using an open-source distributed datalog engine, and an extensive experimental evaluation showing that the computational cost of access control is modest.
Published: 2015
Full Text: View/download PDF

42. Calculer sur des données massives

Author: Abiteboul, Serge, 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), and Interstices, inria
Subjects: big data, calcul, MapReduce, [INFO]Computer Science [cs], [INFO] Computer Science [cs], données massives
Abstract: National audience; Comment fonctionne MapReduce, l’un des principaux logiciels utilisés pour faire des calculs sur des données massives ?
Published: 2015

43. Managing your digital life with a Personal information management system

Author: Abiteboul, Serge, André, Benjamin, Kaplan, Daniel, 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), Cozy Cloud, Fondation internet nouvelle génération [Paris] (FING), and Abiteboul, Serge
Subjects: [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], [INFO.INFO-DB] Computer Science [cs]/Databases [cs.DB]
Abstract: International audience; Computer wizards already know how to control their personal data to some extent. It is now becoming possible for everyone to do the same, and there are many advantages to doing so. Everyone should now be in a position to manage his/her personal information management system. This is the topic of this paper. To appear in Communications of the ACM
Published: 2015

44. The Story of Webdamlog

Author: Abiteboul, Serge, 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), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), and Abiteboul, Serge
Subjects: [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], [INFO.INFO-DB] Computer Science [cs]/Databases [cs.DB]
Abstract: International audience; We summarize in this paper works about the management of data in a distributed manner based on Webdamlog, a datalog-extension. We point to relevant articles on these works. More references may be found there. 1 The Webdamlog approach Information of interest may be found on the Web in a variety of forms, in many systems, and with different access protocols. Today, the control and management of the diversity of data and tasks in this setting are beyond the skills of casual users [1]. Facing similar issues, companies see the cost of managing and integrating information skyrocketing. We are concerned with the management of Web data in place in a distributed manner, with a possibly large number of autonomous, heterogeneous systems collaborating to support certain tasks. We summarize in this paper works in this setting around Webdamlog and point to the relevant articles on it. The thesis is that managing the richness and diversity of data residing on the Web can be tamed using a holistic approach based on a distributed knowledge base. Our approach is to represent all Web information as logical facts, and Web data management tasks as logical rules. A variety of complex data management tasks that currently require intense work and deep expertise may then greatly benefit from the automatic reasoning provided by inference engines, operating over the distributed Web knowledge base: for instance, information access, access control, knowledge acquisition and dissemination. We propose to express the peers logic in Webdamlog, a datalog-style rule-based language. In Webdamlog, peers exchange facts (for information) and rules (in place of code). The use of declarative rules provides the following advantages. Peers may perform automatic reasoning using the available knowledge. Because the model is formally defined, it becomes possible to prove (or disprove) desirable properties. Because the model is based on a datalog-style language, query processing can benefit from optimization techniques. Because the model represents provenance and time, the quality of data can be better controlled. Because We thank all the researchers who participated in the Webdamlog project and in particular
Published: 2015

45. Capturing MSO with One Quantifier

Author: Luc Segoufin, Anuj Dawar, Computer Laboratory [Cambridge], University of Cambridge [UK] (CAM), 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, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: Discrete mathematics, Lindström quantifier, Sibling order, 010102 general mathematics, Transitive closure, 0102 computer and information sciences, Extension (predicate logic), 16. Peace & justice, 01 natural sciences, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Combinatorics, 010201 computation theory & mathematics, Quantifier elimination, Quantifier (linguistics), Tree automaton, 0101 mathematics, Boolean satisfiability problem, Mathematics
Abstract: International audience; We construct a single Lindström quantifier Q such that FO(Q), the extension of first-order logic with Q has the same expressive power as monadic second-order logic on the class of binary trees (with distinct left and right successors) and also on unranked trees with a sibling order. This resolves a conjecture by ten Cate and Segoufin. The quantifier Q is a variation of a quantifier expressing the Boolean satisfiability problem.
Published: 2015
Full Text: View/download PDF

46. Process-Centric Views of Data-Driven Business Artifacts

Author: Adrien Koutsos, Victor Vianu, 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), Department of Computer Science and Engineering [San Diego] (CSE-UCSD), University of California [San Diego] (UC San Diego), University of California-University of California, Department of Computer Science and Engineering [Univ California San Diego] (CSE - UC San Diego), and University of California (UC)-University of California (UC)
Subjects: 1998 ACM Subject Classification H23 Languages: Query languages, Computer Networks and Communications, Computer science, Process (engineering), Semantics (computer science), Artifact (software development), 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, 01 natural sciences, Theoretical Computer Science, System model, Business Process Model and Notation, Control flow, H41 Office Automation: Workflow management, Unified Modeling Language, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, [INFO]Computer Science [cs], computer.programming_language, 000 Computer science, knowledge, general works, [INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], business.industry, Applied Mathematics, Verification, B44 Performance Analysis and Design Aids: Formal models, Workflow, Computational Theory and Mathematics, 010201 computation theory & mathematics, [INFO.INFO-IR]Computer Science [cs]/Information Retrieval [cs.IR], Computer Science, 020201 artificial intelligence & image processing, Data mining, Software engineering, business, computer
Abstract: Declarative, data-aware workflow models are becoming increasingly pervasive. While these have numerous benefits, classical process-centric specifications retain certain advantages. Workflow designers are used to development tools such as BPMN or UML diagrams, that focus on control flow. Views describing valid sequences of tasks are also useful to provide stakeholders with high-level descriptions of the workflow, stripped of the accompanying data. In this paper we study the problem of recovering process-centric views from declarative, data-aware workflow specifications in a variant of IBM's business artifact model. We focus on the simplest process-centric views, specified by finite-state transition systems, describing regular languages. The results characterize when process-centric views of artifact systems are regular, using both linear and branching-time semantics. We also study the impact of data dependencies on regularity of the views. As a side effect, we obtain several new results on verification of business artifacts, including a decidability result for branching-time properties. Linear-time process views of artifact systems are effectively regular.Branching-time process views of globally feedback-free artifact systems are effectively regular.Model-checking branching-time properties of globally feedback-free artifact systems is decidable.Database dependencies have an impact on the regularity of linear and branching-time process views.
Published: 2015
Full Text: View/download PDF

47. Guarded negation

Author: Luc Segoufin, Balder ten Cate, Vince Bárány, 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), University of California [Santa Cruz] (UC Santa Cruz), University of California (UC), University of California [Santa Cruz] (UCSC), and University of California
Subjects: Predicate functor logic, 0102 computer and information sciences, Decidability, 01 natural sciences, Higher-order logic, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], Description logic, Artificial Intelligence, 0101 mathematics, Satisfiability, Autoepistemic logic, Mathematics, Predicate logic, Discrete mathematics, 010102 general mathematics, Fixpoint Logic, Multimodal logic, Modal μ-calculus, 16. Peace & justice, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, Hardware and Architecture, Control and Systems Engineering, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Many-valued logic, Guarded Fragment, Negation, Software, Information Systems
Abstract: We consider restrictions of first-order logic and of fixpoint logic in which all occurrences of negation are required to be guarded by an atomic predicate. In terms of expressive power, the logics in question, called GNFO and GNFP, extend the guarded fragment of first-order logic and the guarded least fixpoint logic, respectively. They also extend the recently introduced unary negation fragments of first-order logic and of least fixpoint logic. We show that the satisfiability problem for GNFO and for GNFP is 2ExpTime-complete, both on arbitrary structures and on finite structures. We also study the complexity of the associated model checking problems. Finally, we show that GNFO and GNFP are not only computationally well behaved, but also model theoretically: we show that GNFO and GNFP have the tree-like model property and that GNFO has the finite model property, and we characterize the expressive power of GNFO in terms of invariance for an appropriate notion of bisimulation. Our complexity upper bounds for GNFO and GNFP hold true even for their “clique-guarded” extensions CGNFO and CGNFP, in which clique guards are allowed in the place of guards.
Published: 2015

48. Constant Delay Enumeration for Conjunctive Queries

Author: Luc Segoufin, 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, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: Class (set theory), Theoretical computer science, Computer science, InformationSystems_DATABASEMANAGEMENT, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], 010201 computation theory & mathematics, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Enumeration, Conjunctive query, Focus (optics), Constant (mathematics), Time complexity, Algorithm, Software, Information Systems
Abstract: We survey some of the recent results about enumerating the answers to queries over a database. We focus on the case where the enumeration is performed with a constant delay between any two consecutive solutions, after a linear time preprocessing. This cannot be always achieved. It requires restricting either the class of queries or the class of databases. We consider conjunctive queries and describe several scenarios when this is possible.
Published: 2015

49. DECIDING DEFINABILITY IN FO 2 (< v , < h ) ON TREES

Author: Place, Thomas, Segoufin, Luc, 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), 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), and Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)
Subjects: [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Abstract: International audience; We provide a decidable characterization of regular forest languages definable in FO 2 (
Published: 2015
Full Text: View/download PDF

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

Catalog

Books, media, physical & digital resources

See catalog results

Searchworks

Select search scope, currently: Articles Catalog books, media & more in Jio Institute collections Articles journal articles & other e-resources

Search

Search Constraints

Refine your results

Search Limiters

Topic

Publication Year Range

Language

Journal

Database

Publisher

156 results on '"Verification in databases (DAHU)"'

Search Results

Catalog

Select search scope, currently: Articles

Catalog

books, media & more in Jio Institute collections

Articles

journal articles & other e-resources