Making the Most of Parallel Composition in Differential Privacy

We show that the ‘optimal’ use of the parallel composition theorem corresponds to finding the size of the largest subset of queries that ‘overlap’ on the data domain, a quantity we call the maximum overlap of the queries. It has previously been shown that a certain instance of this problem, formulated in terms of determining the sensitivity of the queries, is NP-hard, but also that it is possible to use graph-theoretic algorithms, such as finding the maximum clique, to approximate query sensitivity. In this paper, we consider a significant generalization of the aforementioned instance which encompasses both a wider range of differentially private mechanisms and a broader class of queries. We show that for a particular class of predicate queries, determining if they are disjoint can be done in time polynomial in the number of attributes. For this class, we show that the maximum overlap problem remains NP-hard as a function of the number of queries. However, we show that efficient approximate solutions exist by relating maximum overlap to the clique and chromatic numbers of a certain graph determined by the queries. The link to chromatic number allows us to use more efficient approximate algorithms, which cannot be done for the clique number as it may underestimate the privacy budget. Our approach is defined in the general setting of f-differential privacy, which subsumes standard pure differential privacy and Gaussian differential privacy. We prove the parallel composition theorem for f-differential privacy. We evaluate our approach on synthetic and real-world data sets of queries. We show that the approach can scale to large domain sizes (up to 1020000), and that its application can reduce the noise added to query answers by up to 60%.

Data-Driven Convolutional Model for Digital Color Image Demosaicing

Modern digital cameras use specific arrangement of Color Filter Array to sample light wavelength corresponding to visible colors. The most common Color Filter Array is the Bayer filter that samples only one color per pixel. To recover the full resolution image, an interpolation algorithm can be used. This process is called demosaicing and it is one of the first processing stages of a digital imaging pipeline. We introduce a novel data-driven model for demosaicing that takes into account the different requirements for reconstruction of the image Luma and Chrominance channels. The final model is a parallel composition of two reconstruction networks with individual architecture and trained with distinct loss functions. In order to solve the overfitting problem, we prepared a dataset that contains groups of patches that share common chromatic and spectral characteristics. We reported the reconstruction error on noise-free images and measured the effect of random noise and quantization noise in the demosaicing reconstruction. To test our model performance, we implemented the network on NVIDIA Jetson Nano, obtaining an end-to-end running time of less than one second for a full frame 12 MPixel image.

Languages of higher-dimensional automata

We introduce languages of higher-dimensional automata (HDAs) and develop some of their properties. To this end, we define a new category of precubical sets, uniquely naturally isomorphic to the standard one, and introduce a notion of event consistency. HDAs are then finite, labeled, event-consistent precubical sets with distinguished subsets of initial and accepting cells. Their languages are sets of interval orders closed under subsumption; as a major technical step, we expose a bijection between interval orders and a subclass of HDAs. We show that any finite subsumption-closed set of interval orders is the language of an HDA, that languages of HDAs are closed under binary unions and parallel composition, and that bisimilarity implies language equivalence.

A Dynamic Epistemic Logic with Finite Iteration and Parallel Composition

Existing dynamic epistemic logics combine standard epistemic logic with a restricted version of dynamic logic. Instead, we here combine a restricted epistemic logic with a rich version of dynamic logic. The epistemic logic is based on `knowing-whether' operators and basically disallows disjunctions and conjunctions in their scope; it moreover captures `knowing-what'. The dynamic logic has not only all the standard program operators of Propositional Dynamic Logic, but also parallel composition as well as an operator of inclusive nondeterministic composition; its atomic programs are assignments of propositional variables. We show that the resulting dynamic epistemic logic is powerful enough to capture several kinds of sequential and parallel planning, and so both in the unbounded and in the finite horizon version.

Hybrid dynamic logic institutions for event/data-based systems

We propose $$\varepsilon^\downarrow(\mathcal{\vec{D}})$$ ε ↓ ( D → ) -logic as a formal foundation for the specification and development of event-based systems with data states. The framework is presented as an institution in the sense of Goguen and Burstall and the logic itself is parametrised by an underlying institution $$\mathcal{\vec{D}}$$ D → whose structures are used to model data states. $$\varepsilon^\downarrow(\mathcal{\vec{D}})$$ ε ↓ ( D → ) -logic is intended to cover a broad range of abstraction levels from abstract requirements specifications up to constructive specifications. It uses modal diamond and box operators over complex actions adopted from dynamic logic. Atomic actions are pairs "Image missing" where e is an event and $$\psi$$ ψ a state transition predicate capturing the allowed reactions to the event. To write concrete specifications of recursive process structures we integrate (control) state variables and binders of hybrid logic. The semantic interpretation relies on event/data transition systems. For the presentation of constructive specifications we propose operational event/data specifications allowing for familiar, diagrammatic representations by state transition graphs. We show that $$\varepsilon^\downarrow(\mathcal{\vec{D}})$$ ε ↓ ( D → ) -logic is powerful enough to characterise the semantics of an operational specification by a single $$\varepsilon^\downarrow(\mathcal{\vec{D}})$$ ε ↓ ( D → ) -sentence. Thus the whole (formal) development process for event/data-based systems relies on $$\varepsilon^\downarrow(\mathcal{\vec{D}})$$ ε ↓ ( D → ) -logic and its semantics as a common basis. It is supported by a variety of implementation constructors which can express, among others, event refinement and parallel composition. Due to the genericity of the approach, it is also possible to change a data state institution during system development when needed. All steps of our formal treatment are illustrated by a running example.

MP-NeRF: A Massively Parallel Method for Accelerating Protein Structure Reconstruction from Internal Coordinates

The conversion of proteins between internal and cartesian coordinates is a limiting step in many pipelines, such as molecular dynamics simulations and machine learning models. This conversion is typically carried out by sequential or parallel applications of the Natural extension of Reference Frame (NeRF) algorithm. This work proposes a massively parallel NeRF implementation which, depending on the polymer length, achieves speedups between 400-1000x over the previous state-of-the-art NeRF implementation. It accomplishes this by dividing the conversion into three main phases: a parallel composition of the monomer backbone, the assembly of backbone subunits, and the parallel elongation of sidechains; and by batching computations into a minimal number of efficient matrix operations. Special emphasis is placed on reusability and ease of use within diverse pipelines. We open source the code (available at https://github.com/EleutherAI/mp_nerf) and provide a corresponding python package.

Coordination and Control of Hierarchically Organized Interacting Agents

The coordination and control of hierarchically organized interacting agents is an important issue in many applications, e.g., harbor or warehouse automation. A formalism of agents as hierarchical input/output automata is proposed. A system of interacting agents is modeled as the parallel composition of their automata. We extend the usual parallel composition operation of I/O automata with a hierarchical composition operation for refining abstract tasks into lower-level subtasks. We provide an algorithm to synthesize hierarchically organized controllers to coordinate the agents' interactions in order to drive the system toward desired states. Our main contribution regards the formal definition, the representation, the theorems about its properties (i.e., the parallel and hierarchical composition are distributive operations), and the synthesis algorithm, proved to be complete and correct.

Stubborn Sets, Frozen Actions, and Fair Testing

Many partial order methods use some special condition for ensuring that the analysis is not terminated prematurely. In the case of stubborn set methods for safety properties, implementation of the condition is usually based on recognizing the terminal strong components of the reduced state space and, if necessary, expanding the stubborn sets used in their roots. In an earlier study it was pointed out that if the system may execute a cycle consisting of only invisible actions and that cycle is concurrent with the rest of the system in a non-obvious way, then the method may be fooled to construct all states of the full parallel composition. This problem is solved in this study by a method that “freezes” the actions in the cycle. The new method also preserves fair testing equivalence, making it usable for the verification of many progress properties.