Publications « back Journals DFP16 .  .  Logical Methods in Computer Science (LMCS), 2016. To appear. ( PDF |  Abstract & BibTeX  ) Abstract    We study linear-time 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 reachability-like 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 .  .  Journal of Artificial Intelligence Research (JAIR) 53: 271-314, 2015. doi:10.1613/jair.4658 ( 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 first-order 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 (non-symmetric) simulations. We show that the logic including the child axis is equivalent to the fragment of first-order 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 bi-simulations 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 = {271--314}, volume = {53}, doi = {10.1613/jair.4658}, year = {2015}, } FL15b .  .  Theory of Computing Systems (ToCS), 2015. To appear. doi:10.1007/s00224-014-9584-2 ( 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 graph-structured data, and information extraction, for instance. Classes of well-behaved relations typically used in such applications are obtained by adapting some of the equivalent definitions of regularity of words for relations, leading to non-equivalent 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 re-synchronized 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 = {287--318} doi = {10.1007/s00224-014-9584-2}, year = {2015}, } BFL13 .  Graph Logics with Rational Relations.  Logical Methods in Computer Science (LMCS), 9(3:1), 2013. doi:10.2168/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 non-primitive-recursive 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 non-primitive-recursive 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/LMCS-9(3:1)2013}, year = {2013}, } FHL12 .  Relating timed and register automata.  Mathematical Structures in Computer Science (MSCS), 2013. To appear. ( Abstract & BibTeX  ) 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 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 non-primitive 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 .  Alternating Register Automata on Finite Data Words and Trees.  Logical Methods in Computer Science (LMCS), 8(1:22), 2012. doi:10.2168/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 one-way 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 so-called 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, next-sibling and following-sibling 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/LMCS-8(1:22)2012}, year = {2012}, } Fig12 .  Decidability of Downward XPath.  ACM Transactions on Computational Logic (TOCL), 2012. doi:10.1145/2362355.2362362 ( PDF | Abstract & BibTeX  ) Abstract     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. 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 .  The Expressive Power of Memory Logics.  The Review of Symbolic Logic (RSL), 2010.doi:10.1017/S1755020310000389 ( 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 = {290-318}, year = {2010}, } Conferences AFF17 , , and Santiago Figueira.  .  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 downward-XPath, which has a non-primitive-recursive 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 control-state reachability for MVASS, as well as its bottom-up 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 .  .  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 trade-off between utility and privacy. In order to balance these two conflicting'' requirements, privacy preserving mechanisms calibrate the added noise to the so-called \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 .  .  In LICS'16. ACM Press, 2016. ??? ( PDF | Abstract & BibTeX  ) Abstract     The evaluation problem for Conjunctive Queries (CQ) is known to be NP-complete in combined complexity and W[1]-hard in parameterized complexity. However, acyclic CQs and CQs of bounded tree-width can be evaluated in polynomial time in combined com- plexity and they are fixed-parameter tractable.     We study the problem of whether a CQ can be rewritten into an equivalent CQ of bounded tree-width, 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 5-8, 2016}, publisher = {{IEEE} Computer Society Press}, title = {Semantically Acyclic Conjunctive Queries under Functional Dependencies}, pages = {??--??}, year = {2016}, doi = {10.1109/???}, } ABFF16 .  .  In KR'16. AAAI Press, 2016. ( PDF | Abstract & BibTeX  ) Abstract     Bisimulation provides structural conditions to characterize indistinguishability between nodes on graph-like 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 PSPACE-complete, but identify several restrictions that yield better complexity bounds (CO-NP, PTIME) by controlling suitable parameters of the problem; namely, the amount of non-locality 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 25-29, 2016.}, publisher = {{AAAI} Press}, title = {Bisimulations on Data Graphs}, pages = {309--318}, year = {2016}, url = {http://www.aaai.org/ocs/index.php/KR/KR16/paper/view/12876}, } FL15 .  .  In LICS'15. ACM Press, 2015. doi:10.1109/LICS.2015.39 ( 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 path-comparison 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 real-life 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 6-10, 2015}, publisher = {{IEEE} Computer Society Press}, title = {Path Logics for Querying Graphs: Combining Expressiveness and Efficiency}, pages = {329--340}, year = {2015}, doi = {10.1109/LICS.2015.39}, } FL14b .  .  In CSL-LICS'14. ACM Press, 2014. 10.1145/2603088.2603136 ( 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 real-life declarative languages. A recent trend is to add a data-value 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 pattern-based 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 Twenty-Third {EACSL} Annual Conference on Computer Science Logic {(CSL)} and the Twenty-Ninth Annual {ACM/IEEE} Symposium on Logic in Computer Science (LICS), {CSL-LICS} '14}, publisher = {{ACM}}, title = {Pattern logics and auxiliary relations}, pages = {40:1--40:10}, year = {2014}, doi = {10.1145/2603088.2603136}, } FL14 .  Synchronizing Relations on Words.  In STACS'14. LIPIcs, 2014. doi:10.4230/LIPIcs.STACS.2014.518 ( 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 graph-structured data, and information extraction, for instance. Classes of well-behaved relations typically used in such applications are obtained by adapting some of the equivalent definitions of regularity of words for relations, leading to non-equivalent 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 re-synchronized 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 = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, title = {Synchronizing Relations on Words}, pages = {93-104}, volume = {25}, isbn = {978-3-939897-65-1}, year = {2014}, DOI = {10.4230/LIPIcs.STACS.2014.518}, } FFA14 .  .  In ICDT'14. ACM Press, 2014. doi:10.5441/002/icdt.2014.09 ( 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 first-order 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 (non-symmetric) simulations. We show that the logic including the child axis is equivalent to the fragment of first-order 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 = {50-60}, year = {2014}, doi = {10.5441/002/icdt.2014.09}, } DFP13 .  .  In LICS'13. IEEE Computer Society, 2013. doi:10.1109/LICS.2013.8 ( PDF | Abstract & BibTeX  ) Abstract     We study linear-time 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 reachability-like 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 = {33-42}, year = {2013}, doi = {10.1109/LICS.2013.8}, } Fig13 .  On XPath with transitive axes and data tests.  In PODS'13. ACM Press, 2013. doi:10.1145/2463664.2463675 ( 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 reflexive-transitive axes (namely following-sibling-or-self, preceding-sibling-or-self, descendant-or-self) is decidable. Our algorithm yields a complexity of 3ExpSpace, and we also identify an expressive-equivalent 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 reflexive-transitive axes with just transitive (non-reflexive) 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 = {249-260}, publisher = {ACM Press}, title = {On {XP}ath with transitive axes and data tests}, year = {2013}, doi = {10.1145/2463664.2463675}, } BBFP12 .  .  In FSTTCS'12. LIPIcs, 2012. doi:10.4230/LIPIcs.FSTTCS.2012.99 ( 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 = {Leibniz-Zentrum f{\"u}r Informatik}, title = {Decidable classes of documents for {XP}ath}, pages = {99-111}, year = {2012}, doi = {10.4230/LIPIcs.FSTTCS.2012.99}, } BFL12 .  .  In LICS'12. IEEE Computer Society, 2012. doi:10.1109/LICS.2012.23 ( 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 non-primitive-recursive 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 non-primitive-recursive 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 = {115--124}, year = {2012}, doi = {10.1109/LICS.2012.23}, } Fig11 .  .  In LICS'11. IEEE Computer Society, 2011. doi:10.1109/LICS.2011.18 ( 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 two-way, 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- sibling-or-self' and 'preceding-sibling-or-self' axes over data words. We show that this problem is decidable, ExpSpace- complete. This is surprising considering that with the strict (non-reflexive) 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 two-way logic on data words}, pages = {365-374}, year = {2011}, doi = {10.1109/LICS.2011.18}, } FFSS11 .  Ackermannian and primitive-recursive bounds with Dickson's Lemma.  In LICS'11. IEEE Computer Society, 2011. doi:10.1109/LICS.2011.39 ( 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 model-checking, constraint solving, logic, etc. While Dickson’s Lemma is well-known, 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 (Nk,≤), 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{FFSS-lics2011, 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 Primitive-Recursive Bounds with {D}ickson's Lemma}, url = {http://arxiv.org/abs/1007.2989}, year = {2011}, pages = {269-278}, doi = {10.1109/LICS.2011.39}, } BF11 .  Efficient evaluation for a temporal logic on changing XML documents.  In PODS'11. ACM Press, 2011. doi:10.1145/1989284.1989317 ( PDF | Abstract & BibTeX  ) Abstract     We consider a sequence t1,...,tk 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 = {259-270}, publisher = {ACM Press}, title = {Efficient Evaluation for a Temporal Logic on Changing XML Documents}, year = {2011}, } FS11 .  Bottom-up automata on data trees and vertical XPath.  In STACS'11. LIPIcs, 2011.doi:10.4230/LIPIcs.STACS.2011.93 ( 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 bottom-up alternating automaton with one register, enriched with epsilon-transitions 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 = {Leibniz-Zentrum f{\"u}r Informatik}, series = {Leibniz International Proceedings in Informatics}, title = {Bottom-up automata on data trees and vertical {XP}ath}, pages = {93-104}, volume = {9}, year = {2011}, DOI = {10.4230/LIPIcs.STACS.2011.93}, } FHL10 .  Relating timed and register automata.  In EXPRESS'10. 2010. doi:10.4204/EPTCS.41.5 ( PDF | Abstract & BibTeX  ) 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 alter- nating 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. 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.ens-cachan.fr/Publis/PAPERS/PDF/FHL-express10.pdf}, DOI = {10.4204/EPTCS.41.5}, year = {2010}, } Fig10 .  Forward-XPath and extended register automata on data-trees.  In ICDT'10. ACM Press, 2010. ( PDF | PS | PS.GZ | Abstract & BibTeX  ) doi:10.1145/1804669.1804699 Abstract     We consider a fragment of XPath named "forward-XPath", which contains all descendant and rightwards sibling axes as well as data equality and inequality tests. The satisfiability problem for forward-XPath 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 non-emptiness problem for this model is obtained by a direct reduction to a well-structured 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 = {230-240}, publisher = {ACM Press}, title = {Forward-{XP}ath and extended register automata on data-trees}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fig-icdt10.pdf}, year = {2010}, } FS09 .  Future-looking logics on data words and trees.  In MFCS'09, LNCS 5734. Springer, 2009. ( PDF | PS | PS.GZ | Abstract & BibTeX  ) doi:10.1007/978-3-642-03816-7_29 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 1-reg-LTL(F), that extends LTL(F) with one register for storing data values for later comparisons. We show that satisfiability over data words of 1-reg-LTL(F) is already not primitive recursive. We also show that the extension of 1-reg-LTL(F) with either the reverse modality F-1 or with one extra register is undecidable. All those lower bounds were already known for 1-reg-LTL(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/978-3-642-03816-7_29}, editor = {Kr{\'a}lovi{\v c}, Rastislav and Niwi{\'n}ski, Damian}, month = aug, pages = {331-343}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Future-looking logics on data words and trees}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FS-mfcs09.pdf}, volume = {5734}, year = {2009}, } AF09 .  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 = {671-676}, publisher = {AAAI Press}, title = {Which Semantics for Neighbourhood Semantics?}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AF-ijcai09.pdf}, year = {2009}, } AFGM09 .  Tableaux and Model Checking for Memory Logics.  In TABLEAUX'09, LNCS 5607. Springer, 2009. ( PDF | PS | PS.GZ | Abstract & BibTeX  ) doi:10.1007/978-3-642-02716-1_5 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 PSpace-complete. 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/978-3-642-02716-1_5}, editor = {Giese, Martin and Waaler, Arild}, month = jul, pages = {47-61}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Tableaux and Model Checking for Memory Logics}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFGM-tableaux09.pdf}, volume = {5607}, year = {2009}, } Fig09 .  Satisfiability of Downward XPath with Data Equality Tests.  In PODS'09. ACM Press, 2009. ( PDF | PS | PS.GZ | Abstract & BibTeX  ) doi:10.1145/1559795.1559827 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 ExpTime-complete. 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 downward-looking 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 = {197-206}, publisher = {ACM Press}, title = {Satisfiability of Downward {XP}ath with Data Equality Tests}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/fig-pods09.pdf}, year = {2009}, } AFFM08 .  Expressive Power and Decidability for Memory Logics.  In WoLLIC'08, LNCS 5110. Springer, 2008. ( PDF | Abstract & BibTeX  ) doi:10.1007/978-3-540-69937-8_7 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/978-3-540-69937-8_7}, editor = {Hodges, Wilfrid and de Queiroz, Ruy}, month = jul, pages = {56-68}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Expressive Power and Decidability for Memory Logics}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/AFFM-wollic08.pdf}, volume = {5110}, year = {2008}, } Theses FigPhD .  Reasoning on words and trees with data.  Ph.D. Thesis, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2010. ( PDF | Summary | Abstract & BibTeX  ) Abstract     A data word (resp. a data tree) is a finite word (resp. tree) whose every position carries a letter from a finite alphabet and a datum form an infinite domain. In this thesis we investigate automata and logics for data words and data trees with decidable reasoning problems: we focus on the emptiness problem in the case of automata, and the satisfiability problem in the case of logics.     On data words, we present a decidable extension of the model of alternating register automata studied by Demri and Lazić. Further, we show the decidability of the satisfiability problem for the linear-time temporal logic on data words LTL(X,F,U) (studied by Demri and Lazić) extended with quantification over data values. We also prove that the lower bounds of non-primitive recursiveness shown by Demri and Lazić for LTL(X,F) carry over to LTL(F).     On data trees, we consider three decidable automata models with different characteristics. We first introduce the Downward Data automaton (DD automata). Its execution consists in a transduction of the finite labeling of the tree, and a verification of data properties for every subtree of the transduced tree. This model is closed under boolean operations, but the tests it can make on the order of the siblings is very limited. Its emptiness problem is in 2ExpTime. On the contrary, the other two automata models we introduce have an emptiness problem with a non-primitive recursive complexity, and are closed under intersection and union, but not complementation. They are both alternating automata with one register to store and compare data values. The automata class ATRA(guess,spread) extends the top-down automata ATRA of Jurdziński and Lazić. We exhibit similar decidable extensions as the one showed in the case of data words. This class can test for any regular tree language, in contrast to DD automata. Finally, we consider a bottom-up alternating tree automaton with one register (called BUDA). Although BUDA are one-way, they can test data properties by navigating the tree in both directions: upward and downward. In opposition to ATRA(guess,spread), this automaton cannot test for properties on the sequence of siblings (like, for example, the order in which labels appear).     All these three models have connections with the logic XPath: a logic conceived for XML documents, which can be seen as data trees. Through the aforementioned automata we show that the satisfiability of three natural fragments of XPath are decidable. These fragments are: downward XPath, where navigation can only be done by child and descendant axes; forward XPath, where navigation also contains the next sibling axis and its transitive closure; and vertical XPath, whose navigation consists in the child, descendant, parent and ancestor axes. Whereas downward XPath is ExpTime-complete, forward and vertical XPath have non-primitive recursive lower bounds. BibTeX @phdthesis{FigPhD, author = {Figueira, Diego}, month = dec, school = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France}, type = {PhD Thesis}, title = {Reasoning on Words and Trees with Data}, url = {http://www.labri.fr/perso/dfigueir/phd/latest/thesisFigueira.pdf}, year = {2010}, } FigMSc .  Bisimulations on Neighbourhood Semantics.  M.Sc. Thesis, Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, Argentina, December 2006. ( PDF (in Spanish) | Abstract & BibTeX  ) Abstract     In this thesis we investigate the modal logic semantics known as Neighbourhood Semantics. There are two alternative deﬁnitions that correspond to diﬀerent logics, the ﬁrst of which was introduced by Montague and Scott in 1970 (N=), and the second by van Benthem some years later (N⊆). We study and deﬁne the notion of bisimulation in both logics, and observe that N= has a complex bisimulation. For this logic we analyse two extensions deﬁning in each case the corresponding bisimulation. We will meet a bisimulation which is intuitive for a classical extension of the basic language with the universal modality: N=(E). In the ﬁnal part of this work, we study the computational complexity of the satisﬁability problem (SAT) of each logic. We show that SAT-N⊆ is in NP (and therefore NP-Complete), and that SAT-N=(E) has an EXP-Time upper-bound. BibTeX @mastersthesis{FigMSc, author = {Figueira, Diego}, month = dec, school = {Departamento de Computaci{\'o}n, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires, Argentina}, type = {MSc thesis}, title = {Bisimulations on Neighbourhood Semantics}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/figueira-m2.pdf}, year = {2006}, } Unpublished Fig12U .  .  In ArXiv. 2012. ( PDF | Abstract & BibTeX  ) Abstract     We study the finite satisfiability problem for first order logic with two variables and two binary relations, corresponding to the induced successor relations of two finite linear orders. We show that the problem is decidable in NExpTime. BibTeX @misc{Fig12U, author = {Figueira, Diego}, journal = {Computing Research Repository (CoRR)}, title = {Satisfiability for two-variable logic with two successor relations on finite linear orders}, year = {2012}, url = {http://arxiv.org/abs/1204.2495}, }