Search

Your search keyword '"Verification in databases (DAHU)"' showing total 5 results
Start Over Author "Verification in databases (DAHU)" Publisher springer berlin heidelberg
5 results on '"Verification in databases (DAHU)"'

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

2. Reasoning About Pattern-Based XML Queries

Author

Cristina Sirangelo, Leonid Libkin, Amélie Gheerbrant, Laboratory for the Foundations of Computer Science [Edinburgh] (LFCS), University of Edinburgh, Laboratoire d'informatique Algorithmique : Fondements et Applications (LIAFA), Université Paris Diderot - Paris 7 (UPD7)-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), 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
[INFO.INFO-DB]Computer Science [cs]/Databases [cs.DB], Information retrieval, Computer science, computer.internet_protocol, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], InformationSystems_DATABASEMANAGEMENT, 0102 computer and information sciences, 02 engineering and technology, Disjunctive normal form, Static analysis, 01 natural sciences, Satisfiability, Tree (data structure), 010201 computation theory & mathematics, Data exchange, 020204 information systems, Schema (psychology), ComputingMethodologies_DOCUMENTANDTEXTPROCESSING, 0202 electrical engineering, electronic engineering, information engineering, Conjunctive query, computer, XML
Abstract

International audience; We survey results about static analysis of pattern-based queries over XML documents. These queries are analogs of conjunctive queries, their unions and Boolean combinations, in which tree patterns play the role of atomic formulae. As in the relational case, they can be viewed as both queries and incomplete documents, and thus static analysis problems can also be viewed as finding certain answers of queries over such documents. We look at satisfiability of patterns under schemas, containment of queries for various features of XML used in queries, finding certain answers, and applications of pattern-based queries in reasoning about schema mappings for data exchange.

Published
2013
Full Text
View/download PDF

3. Unique Normalization for Shallow TRS

Author

Florent Jacquemard, 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 author was 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 Treinen, Ralf

Subjects
Normalization (statistics), Discrete mathematics, Computation, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Undecidable problem, Decidability, Combinatorics, 010201 computation theory & mathematics, Reachability, Computer Science::Logic in Computer Science, Confluence, 0202 electrical engineering, electronic engineering, information engineering, Computer Science::Programming Languages, 020201 artificial intelligence & image processing, Tree automaton, Time complexity, Mathematics
Abstract

Computation with a term rewrite system (TRS) consists in the application of its rules from a given starting term until a normal form is reached, which is considered the result of the computation. The unique normalization (UN) property for a TRS $\mathcal{R}$ states that any starting term can reach at most one normal form when $\mathcal{R}$ is used, i.e. that the computation with $\mathcal{R}$ is unique. We study the decidability of this property for classes of TRS defined by syntactic restrictions such as linearity (variables can occur only once in each side of the rules), flatness (sides of the rules have height at most one) and shallowness (variables occur at depth at most one in the rules). We prove that UN is decidable in polynomial time for shallow and linear TRS, using tree automata techniques. This result is very near to the limits of decidability, since this property is known undecidable even for very restricted classes like right-ground TRS, flat TRS and also right-flat and linear TRS. We also show that UN is even undecidable for flat and right-linear TRS. The latter result is in contrast with the fact that many other natural properties like reachability, termination, confluence, weak normalization, etc. are decidable for this class of TRS.

Published
2009
Full Text
View/download PDF

4. Tree Automata with Memory, Visibility and Structural Constraints

Author

Florent Jacquemard, Hubert Comon-Lundh, Nicolas Perrin, 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), Laboratoire d'analyse et d'architecture des systèmes (LAAS), Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université Fédérale Toulouse Midi-Pyrénées, Joint Robotics Laboratory [France] (CNRS-AIST JRL), National Institute of Advanced Industrial Science and Technology (AIST)-Centre National de la Recherche Scientifique (CNRS), Helmut Seidl, Université Toulouse Capitole (UT Capitole), Université de Toulouse (UT)-Université de Toulouse (UT)-Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Université de Toulouse (UT)-Institut National des Sciences Appliquées (INSA)-Université Toulouse - Jean Jaurès (UT2J), Université de Toulouse (UT)-Université Toulouse III - Paul Sabatier (UT3), Université de Toulouse (UT)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique (Toulouse) (Toulouse INP), Université de Toulouse (UT), Joint Japanese-French Robotics Research Laboratory [Japon] (JRL), Intelligent Systems Research Institute-National Institute of Advanced Industrial Science and Technology (AIST)-Centre National de la Recherche Scientifique (CNRS), and Centre National de la Recherche Scientifique (CNRS)-National Institute of Advanced Industrial Science and Technology (AIST)

Subjects
Discrete mathematics, TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES, Nested word, Computation, Pushdown automaton, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Universality (dynamical systems), Decidability, Automaton, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Tree structure, 010201 computation theory & mathematics, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Automata theory, Computer Science::Formal Languages and Automata Theory, Mathematics
Abstract

International audience; Tree automata with one memory have been introduced in 2001. They generalize both pushdown (word) automata and the tree automata with constraints of equality between brothers of Bogaert and Tison. Though it has a decidable emptiness problem, the main weakness of this model is its lack of good closure properties. We propose a generalization of the visibly pushdown automata of Alur and Madhusudan to a family of tree recognizers which carry along their (bottom-up) computation an auxiliary unbounded memory with a tree structure (instead of a symbol stack). In other words, these recognizers, called visibly Tree Automata with Memory (VTAM) define a subclass of tree automata with one memory enjoying Boolean closure properties. We show in particular that they can be determinized and the problems like emptiness, inclusion and universality are decidable for VTAM. Moreover, we propose an extension of VTAM whose transitions may be constrained by structural equality and disequality tests between memories, and show that this extension preserves the good closure and decidability properties.

Published
2007
Full Text
View/download PDF

5. Tree Automata with Equality Constraints Modulo Equational Theories

Author

Michaël Rusinowitch, Florent Jacquemard, Laurent Vigneron, Security of information systems (SECSI), Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Combination of approaches to the security of infinite states systems (CASSIS), Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174) (FEMTO-ST), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université de Technologie de Belfort-Montbeliard (UTBM)-Ecole Nationale Supérieure de Mécanique et des Microtechniques (ENSMM)-Centre National de la Recherche Scientifique (CNRS)-Université de Franche-Comté (UFC), Université Bourgogne Franche-Comté [COMUE] (UBFC)-Université Bourgogne Franche-Comté [COMUE] (UBFC)-Inria Nancy - Grand Est, INRIA, Verification in databases (DAHU), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), and Ulrich Furbach and Natarajan Shankar

Subjects
TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES, Horn clause, Logic, basic paramodulation, splitting, Computer science, Modulo, [INFO.INFO-OH]Computer Science [cs]/Other [cs.OH], 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, tree automata, Theoretical Computer Science, first order theorem proving, Computer Science::Logic in Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Quantum finite automata, Tree automaton, Mathematics, Discrete mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Nonlinear Sciences::Cellular Automata and Lattice Gases, Decidability, Automaton, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, 010201 computation theory & mathematics, Automata theory, 020201 artificial intelligence & image processing, Tree (set theory), Software verification, Software, verification of infinite state systems, Computer Science::Formal Languages and Automata Theory
Abstract

International audience; This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that these classes have a good potential for application in e.g. software verification. These tree automata are obtained by extending the standard Horn clause representations with equational conditions and rewrite systems. We show in particular that a generalized membership problem (extending the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodulation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formula.

Published
2006
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results