Searcharxiv⌕ Search

arXiv subjects

Zhilin Wu

Publications and source records attributed to Zhilin Wu.

26 records · Page 2Linked to original sources

Regular path queries on graphs with data: A rigid approach

Regular path queries (RPQ) is a classical navigational query formalism for graph databases to specify constraints on labeled paths. Recently, RPQs have been extended by Libkin and Vrgo$\rm \check{c}$ to incorporate data value comparisons among different nodes on paths, called regular path queries with data (RDPQ). It has been shown that the evaluation problem of RDPQs is PSPACE-complete and NLOGSPACE-complete in data complexity. On the other hand, the containment problem of RDPQs is in general undecidable. In this paper, we propose a novel approach to extend regular path queries with data value comparisons, called rigid regular path queries with data (RRDPQ). The main ingredient of this approach is an automata model called nondeterministic rigid register automata (NRRA), in which the data value comparisons are \emph{rigid}, in the sense that if the data value in the current position $x$ is compared to a data value in some other position $y$, then by only using the labels (but not data values), the position $y$ can be uniquely determined from $x$. We show that NRRAs are robust in the sense that nondeterministic, deterministic and two-way variant of NRRAs, as well as an extension of regular expressions, are all of the same expressivity. We then argue that the expressive power of RDPQs are reasonable by demonstrating that for every graph database, there is a localized transformation of the graph database so that every RDPQ in the original graph database can be turned into an equivalent RRDPQ over the transformed one. Finally, we investigate the computational properties of RRDPQs and conjunctive RRDPQs (CRRDPQ). In particular, we show that the containment of CRRDPQs (and RRDPQs) can be decided in 2EXPSPACE.

cs.LO↗

On Injective Embeddings of Tree Patterns

We study three different kinds of embeddings of tree patterns: weakly-injective, ancestor-preserving, and lca-preserving. While each of them is often referred to as injective embedding, they form a proper hierarchy and their computational properties vary (from P to NP-complete). We present a thorough study of the complexity of the model checking problem i.e., is there an embedding of a given tree pattern in a given tree, and we investigate the impact of various restrictions imposed on the tree pattern: bound on the degree of a node, bound on the height, and type of allowed labels and edges.

cs.DB↗

A Decidable Extension of Data Automata

Data automata on data words is a decidable model proposed by Bojańczyk et al. in 2006. Class automata, introduced recently by Bojańczyk and Lasota, is an extension of data automata which unifies different automata models on data words. The nonemptiness of class automata is undecidable, since class automata can simulate two-counter machines. In this paper, a decidable model called class automata with priority class condition, which restricts class automata but strictly extends data automata, is proposed. The decidability of this model is obtained by establishing a correspondence with priority multicounter automata. This correspondence also completes the picture of the links between various class conditions of class automata and various models of counter machines. Moreover, this model is applied to extend a decidability result of Alur, Cerný and Weinstein on the algorithmic analysis of array-accessing programs.

cs.FL↗

Verifying Recursive Active Documents with Positive Data Tree Rewriting

This paper proposes a data tree-rewriting framework for modeling evolving documents. The framework is close to Guarded Active XML, a platform used for handling XML repositories evolving through web services. We focus on automatic verification of properties of evolving documents that can contain data from an infinite domain. We establish the boundaries of decidability, and show that verification of a {\em positive} fragment that can handle recursive service calls is decidable. We also consider bounded model-checking in our data tree-rewriting framework and show that it is $\nexptime$-complete.

cs.DB↗

On the distributed evaluation of recursive queries over graphs

Logical formalisms such as first-order logic (FO) and fixpoint logic (FP) are well suited to express in a declarative manner fundamental graph functionalities required in distributed systems. We show that these logics constitute good abstractions for programming distributed systems as a whole, since they can be evaluated in a fully distributed manner with reasonable complexity upper-bounds. We first prove that FO and FP can be evaluated with a polynomial number of messages of logarithmic size. We then show that the (global) logical formulas can be translated into rule programs describing the local behavior of the nodes of the distributed system, which compute equivalent results. Finally, we introduce local fragments of these logics, which preserve as much as possible the locality of their distributed computation, while offering a rich expressive power for networking functionalities. We prove that they admit tighter upper-bounds with bounded number of messages of bounded size. Finally, we show that the semantics and the complexity of the local fragments are preserved over locally consistent networks as well as anonymous networks, thus showing the robustness of the proposed local logical formalisms.

cs.LO↗

On Distributed Model Checking of MSO on Graphs

We consider distributed model-checking of Monadic Second-Order logic (MSO) on graphs which constitute the topology of communication networks. The graph is thus both the structure being checked and the system on which the distributed computation is performed. We prove that MSO can be distributively model-checked with only a constant number of messages sent over each link for planar networks with bounded diameter, as well as for networks with bounded degree and bounded tree-length. The distributed algorithms rely on nontrivial transformations of linear time sequential algorithms for tree decompositions of bounded tree-width graphs.

cs.LO↗

Logical locality entails frugal distributed computation over graphs

First-order logic is known to have limited expressive power over finite structures. It enjoys in particular the locality property, which states that first-order formulae cannot have a global view of a structure. This limitation ensures on their low sequential computational complexity. We show that the locality impacts as well on their distributed computational complexity. We use first-order formulae to describe the properties of finite connected graphs, which are the topology of communication networks, on which the first-order formulae are also evaluated. We show that over bounded degree networks and planar networks, first-order properties can be frugally evaluated, that is, with only a bounded number of messages, of size logarithmic in the number of nodes, sent over each link. Moreover, we show that the result carries over for the extension of first-order logic with unary counting.

cs.LO↗

Feasibility of Motion Planning on Acyclic and Strongly Connected Directed Graphs

Motion planning is a fundamental problem of robotics with applications in many areas of computer science and beyond. Its restriction to graphs has been investigated in the literature for it allows to concentrate on the combinatorial problem abstracting from geometric considerations. In this paper, we consider motion planning over directed graphs, which are of interest for asymmetric communication networks. Directed graphs generalize undirected graphs, while introducing a new source of complexity to the motion planning problem: moves are not reversible. We first consider the class of acyclic directed graphs and show that the feasibility can be solved in time linear in the product of the number of vertices and the number of arcs. We then turn to strongly connected directed graphs. We first prove a structural theorem for decomposing strongly connected directed graphs into strongly biconnected components.Based on the structural decomposition, we give an algorithm for the feasibility of motion planning on strongly connected directed graphs, and show that it can also be decided in time linear in the product of the number of vertices and the number of arcs.

cs.DM↗