A separation logic for negative dependence

Formal reasoning about hashing-based probabilistic data structures often requires reasoning about random variables where when one variable gets larger (such as the number of elements hashed into one bucket), the others tend to be smaller (like the number of elements hashed into the other buckets). This is an example of negative dependence , a generalization of probabilistic independence that has recently found interesting applications in algorithm design and machine learning. Despite the usefulness of negative dependence for the analyses of probabilistic data structures, existing verification methods cannot establish this property for randomized programs. To fill this gap, we design LINA, a probabilistic separation logic for reasoning about negative dependence. Following recent works on probabilistic separation logic using separating conjunction to reason about the probabilistic independence of random variables, we use separating conjunction to reason about negative dependence. Our assertion logic features two separating conjunctions, one for independence and one for negative dependence. We generalize the logic of bunched implications (BI) to support multiple separating conjunctions, and provide a sound and complete proof system. Notably, the semantics for separating conjunction relies on a non-deterministic , rather than partial, operation for combining resources. By drawing on closure properties for negative dependence, our program logic supports a Frame-like rule for negative dependence and monotone operations. We demonstrate how LINA can verify probabilistic properties of hash-based data structures and balls-into-bins processes.

Efficiency improvement techniques for private intersection-sum protocol using Bloom filter

A private set intersection protocol is one of the secure multi-party computation protocols, and allows participants to compute the intersection of their sets without revealing them to each other. Ion et al. proposed the private intersection-sum protocol (PI-Sum). The PI-Sum is one of the two-party private set intersection protocol. In the PI-Sum, two parties (say Alice and Bob) have the private sets A and B. Moreover, Bob additionaly has a rational integer associated with each element of B. The PI-Sum allows Bob to obtain the sum of the rational integers associated with the elements of $$A \cap B$$ A ∩ B . This paper proposes the efficiency improvement techniques for the PI-Sum. The proposed techniques are based on Bloom filters which are probabilistic data structures. More precisely, this paper proposes three protocols which are modifications of the PI-Sum. The proposed protocols are more efficient than the PI-Sum.

Epipolar Multitarget Velocity Probability Data Association Algorithm Based on the Movement Characteristics of Blasting Fragments

Fragments generated from the blast-fragmentation warhead after blasting are typically multiple, fast, small, and dense. In light of the epipolar multitarget feature of blasting fragments, this paper utilizes the movement characteristics of blasting fragments for modeling. Then, the modeling results are adopted in probabilistic data association (PDA) algorithm of multitarget tracking. A novel epipolar multitarget velocity PDA (VPDA) algorithm is proposed based on the movement characteristics of blasting fragments. This algorithm forms the movement characteristics with the finite element simulation results of warhead blasting fragments, utilizes the Doppler velocity probability to reassign the association probability, and updates the state and covariance of each target through the probability weighted fusion. Simulation results demonstrate that, the computational complexity of the proposed algorithm is close to that of PDA algorithm, and the association success rate and the state value update error approximates to the association effects of joint probabilistic data association (JPDA) algorithm, which can effectively track the fragments with identical velocity while reducing the complexity of the epipolar multitarget tracking algorithm, and can respond to the group target tracking scenario.

PoBery: Possibly-complete Big Data Queries with Probabilistic Data Placement and Scanning

In big data query processing, there is a trade-off between query accuracy and query efficiency, for example, sampling query approaches trade-off query completeness for efficiency. In this article, we argue that query performance can be significantly improved by slightly losing the possibility of query completeness, that is, the chance that a query is complete. To quantify the possibility, we define a new concept, Probability of query Completeness (hereinafter referred to as PC). For example, If a query is executed 100 times, PC = 0.95 guarantees that there are no more than 5 incomplete results among 100 results. Leveraging the probabilistic data placement and scanning, we trade off PC for query performance. In the article, we propose PoBery (POssibly-complete Big data quERY), a method that supports neither complete queries nor incomplete queries, but possibly-complete queries. The experimental results conducted on HiBench prove that PoBery can significantly accelerate queries while ensuring the PC. Specifically, it is guaranteed that the percentage of complete queries is larger than the given PC confidence. Through comparison with state-of-the-art key-value stores, we show that while Drill-based PoBery performs as fast as Drill on complete queries, it is 1.7 ×, 1.1 ×, and 1.5 × faster on average than Drill, Impala, and Hive, respectively, on possibly-complete queries.