We study a generalization for map matching algorithms that includes both geometric approaches such as the Fréchet distance and global weight approaches such as those typically used by Hidden Markov Models. Through this perspective, we discovered an efficient map matching algorithm with respect to the vertex-monotone Fréchet distance while using a heuristic tie-breaker inspired by global weight methods. While the classical Fréchet distance requires parameterizations to be monotone, the vertex-monotone Fréchet distance allows backtracking within edges. Our analysis and experimental evaluations show that relaxing the monotonicity constraint enables significantly faster algorithms without significantly altering the resulting map matched paths.

We study how to compute routes that avoid traffic in road networks. Imperfections in real-time traffic feeds may yield routes with undesirable detours through parking lots or residential areas. The main challenge we address in this work is that of defining and computing paths that incorporate a volatile secondary cost function. We define the problem, study its complexity, and present algorithms that compute routes without undesirable detours. Experiments on continental-sized road networks demonstrate the feasibility of our approach.

Given an undirected, unweighted graph G on n nodes, there is an O(n^2*poly log(n))-time algorithm that computes a data structure called distance oracle of size O(n^{5/3}*poly log(n)) answering approximate distance queries in constant time. For nodes at distance d the distance estimate is between d and 2d + 1. This new distance oracle improves upon the oracles of Patrascu and Roditty (FOCS 2010), Abraham and Gavoille (DISC 2011), and Agarwal and Brighten Godfrey (PODC 2013) in terms of preprocessing time, and upon the oracle of Baswana and Sen (SODA 2004) in terms of stretch. The running time analysis is tight (up to logarithmic factors) due to a recent lower bound of Abboud and Bodwin (STOC 2016). Techniques include dominating sets, sampling, balls, and spanners, and the main contribution lies in the way these techniques are combined. Perhaps the most interesting aspect from a technical point of view is the application of a spanner without incurring its constant additive stretch penalty.

We provide an implementation of an algorithm that, given a triangulated planar graph with m edges, returns a simple cycle that is a 2/3-balanced separator consisting of at most edges. An efficient construction of a short and balanced separator that forms a simple cycle is essential in numerous planar graph algorithms, e.g., for computing shortest paths, minimum cuts, or maximum flows. To the best of our knowledge, this is the first implementation of such a cycle separator algorithm with a worst-case guarantee on the cycle length. We evaluate the performance of our algorithm and compare it to the planar separator algorithms recently studied by Holzer et al. [ESA 2005, ACM Journal of Experimental Algorithms 2009]. Out of these algorithms, only the Fundamental Cycle Separator (FCS) produces a simple cycle separator. However, FCS does not provide a worst-case size guarantee. We demonstrate that (i) our algorithm is competitive across all test cases in terms of running time, balance and cycle length, (ii) it provides worst-case guarantees on the cycle length, significantly outperforming FCS on some instances, and (iii) it scales to large graphs.

Distance oracles are data structures that provide fast (possibly approximate) answers to shortest-path and distance queries in graphs. The tradeoff between the space requirements and the query time of distance oracles is of particular interest and the main focus of this paper. Unless stated otherwise, we assume all graphs to be planar and undirected. In FOCS 2001 (J. ACM 2004), Thorup introduced approximate distance oracles for planar graphs (concurrent with Klein, SODA 2002). Thorup proved that, for any ε > 0 and for any undirected planar graph G = (V, E) on n = |V| nodes, there exists a (1 + ε)-approximate distance oracle using space O(nε−1 log n) such that approximate distance queries can be answered in time O(ε−1). In this paper, we aim at reducing the polynomial dependency on ε−1 and log n, getting the first improvement in the query time-space tradeoff. To simplify the statement of our bounds, we define Ō(·) to hide log log n and log(1/ε) factors. We provide the first oracle with a time-space product that is subquadratic in ε−1. We obtain an oracle with space Ō(n log n) and query time Ō(ε−1). For unweighted graphs we show how the logarithmic dependency on n can be removed. We obtain an oracle with space Ō(n) and query time Ō(ε−1). This bound also holds for graphs with polylogarithmic average edge length, which may be a quite reasonable assumption, e.g., for road networks.

Given a triangulated planar graph G on n vertices and an integer r

We present new and improved methods for efficient shortest-path query processing. Our methods are tailored to work for two specific classes of graphs: graphs with small tree-width and complex networks. Seemingly unrelated at first glance, these two classes of graphs have some commonalities: complex networks are known to have a core--fringe structure with a dense core and a tree-like fringe.

We present new and improved data structures that answer exact node-to-node distance queries in planar graphs. Such data structures are also known as distance oracles. For any directed planar graph on n nodes with non-negative lengths we obtain the following:1 Given a desired space allocation S ∊ [n lg lg n, n2], we show how to construct in Õ(S) time a data structure of size O(S) that answers distance queries in Õ(n/ √S) time per query. The best distance oracles for planar graphs until the current work are due to Cabello (SODA 2006), Chen and Xu (STOC 2000), Djidjev (WG 1996), and Fakcharoenphol and Rao (FOCS 2001). For σ ∊ (1, 4/3) and space S = nσ, we essentially improve the query time from n2/S to . As a consequence, we obtain an improvement over the fastest algorithm for k–many distances in planar graphs whenever k ∊ [√n, n). We provide a linear-space exact distance oracle for planar graphs with query time O(n1/2 + ε) for any constant ε > 0. This is the first such data structure with provable sublinear query time. For edge lengths ≥ 1, we provide an exact distance oracle of space Õ(n) such that for any pair of nodes at distance ℓ the query time is Õ(min{ℓ, √n}). Comparable query performance had been observed experimentally but could not be explained theoretically. Our data structures with superlinear space are based on the following new tool: given a non-self-crossing cycle C with c = O(√n) nodes, we can preprocess G in Õ(n) time to produce a data structure of size O(n lg lg c) that can answer the following queries in Õ(c) time: for a query node u, output the distance from u to all the nodes of C. This data structure builds on and provides an alternative for a related data structure of Klein (SODA 2005), which reports distances to the boundary of a face, rather than a cycle.

Compact routing addresses the tradeoff between table sizes and stretch, which is the worst-case ratio between the length of the path a packet is routed through by the scheme and the length of an actual shortest path from source to destination. We adapt the compact routing scheme by Thorup and Zwick [2001] to optimize it for power-law graphs. We analyze our adapted routing scheme based on the theory of unweighted random power-law graphs with fixed expected degree sequence by Aiello et al. [2000]. Our result is the first analytical bound coupled to the parameter of the power-law graph model for a compact routing scheme. Let n denote the number of nodes in the network. We provide a labeled routing scheme that, after a stretch--5 handshaking step (similar to DNS lookup in TCP/IP), routes messages along stretch--3 paths. We prove that, instead of routing tables with Õ ( n 1/2 ) bits ( Õ suppresses factors logarithmic in n ) as in the general scheme by Thorup and Zwick, expected sizes of O ( n γ log n ) bits are sufficient, and that all the routing tables can be constructed at once in expected time O ( n 1+γ log n ), with γ = τ-22/τ-3 + ε, where τ∈(2,3) is the power-law exponent and ε 0 (which implies ε < γ < 1/3 + ε). Both bounds also hold with probability at least 1-1/ n (independent of ε). The routing scheme is a labeled scheme, requiring a stretch--5 handshaking step. The scheme uses addresses and message headers with O (log n log log n ) bits, with probability at least 1- o (1). We further demonstrate the effectiveness of our scheme by simulations on real-world graphs as well as synthetic power-law graphs. With the same techniques as for the compact routing scheme, we also adapt the approximate distance oracle by Thorup and Zwick [2001, 2005] for stretch-3 and we obtain a new upper bound of expected Õ ( n 1+γ ) for space and preprocessing for random power-law graphs. Our distance oracle is the first one optimized for power-law graphs. Furthermore, we provide a linear-space data structure that can answer 5--approximate distance queries in time at most Õ ( n 1/4+ε ) (similar to γ, the exponent actually depends on τ and lies between ε and 1/4 + ε).

Motivated by the increasing availability of large collections of noisy GPS traces, we present a new data-driven framework for smoothing trajectory data. The framework, which can be viewed of as a generalization of the classical moving average technique, naturally leads to efficient algorithms for various smoothing objectives. We analyze an algorithm based on this framework and provide connections to previous smoothing techniques. We implement a variation of the algorithm to smooth an entire collection of trajectories and show that it performs well on both synthetic data and massive collections of GPS traces.

Routing with multiplicative stretch 3 (which means that the path used by the routing scheme can be up to three times longer than a shortest path) can be done with routing tables of Θ(√n) bits per node. The space lower bound is due to the existence of dense graphs with large girth. Dense graphs can be sparsified to subgraphs, called spanners, with various stretch guarantees. There are spanners with additive stretch guarantees (some even have constant additive stretch) but only very few additive routing schemes are known.

Thorup and Zwick, in their seminal work, introduced the approximate distance oracle, which is a data structure that answers distance queries in a graph. For any integer k, they showed an efficient algorithm to construct an approximate distance oracle using space O(kn1+1/k) that can answer queries in time O(k) with a distance estimate that is at most ¿ = 2k-1 times larger than the actual shortest distance (this ratio is called the stretch).They proved that, under a combinatorial conjecture, their data structure is optimal in terms of space: if a stretch of at most 2k-1 is desired, then the space complexity is at least n1+1/k. Their proof holds even if infinite query time is allowed: it is essentially an "incompressibility" result. Also, the proof only holds for dense graphs, and the best bound it can prove only implies that the size of the data structure is lower bounded by the number of edges of the graph. Naturally, the following question arises: what happens for sparse graphs? In this paper we give a new lower bound for approximate distance oracles in the cell-probe model. This lower bound holds even for sparse (polylog(n)-degree) graphs, and it is not an "incompressibility" bound: we prove a three-way tradeoff between space, stretch, and query time. We show that when the query time is t and the stretch is ¿, then the space S must be S ¿ n1+¿(1/t¿)/lg n. This lower bound follows by a reduction from lopsided set disjointness to distance oracles, based on and motivated by recent work of Patrascu. Our results in fact show that for any high-girth regular graph, an approximate distance oracle that supports efficient queries for all subgraphs of G must obey this tradeoff. We also prove some lemmas that count sets of paths in high-girth regular graphs and high-girth regular expanders, which might be of independent interest.

Distributed hash tables (DHT) are used for data management in P2P environments. However, since most hash functions ignore relations between items, DHTs are not efficient for operations on related items. In this paper, we modify a DHT into a distributed array (DA) that enables efficient operations on logical arrays. The array elements of a DA are placed in a P2P overlay network according to a simple rule such that the load is balanced and the number of messages required to access elements sequentially is reduced. The number of messages required for array operations is much smaller than that for operations on DHTs. We demonstrate this theoretically and experimentally.

Formal methods allow to verify several properties of specifications and implementations. Intra-specification consistency means that a specification does not contradict itself. When specifications evolve over time, one also wants to check inter-specification consistencies, which mean that specifications defined earlier in the development cycle also hold at a later point in time. VDM++ is a popular and easy-to-use formal specification language. It uses testing instead of formal proofs to validate the consistency of specifications. The strictness of validations thus depends on the completeness of the corresponding test suites. Unfortunately, VDM++ does not support the verification of inter-specification consistencies. We define VDM-R, an extension of VDM++, which allows to annotate relationships between specifications. We also provide the tool VR2EvtB to translate from VDM-R to Event-B. Using an Event-B verifier, we can then formally validate intra- and inter-specification consistencies in an almost fully-automated process.

Software model checkers work directly on single-process programs, but not on multiple processes. Conversion of processes into threads, combined with a network model, allows for model checking distributed applications, but does not cover potential communication failures. This paper contributes a fault model for model checking networked programs. If a naive fault model is used, spurious deadlocks may appear, because certain processes are terminated before they can complete a necessary action. Such spurious deadlocks have to be suppressed, as implemented in our model checker extension. Our approach found several faults in existing applications, and scales well because exceptions generated by our tool can be checked individually.