Search

Your search keyword '"Leverhulme Trust Visiting Professorship VP1-2014-041"' showing total 3 results
Start Over Author "Leverhulme Trust Visiting Professorship VP1-2014-041"
3 results on '"Leverhulme Trust Visiting Professorship VP1-2014-041"'

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

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

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

Catalog

Books, media, physical & digital resources
See catalog results