Journals


DFP16

Stéphane Demri,
Diego Figueira, and
M. Praveen.
Reasoning about Data Repetitions with Counter Systems. Logical Methods in Computer Science (LMCS),
2016. To appear.
( PDF  Abstract & BibTeX )

Abstract

We study lineartime temporal logics interpreted over data words with multiple attributes. We restrict the atomic formulas to equalities of attribute values in successive positions and to repetitions of attribute values in the future or past. We demonstrate correspondences between satisfiability problems for logics and reachabilitylike decision problems for counter systems. We show that allowing/disallowing atomic formulas expressing repetitions of values in the past corresponds to the reachability/coverability problem in Petri nets. This gives us 2expspace upper bounds for several satisfiability problems. We prove matching lower bounds by reduction from a reachability problem for a newly introduced class of counter systems. This new class is a succinct version of vector addition systems with states in which counters are accessed via pointers, a potentially useful feature in other contexts. We strengthen further the correspondences between data logics and counter systems by characterizing the complexity of fragments, extensions and variants of the logic. For instance, we precisely characterize the relationship between the number of attributes allowed in the logic and the number of counters needed in the counter system.

BibTeX

@article{DFP16,
author = {Demri, Stephane and Figueira, Diego and M. Praveen},
journal = {Logical Methods in Computer Science},
title = {Reasoning about Data Repetitions with Counter Systems},
pages = {},
volume = {},
doi = {},
year = {2016},
}
 FFA15

Diego Figueira,
Santiago Figueira, and
Carlos Areces.
Model Theory of XPath on Data Trees. Part I: Bisimulation and Characterization.
Journal of Artificial Intelligence Research (JAIR) 53: 271314,
2015.
( PDF  Abstract & BibTeX )

Abstract

We investigate model theoretic properties of XPath with data (in)equality tests over the class of data trees, i.e., the class of trees where each node contains a label from a finite alphabet and a data value from an infinite domain.
We provide notions of (bi)simulations for XPpath logics containing the child, parent, ancestor and descendant axes to navigate the tree. We show that these notions precisely characterize the equivalence relation associated with each logic. We study formula complexity measures consisting of the number of nested axes and nested subformulas in a formula; these notions are akin to the notion of quantifier rank in firstorder logic. We show characterization results for fine grained notions of equivalence and (bi)simulation that take into account these complexity measures. We also prove that positive fragments of these logics correspond to the formulas preserved under (nonsymmetric) simulations. We show that the logic including the child axis is equivalent to the fragment of firstorder logic invariant under the corresponding notion of bisimulation. If upward navigation is allowed the characterization fails but a weaker result can still be established. These results hold both over the class of possibly infinite data trees and over the class of finite data trees.
Besides their intrinsic theoretical value, we argue that bisimulations are useful tools to prove (non)expressivity results for the logics studied here, and we substantiate this claim with examples.

BibTeX

@article{FFA15,
author = {Figueira, Diego and Figueira, Santiago and Areces, Carlos},
journal = {Journal of Artificial Intelligence Research},
title = {Model Theory of XPath on Data Trees. Part I: Bisimulation and Characterization},
pages = {271314},
volume = {53},
doi = {10.1613/jair.4658},
year = {2015},
}
 FL15b

Diego Figueira
and
Leonid Libkin.
Synchronizing relations on words.
Theory of Computing Systems (ToCS),
2015.
To appear.
( PDF  Abstract & BibTeX )

Abstract

While the theory of languages of words is very mature, our understanding of relations on words is still lagging behind. And yet such relations appear in many new applications such as verification of parameterized systems, querying graphstructured data, and information extraction, for instance. Classes of wellbehaved relations typically used in such applications are obtained by adapting some of the equivalent definitions of regularity of words for relations, leading to nonequivalent notions of recognizable, regular, and rational relations.
The goal of this paper is to propose a systematic way of defining classes of relations on words, of which these three classes are just natural examples, and to demonstrate its advantages compared to some of the standard techniques for studying word relations. The key idea is that of a synchronization of a pair of words, which is a word over an extended alphabet. Using it, we define classes of relations via classes of regular languages over a fixed alphabet, just {1,2} for binary relations. We characterize some of the standard classes of relations on words via finiteness of parameters of synchronization languages, called shift, lag, and shiftlag. We describe these conditions in terms of the structure of cycles of graphs underlying automata, thereby showing their decidability. We show that for these classes there exist canonical synchronization languages, and every class of relations can be effectively resynchronized using those canonical representatives. We also give sufficient conditions on synchronization languages, defined in terms of injectivity and surjectivity of their Parikh images, that guarantee closure under intersection and complement of the classes of relations they define.

BibTeX

@article{FL15b,
author = {Figueira, Diego and Libkin, Leonid},
journal = {Theory of Computing Systems},
title = {Synchronizing Relations on Words},
volume = {57},
number = {2},
pages = {287318}
doi = {10.1007/s0022401495842},
year = {2015},
}

BFL13

Pablo Barceló, Diego Figueira and Leonid Libkin.
Graph Logics with Rational Relations. Logical Methods in Computer Science (LMCS), 9(3:1), 2013.
( PDF  Abstract & BibTeX )

Abstract

We investigate some basic questions about the interaction of regular
and rational relations on words. The primary motivation comes from
the study of logics for querying graph topology, which have recently
found numerous applications. Such logics use conditions on paths
expressed by regular languages and relations, but they often need to
be extended by rational relations such as subword or
subsequence. Evaluating formulae in such extended graph logics boils
down to checking nonemptiness of the intersection of rational
relations with regular or recognizable relations (or, more generally,
to the generalized intersection problem, asking whether some
projections of a regular relation have a nonempty intersection with a
given rational relation).
We prove that for several basic and commonly used rational relations,
the intersection problem with regular relations is either undecidable
(e.g., for subword or suffix, and some generalizations), or decidable
with nonprimitiverecursive complexity (e.g., for subsequence
and its generalizations). These results are used to rule out many
classes of graph logics that freely combine regular and rational
relations, as well as to provide the simplest problem related to
verifying lossy channel systems that has nonprimitiverecursive
complexity. We then prove a dichotomy result for logics combining
regular conditions on individual paths and rational relations on
paths, by showing that the syntactic form of formulae classifies them
into either efficiently checkable or undecidable cases. We also give
examples of rational relations for which such logics are decidable
even without syntactic restrictions.

BibTeX

@article{BFL13,
author = {Barcel{\'o}, Pablo and Figueira, Diego and Libkin, Leonid},
journal = {Logical Methods in Computer Science},
title = {Graph Logics with Rational Relations},
volume = {9},
number = {3:01},
doi = {10.2168/LMCS9(3:1)2013},
year = {2013},
}

FHL12

Diego Figueira, Piotr Hofman and Sławomir Lasota
.
Relating timed and register automata. Mathematical Structures in Computer Science (MSCS), 2013. To appear.
( Abstract & BibTeX )

Abstract

Timed automata and register automata are wellknown 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 diﬀerently, 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 nonprimitive recursive complexity. This is not by chance.
This work conﬁrms 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 over ordered data domain, and conversely that a run of a register automaton can be simulated by a timed automaton. These are exponential time reductions hold both in the ﬁnite and inﬁnite words settings. Our results allow to transfer decidability results back and forth between these two kinds of models, as well complexity results modulo an exponential time reduction. We justify the usefulness of these reductions by obtaining new results on register automata.

BibTeX

@article{FHL12,
author = {Figueira, Diego and Hofman, Piotr and Lasota, S{\l}awomir},
journal = {Mathematical Structures in Computer Science},
title = {Relating timed and register automata},
volume = {?},
number = {?},
doi = {?},
year = {?},
note = {To appear},
}

Fig12b

Diego Figueira.
Alternating Register Automata on Finite Data Words and Trees. Logical Methods in Computer Science (LMCS), 8(1:22), 2012.
( PDF  Abstract & BibTeX )

Abstract

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 an finite alphabet and a data value from an infinite domain. We investigate oneway automata with alternating control over data words or trees, with one register for storing data and compare them for equality. This is a continuation of the study started by Demri, Lazic and Jurdzinski.
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 socalled forward fragment of XPath on XML documents is decidable, even in the presence of DTDs and even of primary key constraints. The decidability is obtained through a reduction to the automata model introduced. This fragment contains the child, descendant, nextsibling and followingsibling axes, as well as data equality and inequality tests.

BibTeX

@article{Fig12b,
author = {Figueira, Diego},
journal = {Logical Methods in Computer Science},
title = {Alternating Register Automata on Finite Data Words and Trees},
volume = {8},
number = {1},
doi = {10.2168/LMCS8(1:22)2012},
year = {2012},
}

Fig12

Diego Figueira.
Decidability of Downward XPath. ACM Transactions on Computational Logic (TOCL), 2012.
( PDF  Abstract & BibTeX )

Abstract

We investigate the satisfiability problem for downwardXPath, 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, ExpTimecomplete. 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 downwardXPath can be reduced to the emptiness problem of DD automata and hence its decidability follows. Although downwardXPath 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 nonprimitive recursive complexity. Finally, we give the exact complexity of the satisfiability problem for several fragments of downwardXPath.

BibTeX

@article{Fig12,
author = {Figueira, Diego},
journal = {ACM Transactions on Computational Logic},
publisher = {ACM Press},
title = {Decidability of Downward {XP}ath},
volume = {13},
number = {4},
doi = {10.1145/2362355.2362362},
year = {2012},
}

AFFM10

Carlos Areces, Diego Figueira, Santiago Figueira and Sergio Mera. The Expressive Power of Memory Logics. The Review of Symbolic Logic (RSL), 2010. ( PDF  Abstract & BibTeX )

Abstract

We investigate the expressive power of memory logics.
These are modal logics extended with the possibility to store (or remove) the
current node of evaluation in (or from) a memory, and to perform
membership tests on the current memory. From this perspective, the hybrid
logic HL(↓), for example, can be thought of as a
particular case of a memory logic where the memory is an indexed list of
elements of the domain.
This work focuses in the case where the memory is
a set, and we can test whether the current node belongs to the set or not. We
prove that, in terms of expressive power, the memory logics we discuss here
lie between the basic modal logic K and
HL(↓). We show that the satisfiability problem of most
of the logics we cover is undecidable. The only logic with a decidable
satisfiability problem is obtained by imposing strong constraints on which
elements can be memorized.

BibTeX

@article{AFFM10,
author = {Areces, Carlos and Figueira, Diego and Figueira, Santiago and Mera, Sergio},
journal = {Review of Symbolic Logic},
publisher = {Cambridge University Press},
title = {The Expressive Power of Memory Logics},
doi = {10.1017/S1755020310000389},
volume = {4},
issue = {2},
pages = {290318},
year = {2010},
}

Conferences

 AFF17

Sergio Abriola,
Diego Figueira, and Santiago Figueira.
Logics of repeating values on data trees and branching counter systems. In FoSSACS'17. 2017.
( PDF  Abstract & BibTeX )

Abstract

We study connections between the satisfiability problem for logics on data trees and Branching Vector Addition Systems (BVAS). We consider a natural temporal logic of "repeating values" (LRV) featuring an operator which tests whether a data value in the current node is repeated in some descendant node.
On the one hand, we show that the satisfiability of a restricted version of LRV on ranked data trees can be reduced to the coverability problem for Branching Vector Addition Systems. This immediately gives elementary upper bounds for its satisfiability problem, showing that restricted LRV behaves much better than downwardXPath, which has a nonprimitiverecursive satisfiability problem.
On the other hand, satisfiability for LRV is shown to be reducible to the coverability for a novel branching model we introduce here, called Merging VASS (MVASS). MVASS is an extension of Branching Vector Addition Systems with States (BVASS) allowing richer merging operations of the vectors. We show that the controlstate reachability for MVASS, as well as its bottomup coverability, are in 3ExpTime.
This work can be seen as a natural continuation of the work initiated by Demri, D'Souza and Gascon for the case of data words, this time considering branching structures and counter systems, although, as we show, in the case of data trees more powerful models are needed to encode satisfiability.

BibTeX

@inproceedings{AFF17,
author = {Sergio Abriola, Diego Figueira, Santiago Figueira},
booktitle = {Foundations of Software Science and Computation Structures, {FOSSACS} 2017},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {},
publisher = {Springer},
title = {Logics of repeating values on data trees and branching counter systems},
pages = {????},
year = {2017},
doi = {10.1109/???},
}
 AFG16

Myrto Arapinis,
Diego Figueira, and
Marco Gaboardi.
Sensitivity of Counting Queries. In ICALP'16. ACM Press, 2016.
( PDF  Abstract & BibTeX )

Abstract

In the context of statistical databases, the release of accurate statistical information about the collected data often puts at risk the privacy of the individual contributors. The goal of differential privacy is to maximise the utility of a query while protecting the individual records in the database. A natural way to achieve differential privacy is to add statistical noise to the result of the query. In this context, a mechanism for releasing statistical information is thus a tradeoff between utility and privacy. In order to balance these two ``conflicting'' requirements, privacy preserving mechanisms calibrate the added noise to the socalled \emph{sensitivity} of the query, and thus a precise estimate of the sensitivity of the query is necessary to determine the amplitude of the noise to be added.
In this paper, we initiate a systematic study of sensitivity of counting queries over relational databases. We first observe that the sensitivity of a Relational Algebra query with counting is not computable in general, and that while the sensitivity of Conjunctive Queries with counting is computable, it becomes unbounded as soon as the query includes a join. We then consider restricted classes of databases (databases with constraints), and study the problem of computing the sensitivity of a query given such constraints. We are able to establish bounds on the sensitivity of counting conjunctive queries over constrained databases. The kind of constraints studied here are: functional dependencies and cardinality dependencies. The latter is a natural generalisation of functional dependencies that allows us to provide tight bounds on the sensitivity of counting conjunctive queries.

BibTeX

@inproceedings{AFG16,
author = {Myrto Arapinis, Diego Figueira, Marco Gaboardi},
booktitle = {Automata, Languages, and Programming  43rd International Colloquium, {ICALP} 2016, Rome, Italy, July 2015, Proceedings},
publisher = {Springer},
title = {Sensitivity of Counting Queries},
pages = {????},
year = {2016},
doi = {10.1109/???},
}
 Fig16

Diego Figueira.
Semantically Acyclic Conjunctive Queries under Functional Dependencies. In LICS'16. ACM Press, 2016.
( PDF  Abstract & BibTeX )

Abstract

The evaluation problem for Conjunctive Queries (CQ) is known to be NPcomplete in combined complexity and W[1]hard in parameterized complexity. However, acyclic CQs and CQs of bounded treewidth can be evaluated in polynomial time in combined com plexity and they are fixedparameter tractable.
We study the problem of whether a CQ can be rewritten into an equivalent CQ of bounded treewidth, in the presence of unary functional dependencies, assuming bounded arity signatures. We show that this problem is decidable in doubly exponential time, or in exponential time for a subclass of CQ’s. When it exists, the algorithm also yields a witness query.

BibTeX

@inproceedings{Fig16,
author = {Diego Figueira},
booktitle = {31st Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS}
2016, New York, NY, USA, July 58, 2016},
publisher = {{IEEE} Computer Society Press},
title = {Semantically Acyclic Conjunctive Queries under Functional Dependencies},
pages = {????},
year = {2016},
doi = {10.1109/???},
}
 ABFF16

Sergio Abriola,
Pablo Barceló, Diego Figueira, Santiago Figueira.
Bisimulations on Data Graphs. In KR'16. AAAI Press, 2016.
( PDF  Abstract & BibTeX )

Abstract

Bisimulation provides structural conditions to characterize indistinguishability between nodes on graphlike structures
from an external observer. It is a fundamental notion used
in many areas. However, many applications use graphs where
nodes have data, and where observers can test for equality or
inequality of data values (e.g., asking the attribute ‘name’ of
a node to be different from that of all its neighbors).
The present work constitutes a first investigation of “data
aware” bisimulations on data graphs. We study the problem of
computing such bisimulations, based on the observational indistinguishability
for XPath —a language that extends modal
logic with tests for data equality. We show that in general
the problem is PSPACEcomplete, but identify several restrictions
that yield better complexity bounds (CONP, PTIME)
by controlling suitable parameters of the problem; namely,
the amount of nonlocality allowed, and the class of models
considered (graph, DAG, tree). In particular, this analysis
yields a hierarchy of tractable fragments.

BibTeX

@inproceedings{ABFF16,
author = {Sergio Abriola and
Pablo Barcel{\'{o}} and
Diego Figueira and
Santiago Figueira},
booktitle = {Principles of Knowledge Representation and Reasoning: Proceedings
of the Fifteenth International Conference, {KR} 2016, Cape Town, South
Africa, April 2529, 2016.},
publisher = {{AAAI} Press},
title = {Bisimulations on Data Graphs},
pages = {309318},
year = {2016},
url = {http://www.aaai.org/ocs/index.php/KR/KR16/paper/view/12876},
}
 FL15

Diego Figueira and
Leonid Libkin.
Path Logics for Querying Graphs: Combining Expressiveness and Efficiency. In LICS'15. ACM Press, 2015.
( PDF  Abstract & BibTeX )

Abstract

We study logics expressing properties of paths in graphs that are tailored to querying graph databases: a data model for new applications such as social networks, the Semantic Web, biological data, crime detection, and others. The basic construct of such logics, a regular path query, checks for paths whose labels belong to a regular language. These logics fail to capture two commonly needed features: counting properties, and the ability to compare paths. It is known that regular pathcomparison relations (e.g., Prefix or equality) can be added without significant complexity overhead, however, adding common relations often demanded by applications (e.g., Sub word, subsequence, suffix) results in either undecidability or astronomical complexity. We propose, as a way around this problem, to use automata with counting functionalities, namely Parikh automata. They express many counting properties directly, and they approximate many relations of interest. We prove that with Parikh automata defining both languages and relations used in queries, we retain the low complexity of the standard path logics for graphs. In particular, this gives us efficient approximations to queries with prohibitively high complexity. We extend the best known decidability results by showing that even more expressive classes of relations are possible in query languages (sometimes with restriction on the shape of formulae). We also show that Parikh automata admit two convenient representations by analogs of regular expressions, making them usable in reallife querying.

BibTeX

@inproceedings{FL15,
author = {Diego Figueira and Leonid Libkin},
booktitle = {30th Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS}
2015, Kyoto, Japan, July 610, 2015},
publisher = {{IEEE} Computer Society Press},
title = {Path Logics for Querying Graphs: Combining Expressiveness and Efficiency},
pages = {329340},
year = {2015},
doi = {10.1109/LICS.2015.39},
}
 FL14b

Diego Figueira and
Leonid Libkin.
Pattern Logics and Auxiliary Relations. In CSLLICS'14. ACM Press, 2014.
( PDF  Abstract & BibTeX )

Abstract

A common theme in the study of logics over finite structures is
adding auxiliary predicates to enhance expressiveness and convey
additional information. Examples include adding an order or arithmetic
for capturing complexity classes, or the power of reallife
declarative languages. A recent trend is to add a datavalue comparison
relation to words, trees, and graphs, for capturing modern
data models such as XML and graph databases.
Such additions often result in the loss of good properties of
the underlying logic. Our goal is to show that such a loss can be
avoided if we use patternbased logics, standard in XML and graph
data querying. The essence of such logics is that auxiliary relations
are tested locally with respect to other relations in the structure.
These logics are shown to admit strong versions of Hanf and Gaifman
locality theorems, which are used to prove a homomorphism
preservation theorem, and a decidability result for the satisfiability
problem. We discuss applications of these results to pattern logics
over data forests, and consequently to querying XML data

BibTeX

@inproceedings{FL14b,
address = {Vienna, Austria},
author = {Figueira, Diego and Libkin, Leonid},
booktitle = {Joint Meeting of the TwentyThird {EACSL} Annual Conference on Computer
Science Logic {(CSL)} and the TwentyNinth Annual {ACM/IEEE} Symposium
on Logic in Computer Science (LICS), {CSLLICS} '14},
publisher = {{ACM}},
title = {Pattern logics and auxiliary relations},
pages = {40:140:10},
year = {2014},
doi = {10.1145/2603088.2603136},
}
 FL14

Diego Figueira and Leonid Libkin. Synchronizing Relations on Words. In STACS'14. LIPIcs, 2014. ( PDF  Abstract & BibTeX )

Abstract

While the theory of languages of words is very mature, our understanding of relations on words is still lagging behind. And yet such relations appear in many new applications such as verification of parameterized systems, querying graphstructured data, and information extraction, for instance. Classes of wellbehaved relations typically used in such applications are obtained by adapting some of the equivalent definitions of regularity of words for relations, leading to nonequivalent notions of recognizable, regular, and rational relations.
The goal of this paper is to propose a systematic way of defining classes of relations on words, of which these three classes are just natural examples, and to demonstrate its advantages compared to some of the standard techniques for studying word relations. The key idea is that of a synchronization of a pair of words, which is a word over an extended alphabet. Using it, we define classes of relations via classes of regular languages over a fixed alphabet, just {1,2} for binary relations. We characterize some of the standard classes of relations on words via finiteness of parameters of synchronization languages, called shift, lag, and shiftlag. We describe these conditions in terms of the structure of cycles of graphs underlying automata, thereby showing their decidability. We show that for these classes there exist canonical synchronization languages, and every class of relations can be effectively resynchronized using those canonical representatives. We also give sufficient conditions on synchronization languages, defined in terms of injectivity and surjectivity of their Parikh images, that guarantee closure under intersection and complement of the classes of relations they define.

BibTeX

@inproceedings{FL14,
address = {Lyon, France},
author = {Figueira, Diego and Libkin, Leonid},
booktitle = {{P}roceedings of the 31st {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'14)},
month = mar,
publisher = {LeibnizZentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
title = {Synchronizing Relations on Words},
pages = {93104},
volume = {25},
isbn = {9783939897651},
year = {2014},
DOI = {10.4230/LIPIcs.STACS.2014.518},
}
 FFA14

Diego Figueira,
Santiago Figueira, and
Carlos Areces.
Basic model theory of XPath on data trees. In ICDT'14. ACM Press, 2014.
( PDF  Abstract & BibTeX )

Abstract

We investigate model theoretic properties of XPath with data
(in)equality tests over the class of data trees, i.e., the class of
trees where each node contains a label from a finite alphabet and a
data value from an infinite domain.
We provide notions of (bi)simulations for XPath logics containing
the child, descendant, parent and ancestor axes to navigate
the tree. We show that these notions precisely characterize the
equivalence relation associated with each logic.
We study formula complexity measures consisting of the number of
nested axes and nested subformulas in a formula; these notions are
akin to the notion of quantifier rank in firstorder logic. We show
characterization results for fine grained notions of equivalence and
(bi)simulation that take into account these complexity measures.
We also prove that positive fragments of these logics correspond to
the formulas preserved under (nonsymmetric) simulations.
We show that the logic including the child axis is equivalent to
the fragment of firstorder logic invariant under the corresponding
notion of bisimulation. If upward navigation is allowed the
characterization fails but a weaker result can still be established.
These results hold over the class of possibly
infinite data trees and over the class of finite data trees.
Besides their intrinsic theoretical value, we argue that
bisimulations are useful tools to prove
(non)expressivity results for the logics studied here, and we
substantiate this claim with examples.

BibTeX

@inproceedings{FFA14,
address = {Athens, Greece},
author = {Figueira, Diego and Figueira, Santiago and Areces, Carlos},
booktitle = {{P}roceedings of the 17th {I}nternational {C}onference on {D}atabase {T}heory ({ICDT}'14)},
month = mar,
publisher = {ACM Press},
title = {Basic Model Theory of XPath on Data Trees},
pages = {5060},
year = {2014},
doi = {10.5441/002/icdt.2014.09},
}
 DFP13

Stéphane Demri,
Diego Figueira, and
M. Praveen.
Reasoning about data repetitions with counter systems. In LICS'13. IEEE Computer Society, 2013.
( PDF  Abstract & BibTeX )

Abstract

We study lineartime temporal logics interpreted over data words with multiple attributes. We restrict the atomic formulas to equalities of attribute values in successive positions and to repetitions of attribute values in the future or past. We demonstrate correspondences between satisfiability problems for logics and reachabilitylike decision problems for counter systems. We show that allowing/disallowing atomic formulas expressing repetitions of values in the past corresponds to the reachability/coverability problem in Petri nets. This gives us 2EXPSPACE upper bounds for several satisfiability problems. We prove matching lower bounds by reduction from a reachability problem for a newly introduced class of counter systems. This new class is a succinct version of vector addition systems with states in which counters are accessed via pointers, a poten tially useful feature in other contexts. We strengthen further the correspondences between data logics and counter systems by characterizing the complexity of fragments, extensions and variants of the logic. For instance, we precisely characterize the relationship between the number of attributes allowed in the logic and the number of counters needed in the counter system.

BibTeX

@inproceedings{DFP13,
address = {New Orleans, LA, USA},
author = {Demri, Stéphane and Figueira, Diego and M. Praveen},
booktitle = {{P}roceedings of the 28th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'13)},
month = jun,
publisher = {{IEEE} Computer Society Press},
title = {Reasoning about data repetitions with counter systems},
pages = {3342},
year = {2013},
doi = {10.1109/LICS.2013.8},
}
 Fig13

Diego Figueira. On XPath with transitive axes and data tests. In PODS'13. ACM Press, 2013.
( PDF  Abstract & BibTeX )

Abstract

We study the satisfiability problem for XPath with data equality tests. XPath is a node selecting language for XML documents whose satisfiability problem is known to be undecidable, even for very simple fragments. However, we show that the satisfiability for XPath with the rightward, leftward and downward reflexivetransitive axes (namely followingsiblingorself, precedingsiblingorself, descendantorself) is decidable. Our algorithm yields a complexity of 3ExpSpace, and we also identify an expressiveequivalent normal form for the logic for which the satisfiability problem is in 2ExpSpace. These results are in contrast with the undecidability of the satisfiability problem as soon as we replace the reflexivetransitive axes with just transitive (nonreflexive) ones.

BibTeX

@inproceedings{Fig13,
address = {New York, NY, USA},
author = {Figueira, Diego},
booktitle = {{P}roceedings of the 31st {A}nnual {ACM} {SIGACT}{SIGMOD}{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'13)},
editor = {Fan, Wenfei},
month = jun,
pages = {249260},
publisher = {ACM Press},
title = {On {XP}ath with transitive axes and data tests},
year = {2013},
doi = {10.1145/2463664.2463675},
}
 BBFP12

Vince Bárány,
Mikołaj Bojańczyk,
Diego Figueira, and
Paweł Parys.
Decidable classes of documents for XPath. In FSTTCS'12. LIPIcs, 2012.
( PDF  Abstract & BibTeX )

Abstract

We study the satisfiability problem for XPath over XML documents of bounded depth. We define two parameters, called match width and braid width, that assign a number to any class of documents. We show that for all k, satisfiability for XPath restricted to bounded depth documents with match width at most k is decidable; and that XPath is undecidable on any class of documents with unbounded braid width. We conjecture that these two parameters are equivalent, in the sense that a class of documents has bounded match width iff it has bounded braid width.

BibTeX

@inproceedings{BBFP12,
address = {Hyderabad, India},
author = {B{\'a}r{\'a}ny, Vince and Boja{\'n}czyk, Miko{\l}aj and Figueira, Diego and Parys, Pawe{\l}},
booktitle = {{P}roceedings of {IARCS} Annual Conference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'12)},
month = dec,
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
publisher = {LeibnizZentrum f{\"u}r Informatik},
title = {Decidable classes of documents for {XP}ath},
pages = {99111},
year = {2012},
doi = {10.4230/LIPIcs.FSTTCS.2012.99},
}
 BFL12

Pablo Barceló,
Diego Figueira, and
Leonid Libkin.
Graph Logics with Rational Relations and the Generalized Intersection Problem. In LICS'12. IEEE Computer Society, 2012.
( PDF  Abstract & BibTeX )

Abstract

We investigate some basic questions about the interaction of regular
and rational relations on words. The primary motivation comes from
the study of logics for querying graph topology, which have recently
found numerous applications. Such logics use conditions on paths
expressed by regular languages and relations, but they often need to
be extended by rational relations such as subword or
subsequence. Evaluating formulae in such extended graph logics boils
down to checking nonemptiness of the intersection of rational
relations with regular or recognizable relations (or, more generally,
to the generalized intersection problem, asking whether some
projections of a regular relation have a nonempty intersection with a
given rational relation).
We prove that for several basic and commonly used rational relations,
the intersection problem with regular relations is either undecidable
(e.g., for subword or suffix, and some generalizations), or decidable
with nonprimitiverecursive complexity (e.g., for subsequence
and its generalizations). These results are used to rule out many
classes of graph logics that freely combine regular and rational
relations, as well as to provide the simplest problem related to
verifying lossy channel systems that has nonprimitiverecursive
complexity. We then prove a dichotomy result for logics combining
regular conditions on individual paths and rational relations on
paths, by showing that the syntactic form of formulae classifies them
into either efficiently checkable or undecidable cases. We also give
examples of rational relations for which such logics are decidable
even without syntactic restrictions.

BibTeX

@inproceedings{BFL12,
address = {Dubrovnik, Croatia},
author = {Barcel{\'o}, Pablo and Figueira, Diego and Libkin, Leonid},
booktitle = {{P}roceedings of the 27th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'12)},
month = jun,
publisher = {{IEEE} Computer Society Press},
title = {Graph Logics with Rational Relations and the Generalized Intersection Problem},
pages = {115124},
year = {2012},
doi = {10.1109/LICS.2012.23},
}
 Fig11

Diego Figueira.
A decidable twoway logic on data words. In LICS'11. IEEE Computer Society, 2011.
( PDF  Abstract & BibTeX )

Abstract

We study the satisfiability problem for a logic on data words. A data word is a finite word where every position carries a label from a finite alphabet and a data value from an infinite domain. The logic we consider is twoway, contains future and past modalities, which are considered as reflexive and transitive relations, and data equality and inequality tests. This logic corresponds to the fragment of XPath with the 'following siblingorself' and 'precedingsiblingorself' axes over data words. We show that this problem is decidable, ExpSpace complete. This is surprising considering that with the strict (nonreflexive) navigation relations the satisfiability problem is undecidable. To prove this, we first reduce the problem to a derivation problem for an infinite transition system, and then we show how to abstract this problem into a reachability problem of a finite transition system.

BibTeX

@inproceedings{Fig11,
address = {Toronto, Canada},
author = {Figueira, Diego},
booktitle = {{P}roceedings of the 26th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'11)},
month = jun,
publisher = {{IEEE} Computer Society Press},
title = {A decidable twoway logic on data words},
pages = {365374},
year = {2011},
doi = {10.1109/LICS.2011.18},
}
 FFSS11

Diego Figueira, Santiago Figueira, Sylvain Schmitz and Philippe Schnoebelen. Ackermannian and primitiverecursive bounds with Dickson's Lemma. In LICS'11. IEEE Computer Society, 2011.
( PDF  Abstract & BibTeX )

Abstract

Dickson’s Lemma is a simple yet powerful tool widely used in decidability proofs, especially when dealing with counters or related data structures in algorithmics, verification and modelchecking, constraint solving, logic, etc. While Dickson’s Lemma is wellknown, most computer scientists are not aware of the complexity upper bounds that are entailed by its use. This is mainly because, on this issue, the existing literature is not very accessible.
We propose a new analysis of the length of bad sequences over (N^{k},≤), improving on earlier results and providing upper bounds that are essentially tight. This analysis is complemented by a “user guide” explaining through practical examples how to easily derive complexity upper bounds from Dickson’s Lemma.

BibTeX

@inproceedings{FFSSlics2011,
address = {Toronto, Canada},
author = {Figueira, Diego and Figueira, Santiago and Schmitz, Sylvain and Schnoebelen, {\relax Ph}ilippe},
booktitle = {{P}roceedings of the 26th {A}nnual {IEEE} {S}ymposium on {L}ogic in {C}omputer {S}cience ({LICS}'11)},
month = jun,
publisher = {{IEEE} Computer Society Press},
title = {{A}ckermannian and PrimitiveRecursive Bounds with {D}ickson's Lemma},
url = {http://arxiv.org/abs/1007.2989},
year = {2011},
pages = {269278},
doi = {10.1109/LICS.2011.39},
}
 BF11

Mikołaj Bojańczyk and
Diego Figueira. Efficient evaluation for a temporal logic on changing XML documents. In PODS'11. ACM Press, 2011.
( PDF  Abstract & BibTeX )

Abstract

We consider a sequence t_{1},...,t_{k} of XML documents that is produced by a sequence of local edit operations. To describe properties of such a sequence, we use a temporal logic. The logic can navigate both in time and in the document, e.g. a formula can say that every node with label a eventually gets a descendant with label b. For every fixed formula, we provide an evaluation algorithm that works in time O( k·log(n) ), where k is the number of edit operations and n is the maximal size of document that is produced. In the algorithm, we represent formulas of the logic by a kind of automaton, which works on sequences of documents. The algorithm works on XML documents of bounded depth.

BibTeX

@inproceedings{BF09,
address = {Athens, Greece},
author = {Boja{\'n}czyk, Miko{\l}aj and Figueira, Diego},
booktitle = {{P}roceedings of the 29th {A}nnual {ACM} {SIGACT}{SIGMOD}{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'11)},
DOI = {10.1145/1989284.1989317},
editor = {Schwentick, Thomas},
month = jun,
pages = {259270},
publisher = {ACM Press},
title = {Efficient Evaluation for a Temporal Logic on Changing XML Documents},
year = {2011},
}
 FS11

Diego Figueira and Luc Segoufin. Bottomup automata on data trees and vertical XPath. In STACS'11. LIPIcs, 2011. ( PDF  Abstract & BibTeX )

Abstract

A data tree is a 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 bottomup alternating automaton with one
register, enriched with epsilontransitions that perform tests on the data
values of the subtree. 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.

BibTeX

@inproceedings{FS11,
address = {Dortmund, Germany},
author = {Figueira, Diego and Segoufin, Luc},
booktitle = {{P}roceedings of the 28th {A}nnual {S}ymposium on {T}heoretical {A}spects of {C}omputer {S}cience ({STACS}'11)},
editor = {D{\"u}rr, Christoph and Schwentick, Thomas},
month = mar,
publisher = {LeibnizZentrum f{\"u}r Informatik},
series = {Leibniz International Proceedings in Informatics},
title = {Bottomup automata on data trees and vertical {XP}ath},
pages = {93104},
volume = {9},
year = {2011},
DOI = {10.4230/LIPIcs.STACS.2011.93},
}
 FHL10

Diego Figueira, Piotr Hofman and Sławomir Lasota. Relating timed and register automata. In EXPRESS'10. 2010. ( PDF  Abstract & BibTeX )

Abstract

Timed automata and register automata are wellknown 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 alter nating automata with one clock or register, both with nonprimitive 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.

BibTeX

@inproceedings{FHL10,
address = {Paris, France},
author = {Figueira, Diego and Hofman, Piotr and Lasota, S{\l}awomir},
booktitle = {{P}roceedings of the 17th {I}nternational {W}orkshop on {E}xpressiveness in {C}oncurrency ({EXPRESS}'10)},
editor = {Fr{\"o}schle, Sibylle and Valencia, Franck},
month = aug,
title = {Relating timed and register automata},
url = {http://www.lsv.enscachan.fr/Publis/PAPERS/PDF/FHLexpress10.pdf},
DOI = {10.4204/EPTCS.41.5},
year = {2010},
}
 Fig10

Diego Figueira. ForwardXPath and extended register automata on datatrees. In ICDT'10. ACM Press, 2010. ( PDF  PS  PS.GZ  Abstract & BibTeX )

Abstract

We consider a fragment of XPath named "forwardXPath", which
contains all descendant and rightwards sibling axes as well as data equality
and inequality tests. The satisfiability problem for forwardXPath in the
presence of DTDs and even of primary key constraints is shown here to be
decidable.
To show decidability we introduce a model of alternating
automata on data trees that can move downwards and rightwards in the tree,
have one register for storing data and compare them for equality, and have
the ability to (1) nondeterministically guess a data value and store it, and
(2) quantify universally over the set of data values seen so far during the
run. This model extends the work of Jurdziński and Lazić.
Decidability of the finitary nonemptiness problem for this model is obtained
by a direct reduction to a wellstructured transition system, contrary to
previous approaches.

BibTeX

@inproceedings{Fig10,
address = {Lausanne, Switzerland},
author = {Figueira, Diego},
booktitle = {{P}roceedings of the 13th {I}nternational {C}onference on {D}atabase {T}heory ({ICDT}'10)},
DOI = {10.1145/1804669.1804699},
editor = {Segoufin, Luc},
month = mar,
pages = {230240},
publisher = {ACM Press},
title = {Forward{XP}ath and extended register automata on datatrees},
url = {http://www.lsv.enscachan.fr/Publis/PAPERS/PDF/figicdt10.pdf},
year = {2010},
}
 FS09

Diego Figueira and Luc Segoufin. Futurelooking logics on data words and trees. In MFCS'09, LNCS 5734. Springer, 2009. ( PDF  PS  PS.GZ  Abstract & BibTeX )

Abstract

In a data word or a data tree each position carries a label from
a finite alphabet and a data value from an infinite domain. These models have
been considered in the realm of semistructured data, timed automata and
extended temporal logics.
Over data words we consider the logic
1regLTL(F), that extends LTL(F) with one register
for storing data values for later comparisons. We show that satisfiability
over data words of 1regLTL(F) is already not primitive
recursive. We also show that the extension of 1regLTL(F) with
either the reverse modality F^{1} or with one extra register is
undecidable. All those lower bounds were already known for
1regLTL(X,F) and our results essentially show
that the X modality was not necessary.
Moreover we show that
over data trees similar lower bounds hold for certain fragments of
XPath.

BibTeX

@inproceedings{FS09,
address = {Novy Smokovec, Slovakia},
author = {Figueira, Diego and Segoufin, Luc},
booktitle = {{P}roceedings of the 34th {I}nternational {S}ymposium on {M}athematical {F}oundations of {C}omputer {S}cience ({MFCS}'09)},
DOI = {10.1007/9783642038167_29},
editor = {Kr{\'a}lovi{\v c}, Rastislav and Niwi{\'n}ski, Damian},
month = aug,
pages = {331343},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Futurelooking logics on data words and trees},
url = {http://www.lsv.enscachan.fr/Publis/PAPERS/PDF/FSmfcs09.pdf},
volume = {5734},
year = {2009},
}
 AF09

Carlos Areces and Diego Figueira. Which Semantics for Neighbourhood Semantics? In IJCAI'09. AAAI Press, 2009. ( PDF  PS  PS.GZ  Abstract & BibTeX )

Abstract

In this article we discuss two alternative proposals for
neighbourhood semantics (which we call strict and loose neighbourhood
semantics, NSS and NSL respectively) that have been previously introduced in
the literature. Our main tools are suitable notions of bisimulation. While an
elegant notion of bisimulation exists for NSL, the required bisimulation for
NSS is rather involved. We propose a simple extension of NSS with a universal
modality that we call NSS(E), which comes together with a natural notion of
bisimulation. We also investigate the complexity of the satisfiability
problem for NSL and NSS(E).

BibTeX

@inproceedings{AF09,
address = {Pasadena, CA, USA},
author = {Areces, Carlos and Figueira, Diego},
booktitle = {{P}roceedings of the 21st {I}nternational {J}oint {C}onference on {A}rtificial {I}ntelligence ({IJCAI}'09)},
editor = {Boutilier, Craig},
month = jul,
pages = {671676},
publisher = {AAAI Press},
title = {Which Semantics for Neighbourhood Semantics?},
url = {http://www.lsv.enscachan.fr/Publis/PAPERS/PDF/AFijcai09.pdf},
year = {2009},
}
 AFGM09

Carlos Areces, Diego Figueira, Daniel Gorín and Sergio Mera. Tableaux and Model Checking for Memory Logics. In TABLEAUX'09, LNCS 5607. Springer, 2009. ( PDF  PS  PS.GZ  Abstract & BibTeX )

Abstract

Memory logics are modal logics whose semantics is specified in
terms of relational models enriched with additional data structure to
represent memory. The logical language is then extended with a collection of
operations to access and modify the data structure. In this paper we study
their satisfiability and the model checking problems.
We first give sound
and complete tableaux calculi for the memory logic ML(k,r,e) (the basic
modal language extended with the operator r used to memorize a state, the
operator e used to wipe out the memory, and the operator k used to
check if the current point of evaluation is memorized) and some of its
sublanguages. As the satisfiability problem of ML(k,r,e) is undecidable,
the tableau calculus we present is non terminating. Hence, we furthermore
study a variation that ensures termination, at the expense of completeness,
and we use model checking to ensure soundness. Secondly, we show that the
model checking problem is PSpacecomplete.

BibTeX

@inproceedings{AFGM09,
address = {Oslo, Norway},
author = {Areces, Carlos and Figueira, Diego and Gor{\'\i}n, Daniel and Mera, Sergio},
booktitle = {{P}roceedings of the 18th {I}nternational {W}orkshop on {T}heorem {P}roving with {A}nalytic {T}ableaux and {R}elated {M}ethods ({TABLEAUX}'09)},
DOI = {10.1007/9783642027161_5},
editor = {Giese, Martin and Waaler, Arild},
month = jul,
pages = {4761},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Tableaux and Model Checking for Memory Logics},
url = {http://www.lsv.enscachan.fr/Publis/PAPERS/PDF/AFGMtableaux09.pdf},
volume = {5607},
year = {2009},
}
 Fig09

Diego Figueira. Satisfiability of Downward XPath with Data Equality Tests. In PODS'09. ACM Press, 2009. ( PDF  PS  PS.GZ  Abstract & BibTeX )

Abstract

In this work we investigate the satisfiability problem for the
logic XPath(↓,↓^{*},=), that includes all
downward axes as well as equality and inequality tests. We address this
problem in the absence of DTDs and the sibling axis. We prove that this
fragment is decidable, and we nail down its complexity, showing the problem
to be ExpTimecomplete. The result also holds when path expressions allow
closure under the Kleene star operator. To obtain these results, we introduce
a new automaton model over data trees that captures
XPath(↓,↓^{*},=) and has an ExpTime emptiness
problem. Furthermore, we give the exact complexity of several
downwardlooking fragments.

BibTeX

@inproceedings{Fig09,
address = {Providence, RI, USA},
author = {Figueira, Diego},
booktitle = {{P}roceedings of the 27th {A}nnual {ACM} {SIGACT}{SIGMOD}{SIGART} {S}ymposium on {P}rinciples of {D}atabase {S}ystems ({PODS}'09)},
DOI = {10.1145/1559795.1559827},
editor = {Su, Jianwen},
month = jun # {} # jul,
pages = {197206},
publisher = {ACM Press},
title = {Satisfiability of Downward {XP}ath with
Data Equality Tests},
url = {http://www.lsv.enscachan.fr/Publis/PAPERS/PDF/figpods09.pdf},
year = {2009},
}
 AFFM08

Carlos Areces, Diego Figueira, Santiago Figueira and Sergio Mera. Expressive Power and Decidability for Memory Logics. In WoLLIC'08, LNCS 5110. Springer, 2008. ( PDF  Abstract & BibTeX )

Abstract

We investigate the expressive power of memory logics.
These are modal logics extended with the possibility to store (or remove) the
current node of evaluation in (or from) a memory, and to perform
membership tests on the current memory. From this perspective, the hybrid
logic HL(↓), for example, can be thought of as a
particular case of a memory logic where the memory is an indexed list of
elements of the domain.
This work focuses in the case where the memory is
a set, and we can test whether the current node belongs to the set or not. We
prove that, in terms of expressive power, the memory logics we discuss here
lie between the basic modal logic K and
HL(↓). We show that the satisfiability problem of most
of the logics we cover is undecidable. The only logic with a decidable
satisfiability problem is obtained by imposing strong constraints on which
elements can be memorized.

BibTeX

@inproceedings{AFFM08,
address = {Edinburgh, Scotland, UK},
author = {Areces, Carlos and Figueira, Diego and Figueira, Santiago and Mera, Sergio},
booktitle = {{P}roceedings of the 15th {W}orkshop on {L}ogic, {L}anguage, {I}nformation and {C}omputation ({WoLLIC}'08)},
DOI = {10.1007/9783540699378_7},
editor = {Hodges, Wilfrid and de Queiroz, Ruy},
month = jul,
pages = {5668},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Expressive Power and Decidability for Memory Logics},
url = {http://www.lsv.enscachan.fr/Publis/PAPERS/PDF/AFFMwollic08.pdf},
volume = {5110},
year = {2008},
}
