Search

Your search keyword '"Grant A Fox"' showing total 2 results
Start Over Author "Grant A Fox" Topic computer science - logic in computer science
2 results on '"Grant A Fox"'

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

2. First-order query evaluation on structures of bounded degree

Author

Wojciech Kazana, 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, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), We acknowledge the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under the FET-Open grant agreement FOX, number FP7-ICT-233599., and European Project: 226513,EC:FP7:ERC,ERC-2008-AdG,WEBDAM(2008)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, General Computer Science, Matching (graph theory), First-order, Structure (category theory), 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, query evaluation, [INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL], enumeration, Theoretical Computer Science, 0202 electrical engineering, electronic engineering, information engineering, Enumeration, constant delay, F.4.1, F.1.3, Mathematics, Discrete mathematics, Degree (graph theory), Logic in Computer Science (cs.LO), Exponential function, 010201 computation theory & mathematics, Precomputation, Bounded function, 020201 artificial intelligence & image processing, Constant (mathematics)
Abstract

International audience; We consider the enumeration problem of first-order queries over structures of bounded degree. In [3] it was shown that this problem is in Constant-Delay lin. An enumeration problem belongs to Constant-Delay lin if for an input of size n it can be solved by: • an O(n) precomputation phase building an index structure, • followed by a phase enumerating the answers with no repetition and a constant delay between two consecutive outputs. In this article we give a different proof of this result based on Gaifman's locality theorem for first-order logic. Moreover, the constants we obtain yield a total evaluation time that is triply exponential in the size of the input formula, matching the complexity of the best known evaluation algorithms.

Published
2011
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results