OpenRaiser/Intern-Atlas huggingface dataset:
On Termination of Polynomial Programs with Equality Conditions
Venue: arXiv cs.PL 2020
Year: 2020

We investigate the termination problem of a family of multi-path polynomial programs (MPPs), in which all assignments to program variables are polynomials, and test conditions of loops and conditional statements are polynomial equalities. We show that the set of non-terminating inputs (NTI) of such a program is algorithmically computable, thus leading to the decidability of its termination. To the best of our knowledge, the considered family of MPPs is hitherto the largest one for which termination is decidable. We present an explicit recursive function which is essentially Ackermannian, to compute the maximal length of ascending chains of polynomial ideals under a control function, and thereby obtain a complete answer to the questions raised by Seidenberg. This maximal length facilitates a precise complexity analysis of our algorithms for computing the NTI and deciding termination of MPPs. We extend our method to programs with polynomial guarded commands and show how an incomplete procedure for MPPs with inequality guards can be obtained. An application of our techniques to invariant generation of polynomial programs is further presented.
Closed-Form Expressions of Ergodic Capacity and MMSE Achievable Sum Rate for MIMO Jacobi and Rayleigh Fading Channels
Venue: arXiv cs.IT 2020
Year: 2020

Multimode/multicore fibers are expected to provide an attractive solution to overcome the capacity limit of the current optical communication system. In the presence of high cross-talk between modes/cores, the squared singular values of the input/output transfer matrix follow the law of the Jacobi ensemble of random matrices. Assuming that the channel state information is only available at the receiver, we derive a new expression for the ergodic capacity of the MIMO Jacobi fading channel. This expression involves double integrals which can be evaluated easily and efficiently. Moreover, the method used in deriving this expression does not appeal to the classical one-point correlation function of the random matrix model. Using a limiting transition between Jacobi and Laguerre polynomials, we derive a similar formula for the ergodic capacity of the MIMO Rayleigh fading channel. Moreover, we derive a new exact closed form expressions for the achievable sum rate of MIMO Jacobi and Rayleigh fading channels employing linear minimum mean squared error (MMSE) receivers. The analytical results are compared to the results obtained by Monte Carlo simulations and the related results available in the literature, which shows perfect agreement.
Computation of Transition Adjacency Relations Based on Complete Prefix Unfolding (Technical Report)
Venue: arXiv cs.OH 2020
Year: 2020

An increasing number of works have devoted to the application of Transition Adjacency Relation (TAR) as a means to capture behavioral features of business process models. In this paper, we systematically study the efficient TAR derivation from process models using unfolding technique which previously has been used to address the state space explosion when dealing with concurrent behaviors of a Petri net. We reveal and formally describe the equivalence between TAR and Event Adjacency Relation (EAR), the manifestation of TAR in the Complete Prefix Unfolding (CPU) of a Petri net. By computing TARs from CPU using this equivalence, we can alleviate the concurrency caused state-explosion issues. Furthermore, structural boosting rules are categorized, proved and added to the TAR computing algorithm. Formal proofs of correctness and generality of CPU-based TAR computation are provided for the first time by this work, and they significantly expand the range of Petri nets from which TARs can be efficiently derived. Experiments on both industrial and synthesized process models show the effectiveness of proposed CPU-based algorithms as well as the observation that they scale well with the increase in size and concurrency of business process models.
BOLA: Near-Optimal Bitrate Adaptation for Online Videos
Venue: arXiv cs.NI 2020
Year: 2020

Modern video players employ complex algorithms to adapt the bitrate of the video that is shown to the user. Bitrate adaptation requires a tradeoff between reducing the probability that the video freezes (rebuffers) and enhancing the quality of the video. A bitrate that is too high leads to frequent rebuffering, while a bitrate that is too low leads to poor video quality. Video providers segment videos into short segments and encode each segment at multiple bitrates. The video player adaptively chooses the bitrate of each segment to download, possibly choosing different bitrates for successive segments. We formulate bitrate adaptation as a utility-maximization problem and devise an online control algorithm called BOLA that uses Lyapunov optimization to minimize rebuffering and maximize video quality. We prove that BOLA achieves a time-average utility that is within an additive term O(1/V) of the optimal value, for a control parameter V related to the video buffer size. Further, unlike prior work, BOLA does not require prediction of available network bandwidth. We empirically validate BOLA in a simulated network environment using a collection of network traces. We show that BOLA achieves near-optimal utility and in many cases significantly higher utility than current state-of-the-art algorithms. Our work has immediate impact on real-world video players and for the evolving DASH standard for video transmission. We also implemented an updated version of BOLA that is now part of the standard reference player dash.js and is used in production by several video providers such as Akamai, BBC, CBS, and Orange.
Simple Characterizations of Potential Games and Zero-sum Games
Venue: arXiv cs.GT 2020
Year: 2020

We provide several tests to determine whether a game is a potential game or whether it is a zero-sum equivalent game---a game which is strategically equivalent to a zero-sum game in the same way that a potential game is strategically equivalent to a common interest game. We present a unified framework applicable for both potential and zero-sum equivalent games by deriving a simple but useful characterization of these games. This allows us to re-derive known criteria for potential games, as well as obtain several new criteria. In particular, we prove (1) new integral tests for potential games and for zero-sum equivalent games, (2) a new derivative test for zero-sum equivalent games, and (3) a new representation characterization for zero-sum equivalent games.
Can we still avoid automatic face detection?
Venue: arXiv cs.CV 2020
Year: 2020

After decades of study, automatic face detection and recognition systems are now accurate and widespread. Naturally, this means users who wish to avoid automatic recognition are becoming less able to do so. Where do we stand in this cat-and-mouse race? We currently live in a society where everyone carries a camera in their pocket. Many people willfully upload most or all of the pictures they take to social networks which invest heavily in automatic face recognition systems. In this setting, is it still possible for privacy-conscientious users to avoid automatic face detection and recognition? If so, how? Must evasion techniques be obvious to be effective, or are there still simple measures that users can use to protect themselves? In this work, we find ways to evade face detection on Facebook, a representative example of a popular social network that uses automatic face detection to enhance their service. We challenge widely-held beliefs about evading face detection: do our old techniques such as blurring the face region or wearing "privacy glasses" still work? We show that in general, state-of-the-art detectors can often find faces even if the subject wears occluding clothing or even if the uploader damages the photo to prevent faces from being detected.
De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic
Venue: arXiv cs.LO 2020
Year: 2020

This paper explores the proof theory necessary for recommending an expressive but decidable first-order system, named MAV1, featuring a de Morgan dual pair of nominal quantifiers. These nominal quantifiers called `new' and `wen' are distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these nominal quantifiers is they are polarised in the sense that `new' distributes over positive operators while `wen' distributes over negative operators. This greater control of bookkeeping enables private names to be modelled in processes embedded as formulae in MAV1. The technical challenge is to establish a cut elimination result, from which essential properties including the transitivity of implication follow. Since the system is defined using the calculus of structures, a generalisation of the sequent calculus, novel techniques are employed. The proof relies on an intricately designed multiset-based measure of the size of a proof, which is used to guide a normalisation technique called splitting. The presence of equivariance, which swaps successive quantifiers, induces complex inter-dependencies between nominal quantifiers, additive conjunction and multiplicative operators in the proof of splitting. Every rule is justified by an example demonstrating why the rule is necessary for soundly embedding processes and ensuring that cut elimination holds.
A Constant Approximation Algorithm for Scheduling Packets on Line Networks
Venue: arXiv cs.DS 2020
Year: 2020

In this paper we improve the approximation ratio for the problem of scheduling packets on line networks with bounded buffers, where the aim is that of maximizing the throughput. Each node in the network has a local buffer of bounded size $B$, and each edge (or link) can transmit a limited number, $c$, of packets in every time unit. The input to the problem consists of a set of packet requests, each defined by a source node, a destination node, and a release time. We denote by $n$ the size of the network. A solution for this problem is a schedule that delivers (some of the) packets to their destinations without violating the capacity constraints of the network (buffers or edges). Our goal is to design an efficient algorithm that computes a schedule that maximizes the number of packets that arrive to their respective destinations. We give a randomized approximation algorithm with constant approximation ratio for the case where $B=Θ(c)$. This improves over the previously best result of $O(\log^* n)$ (Räcke and Rosén, Theory Comput. Syst., 49(4), 2011). Our improvement is based on a new combinatorial lemma that we prove, stating, roughly speaking, that if packets are allowed to stay put in buffers only a limited number of time steps, $2d$, where $d$ is the longest source-destination distance of any input packet, then the cardinality of the optimal solution is decreased by only a constant factor. This claim was not previously known in the directed integral (i.e., unsplittable, zero-one) case, and may find additional applications for routing and scheduling algorithms.
On the additive chromatic number of several families of graphs
Venue: arXiv cs.DM 2020
Year: 2020

The Additive Coloring Problem is a variation of the Coloring Problem where labels of $\{1,\ldots,k\}$ are assigned to the vertices of a graph $G$ so that the sum of labels over the neighborhood of each vertex is a proper coloring of $G$. The least value $k$ for which $G$ admits such labeling is called \emph{additive chromatic number} of $G$. This problem was first presented by Czerwiński, Grytczuk and Żelazny who also proposed a conjecture that for every graph $G$, the additive chromatic number never exceeds the classic chromatic number. Up to date, the conjecture has been proved for complete graphs, trees, non-3-colorable planar graphs with girth at least 13 and non-bipartite planar graphs with girth at least 26. In this work, we show that the conjecture holds for split graphs. We also present exact formulas for computing the additive chromatic number for some subfamilies of split graphs (complete split, headless spiders and complete sun), regular bipartite, complete multipartite, fan, windmill, circuit, wheel, cycle sun and wheel sun.
Probably Approximately Correct Greedy Maximization with Efficient Bounds on Information Gain for Sensor Selection
Venue: arXiv cs.AI 2020
Year: 2020

Submodular function maximization finds application in a variety of real-world decision-making problems. However, most existing methods, based on greedy maximization, assume it is computationally feasible to evaluate F, the function being maximized. Unfortunately, in many realistic settings F is too expensive to evaluate exactly even once. We present probably approximately correct greedy maximization, which requires access only to cheap anytime confidence bounds on F and uses them to prune elements. We show that, with high probability, our method returns an approximately optimal set. We propose novel, cheap confidence bounds for conditional entropy, which appears in many common choices of F and for which it is difficult to find unbiased or bounded estimates. Finally, results on a real-world dataset from a multi-camera tracking system in a shopping mall demonstrate that our approach performs comparably to existing methods, but at a fraction of the computational cost.
Using Private and Public Assessments in Security Information Sharing Agreements
Venue: arXiv cs.GT 2020
Year: 2020

Information sharing among organizations has been gaining attention as a method for improving cybersecurity. However, the associated disclosure costs act as deterrents for firms' voluntary cooperation. In this work, we take a game-theoretic approach to understanding firms' incentives in these agreements. We propose the design of inter-temporal incentives (i.e. conditioning future cooperation on past interactions). Specifically, we show that incentives for full cooperation can be designed if firms share their private assessments of other firms' disclosure decisions through a common communication platform. We further show that similar incentives can be designed based on outcomes of a public rating/assessment system.
A metric on the space of finite sets of trajectories for evaluation of multi-target tracking algorithms
Venue: arXiv cs.CV 2020
Year: 2020

In this paper, we propose a metric on the space of finite sets of trajectories for assessing multi-target tracking algorithms in a mathematically sound way. The main use of the metric is to compare estimates of trajectories from different algorithms with the ground truth of trajectories. The proposed metric includes intuitive costs associated to localization error for properly detected targets, missed and false targets and track switches at each time step. The metric computation is based on solving a multi-dimensional assignment problem. We also propose a lower bound for the metric, which is also a metric for sets of trajectories and is computable in polynomial time using linear programming. We also extend the proposed metrics on sets of trajectories to random finite sets of trajectories.
Efficient Feature-based Image Registration by Mapping Sparsified Surfaces
Venue: arXiv cs.GR 2020
Year: 2020

With the advancement in the digital camera technology, the use of high resolution images and videos has been widespread in the modern society. In particular, image and video frame registration is frequently applied in computer graphics and film production. However, conventional registration approaches usually require long computational time for high resolution images and video frames. This hinders the application of the registration approaches in the modern industries. In this work, we first propose a new image representation method to accelerate the registration process by triangulating the images effectively. For each high resolution image or video frame, we compute an optimal coarse triangulation which captures the important features of the image. Then, we apply a surface registration algorithm to obtain a registration map which is used to compute the registration of the high resolution image. Experimental results suggest that our overall algorithm is efficient and capable to achieve a high compression rate while the accuracy of the registration is well retained when compared with the conventional grid-based approach. Also, the computational time of the registration is significantly reduced using our triangulation-based approach.
Founded Semantics and Constraint Semantics of Logic Rules
Venue: arXiv cs.LO 2020
Year: 2020

Logic rules and inference are fundamental in computer science and have been studied extensively. However, prior semantics of logic languages can have subtle implications and can disagree significantly, on even very simple programs, including in attempting to solve the well-known Russell's paradox. These semantics are often non-intuitive and hard-to-understand when unrestricted negation is used in recursion. This paper describes a simple new semantics for logic rules, founded semantics, and its straightforward extension to another simple new semantics, constraint semantics, that unify the core of different prior semantics. The new semantics support unrestricted negation, as well as unrestricted existential and universal quantifications. They are uniquely expressive and intuitive by allowing assumptions about the predicates, rules, and reasoning to be specified explicitly, as simple and precise binary choices. They are completely declarative and relate cleanly to prior semantics. In addition, founded semantics can be computed in linear time in the size of the ground program.
Minimum Rectilinear Polygons for Given Angle Sequences
Venue: arXiv cs.CG 2020
Year: 2020

A rectilinear polygon is a polygon whose edges are axis-aligned. Walking counterclockwise on the boundary of such a polygon yields a sequence of left turns and right turns. The number of left turns always equals the number of right turns plus 4. It is known that any such sequence can be realized by a rectilinear polygon. In this paper, we consider the problem of finding realizations that minimize the perimeter or the area of the polygon or the area of the bounding box of the polygon. We show that all three problems are NP-hard in general. This answers an open question of Patrignani [CGTA 2001], who showed that it is NP-hard to minimize the area of the bounding box of an orthogonal drawing of a given planar graph. We also show that realizing polylines with minimum bounding box area is NP-hard. Then we consider the special cases of $x$-monotone and $xy$-monotone rectilinear polygons. For these, we can optimize the three objectives efficiently.
Manifold Approximation by Moving Least-Squares Projection (MMLS)
Venue: arXiv cs.GR 2020
Year: 2020

In order to avoid the curse of dimensionality, frequently encountered in Big Data analysis, there was a vast development in the field of linear and nonlinear dimension reduction techniques in recent years. These techniques (sometimes referred to as manifold learning) assume that the scattered input data is lying on a lower dimensional manifold, thus the high dimensionality problem can be overcome by learning the lower dimensionality behavior. However, in real life applications, data is often very noisy. In this work, we propose a method to approximate $\mathcal{M}$ a $d$-dimensional $C^{m+1}$ smooth submanifold of $\mathbb{R}^n$ ($d \ll n$) based upon noisy scattered data points (i.e., a data cloud). We assume that the data points are located "near" the lower dimensional manifold and suggest a non-linear moving least-squares projection on an approximating $d$-dimensional manifold. Under some mild assumptions, the resulting approximant is shown to be infinitely smooth and of high approximation order (i.e., $O(h^{m+1})$, where $h$ is the fill distance and $m$ is the degree of the local polynomial approximation). The method presented here assumes no analytic knowledge of the approximated manifold and the approximation algorithm is linear in the large dimension $n$. Furthermore, the approximating manifold can serve as a framework to perform operations directly on the high dimensional data in a computationally efficient manner. This way, the preparatory step of dimension reduction, which induces distortions to the data, can be avoided altogether.
Convexity and Order in Probabilistic Call-by-Name FPC
Venue: arXiv cs.LO 2020
Year: 2020

Kegelspitzen are mathematical structures coined by Keimel and Plotkin, in order to encompass the structure of a convex set and the structure of a dcpo. In this paper, we ask ourselves what are Kegelspitzen the model of. We adopt a categorical viewpoint and show that Kegelspitzen model stochastic matrices onto a category of domains. Consequently, Kegelspitzen form a denotational model of pPCF, an abstract functional programming language for probabilistic computing. We conclude the present work with a discussion of the interpretation of (probabilistic) recursive types, which are types for entities which might contain other entities of the same type, such as lists and trees.
Rectifier Neural Network with a Dual-Pathway Architecture for Image Denoising
Venue: arXiv cs.CV 2020
Year: 2020

Recently deep neural networks based on tanh activation function have shown their impressive power in image denoising. In this letter, we try to use rectifier function instead of tanh and propose a dual-pathway rectifier neural network by combining two rectifier neurons with reversed input and output weights in the same hidden layer. We drive the equivalent activation function and compare it to some typical activation functions for image denoising under the same network architecture. The experimental results show that our model achieves superior performances faster especially when the noise is small.
Efficient Error-tolerant Search on Knowledge Graphs
Venue: arXiv cs.DB 2020
Year: 2020

Edge-labeled graphs are widely used to describe relationships between entities in a database. Given a query subgraph that represents an example of what the user is searching for, we study the problem of efficiently searching for similar subgraphs in a large data graph, where the similarity is defined in terms of the well-known graph edit distance. We call these queries "error-tolerant exemplar queries" since matches are allowed despite small variations in the graph structure and the labels. The problem in its general case is computationally intractable, but efficient solutions are reachable for labeled graphs under well-behaved distribution of the labels, commonly found in knowledge graphs. We propose two efficient exact algorithms, based on a filtering-and-verification framework, for finding subgraphs in a large data graph that are isomorphic to a query graph under some edit operations. Our filtering scheme, which uses the neighbourhood structure around a node and the presence or absence of paths, significantly reduces the number of candidates that are passed to the verification stage. Moreover, we analyze the costs of our algorithms and the conditions under which one algorithm is expected to outperform the other. Our analysis identifies some of the variables that affect the cost, including the number and the selectivity of query edge labels and the degree of nodes in the data graph, and characterizes their relationships. We empirically evaluate the effectiveness of our filtering schemes and queries, the efficiency of our algorithms and the reliability of our cost models on real datasets.