OpenRaiser/Intern-Atlas huggingface dataset:
Optimal controller synthesis for timed systems
Venue: arXiv cs.LO 2023
Year: 2023

Weighted timed games are zero-sum games played by two players on a timed automaton equipped with weights, where one player wants to minimise the cumulative weight while reaching a target. Used in a reactive synthesis perspective, this quantitative extension of timed games allows one to measure the quality of controllers in real-time systems. Weighted timed games are notoriously difficult and quickly undecidable, even when restricted to non-negative weights. For non-negative weights, the largest class that can be analysed has been introduced by Bouyer, Jaziri and Markey in 2015. Though the value problem is undecidable, the authors show how to approximate the value by considering regions with a refined granularity. In this work, we extend this class to incorporate negative weights, allowing one to model energy for instance, and prove that the value can still be approximated, with the same complexity. A small restriction also allows us to obtain a class of decidable weighted timed games with negative weights and an arbitrary number of clocks. In addition, we show that a symbolic algorithm, relying on the paradigm of value iteration, can be used as an approximation/computation schema over these classes. We also consider the special case of untimed weighted games, where the same fragments are solvable in polynomial time: this contrasts with the pseudo-polynomial complexity, known so far, for weighted games without restrictions.
There is no APTAS for 2-dimensional vector bin packing: Revisited
Venue: arXiv cs.DS 2023
Year: 2023

We study the Vector Bin Packing and the Vector Bin Covering problems, multidimensional generalizations of the Bin Packing and the Bin Covering problems, respectively. In the Vector Bin Packing, we are given a set of $d$-dimensional vectors from $[0,1]^d$ and the aim is to partition the set into the minimum number of bins such that for each bin $B$, each component of the sum of the vectors in $B$ is at most 1. Woeginger [Woe97] claimed that the problem has no APTAS for dimensions greater than or equal to 2. We note that there was a slight oversight in the original proof. In this work, we give a revised proof using some additional ideas from [BCKS06,CC09]. In fact, we show that it is NP-hard to get an asymptotic approximation ratio better than $\frac{600}{599}$. An instance of Vector Bin Packing is called $δ$-skewed if every item has at most one dimension greater than $δ$. As a natural extension of our general $d$-Dimensional Vector Bin Packing result we show that for $\varepsilon\in (0,\frac{1}{2500})$ it is NP-hard to obtain a $(1+\varepsilon)$-approximation for $δ$-Skewed Vector Bin Packing if $δ>20\sqrt \varepsilon$. In the Vector Bin Covering problem given a set of $d$-dimensional vectors from $[0,1]^d$, the aim is to obtain a family of disjoint subsets (called bins) with the maximum cardinality such that for each bin $B$, each component of the sum of the vectors in $B$ is at least 1. Using ideas similar to our Vector Bin Packing result, we show that for Vector Bin Covering there is no APTAS for dimensions greater than or equal to 2. In fact, we show that it is NP-hard to get an asymptotic approximation ratio better than $\frac{998}{997}$.
Semantic Bounds and Strong Call-by-Value Normalization
Venue: arXiv cs.LO 2023
Year: 2023

This paper explores two topics at once: the use of denotational semantics to bound the evaluation length of functional programs, and the semantics of strong (that is, possibly under abstractions) call-by-value evaluation. About the first, we analyze de Carvalho's seminal use of relational semantics for bounding the evaluation length of lambda-terms, starting from the presentation of the semantics as an intersection types system. We focus on the part of his work which is usually neglected in its many recent adaptations, despite being probably the conceptually deeper one: how to transfer the bounding power from the type system to the relational semantics itself. We dissect this result and re-understand it via the isolation of a simpler size representation property. About the second, we use relational semantics to develop a semantical study of strong call-by-value evaluation, which is both a delicate and neglected topic. We give a semantic characterization of terms normalizable with respect to strong evaluation, providing in particular the first result of adequacy with respect to strong call-by-value. Moreover, we extract bounds about strong evaluation from both the type systems and the relational semantics. Essentially, we use strong call-by-value to revisit de Carvalho's semantic bounds, and de Carvalho's technique to provide semantical foundations for strong call-by-value.
Randomized Histogram Matching: A Simple Augmentation for Unsupervised Domain Adaptation in Overhead Imagery
Venue: arXiv cs.CV 2023
Year: 2023

Modern deep neural networks (DNNs) are highly accurate on many recognition tasks for overhead (e.g., satellite) imagery. However, visual domain shifts (e.g., statistical changes due to geography, sensor, or atmospheric conditions) remain a challenge, causing the accuracy of DNNs to degrade substantially and unpredictably when testing on new sets of imagery. In this work, we model domain shifts caused by variations in imaging hardware, lighting, and other conditions as non-linear pixel-wise transformations, and we perform a systematic study indicating that modern DNNs can become largely robust to these types of transformations, if provided with appropriate training data augmentation. In general, however, we do not know the transformation between two sets of imagery. To overcome this, we propose a fast real-time unsupervised training augmentation technique, termed randomized histogram matching (RHM). We conduct experiments with two large benchmark datasets for building segmentation and find that despite its simplicity, RHM consistently yields similar or superior performance compared to state-of-the-art unsupervised domain adaptation approaches, while being significantly simpler and more computationally efficient. RHM also offers substantially better performance than other comparably simple approaches that are widely used for overhead imagery.
Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets
Venue: arXiv cs.LO 2023
Year: 2023

We prove that the well-known (strong) fully-concurrent bisimilarity and the novel i-causal-net bisimilarity, which is a sligtlhy coarser variant of causal-net bisimilarity, are decidable for finite bounded Petri nets. The proofs are based on a generalization of the ordered marking proof technique that Vogler used to demonstrate that (strong) fully-concurrent bisimilarity (or, equivalently, history-preserving bisimilarity) is decidable on finite safe nets.
Paraphrastic Representations at Scale
Venue: arXiv cs.CL 2023
Year: 2023

We present a system that allows users to train their own state-of-the-art paraphrastic sentence representations in a variety of languages. We also release trained models for English, Arabic, German, French, Spanish, Russian, Turkish, and Chinese. We train these models on large amounts of data, achieving significantly improved performance from the original papers proposing the methods on a suite of monolingual semantic similarity, cross-lingual semantic similarity, and bitext mining tasks. Moreover, the resulting models surpass all prior work on unsupervised semantic textual similarity, significantly outperforming even BERT-based models like Sentence-BERT (Reimers and Gurevych, 2019). Additionally, our models are orders of magnitude faster than prior work and can be used on CPU with little difference in inference speed (even improved speed over GPU when using more CPU cores), making these models an attractive choice for users without access to GPUs or for use on embedded devices. Finally, we add significantly increased functionality to the code bases for training paraphrastic sentence models, easing their use for both inference and for training them for any desired language with parallel data. We also include code to automatically download and preprocess training data.
Causality-based Counterfactual Explanation for Classification Models
Venue: arXiv cs.LG 2023
Year: 2023

Counterfactual explanation is one branch of interpretable machine learning that produces a perturbation sample to change the model's original decision. The generated samples can act as a recommendation for end-users to achieve their desired outputs. Most of the current counterfactual explanation approaches are the gradient-based method, which can only optimize the differentiable loss functions with continuous variables. Accordingly, the gradient-free methods are proposed to handle the categorical variables, which however have several major limitations: 1) causal relationships among features are typically ignored when generating the counterfactuals, possibly resulting in impractical guidelines for decision-makers; 2) the counterfactual explanation algorithm requires a great deal of effort into parameter tuning for dertermining the optimal weight for each loss functions which must be conducted repeatedly for different datasets and settings. In this work, to address the above limitations, we propose a prototype-based counterfactual explanation framework (ProCE). ProCE is capable of preserving the causal relationship underlying the features of the counterfactual data. In addition, we design a novel gradient-free optimization based on the multi-objective genetic algorithm that generates the counterfactual explanations for the mixed-type of continuous and categorical features. Numerical experiments demonstrate that our method compares favorably with state-of-the-art methods and therefore is applicable to existing prediction models. All the source codes and data are available at \url{https://github.com/tridungduong16/multiobj-scm-cf}.
Simulation by Rounds of Letter-to-Letter Transducers
Venue: arXiv cs.FL 2023
Year: 2023

Letter-to-letter transducers are a standard formalism for modeling reactive systems. Often, two transducers that model similar systems differ locally from one another, by behaving similarly, up to permutations of the input and output letters within "rounds". In this work, we introduce and study notions of simulation by rounds and equivalence by rounds of transducers. In our setting, words are partitioned to consecutive subwords of a fixed length $k$, called rounds. Then, a transducer $\mathcal{T}_1$ is $k$-round simulated by transducer $\mathcal{T}_2$ if, intuitively, for every input word $x$, we can permute the letters within each round in $x$, such that the output of $\mathcal{T}_2$ on the permuted word is itself a permutation of the output of $\mathcal{T}_1$ on $x$. Finally, two transducers are $k$-round equivalent if they simulate each other. We solve two main decision problems, namely whether $\mathcal{T}_2$ $k$-round simulates $\mathcal{T}_1$ (1) when $k$ is given as input, and (2) for an existentially quantified $k$. We demonstrate the usefulness of the definitions by applying them to process symmetry: a setting in which a permutation in the identities of processes in a multi-process system naturally gives rise to two transducers, whose $k$-round equivalence corresponds to stability against such permutations.
Attention for Image Registration (AiR): an unsupervised Transformer approach
Venue: arXiv cs.CV 2023
Year: 2023

Image registration is a crucial task in signal processing, but it often encounters issues with stability and efficiency. Non-learning registration approaches rely on optimizing similarity metrics between fixed and moving images, which can be expensive in terms of time and space complexity. This problem can be exacerbated when the images are large or there are significant deformations between them. Recently, deep learning, specifically convolutional neural network (CNN)-based methods, have been explored as an effective solution to the weaknesses of non-learning approaches. To further advance learning approaches in image registration, we introduce an attention mechanism in the deformable image registration problem. Our proposed approach is based on a Transformer framework called AiR, which can be efficiently trained on GPGPU devices. We treat the image registration problem as a language translation task and use the Transformer to learn the deformation field. The method learns an unsupervised generated deformation map and is tested on two benchmark datasets. In summary, our approach shows promising effectiveness in addressing stability and efficiency issues in image registration tasks. The source code of AiR is available on Github.
Towards Inference Delivery Networks: Distributing Machine Learning with Optimality Guarantees
Venue: arXiv cs.NI 2023
Year: 2023

An increasing number of applications rely on complex inference tasks that are based on machine learning (ML). Currently, there are two options to run such tasks: either they are served directly by the end device (e.g., smartphones, IoT equipment, smart vehicles), or offloaded to a remote cloud. Both options may be unsatisfactory for many applications: local models may have inadequate accuracy, while the cloud may fail to meet delay constraints. In this paper, we present the novel idea of inference delivery networks (IDNs), networks of computing nodes that coordinate to satisfy ML inference requests achieving the best trade-off between latency and accuracy. IDNs bridge the dichotomy between device and cloud execution by integrating inference delivery at the various tiers of the infrastructure continuum (access, edge, regional data center, cloud). We propose a distributed dynamic policy for ML model allocation in an IDN by which each node dynamically updates its local set of inference models based on requests observed during the recent past plus limited information exchange with its neighboring nodes. Our policy offers strong performance guarantees in an adversarial setting and shows improvements over greedy heuristics with similar complexity in realistic scenarios.
DAMOV: A New Methodology and Benchmark Suite for Evaluating Data Movement Bottlenecks
Venue: arXiv cs.AR 2023
Year: 2023

Data movement between the CPU and main memory is a first-order obstacle against improving performance, scalability, and energy efficiency in modern systems. Computer systems employ a range of techniques to reduce overheads tied to data movement, spanning from traditional mechanisms (e.g., deep multi-level cache hierarchies, aggressive hardware prefetchers) to emerging techniques such as Near-Data Processing (NDP), where some computation is moved close to memory. Our goal is to methodically identify potential sources of data movement over a broad set of applications and to comprehensively compare traditional compute-centric data movement mitigation techniques to more memory-centric techniques, thereby developing a rigorous understanding of the best techniques to mitigate each source of data movement. With this goal in mind, we perform the first large-scale characterization of a wide variety of applications, across a wide range of application domains, to identify fundamental program properties that lead to data movement to/from main memory. We develop the first systematic methodology to classify applications based on the sources contributing to data movement bottlenecks. From our large-scale characterization of 77K functions across 345 applications, we select 144 functions to form the first open-source benchmark suite (DAMOV) for main memory data movement studies. We select a diverse range of functions that (1) represent different types of data movement bottlenecks, and (2) come from a wide range of application domains. Using NDP as a case study, we identify new insights about the different data movement bottlenecks and use these insights to determine the most suitable data movement mitigation mechanism for a particular application. We open-source DAMOV and the complete source code for our new characterization methodology at https://github.com/CMU-SAFARI/DAMOV.
Bounding Information Leakage in Machine Learning
Venue: arXiv cs.LG 2023
Year: 2023

Recently, it has been shown that Machine Learning models can leak sensitive information about their training data. This information leakage is exposed through membership and attribute inference attacks. Although many attack strategies have been proposed, little effort has been made to formalize these problems. We present a novel formalism, generalizing membership and attribute inference attack setups previously studied in the literature and connecting them to memorization and generalization. First, we derive a universal bound on the success rate of inference attacks and connect it to the generalization gap of the target model. Second, we study the question of how much sensitive information is stored by the algorithm about its training set and we derive bounds on the mutual information between the sensitive attributes and model parameters. Experimentally, we illustrate the potential of our approach by applying it to both synthetic data and classification tasks on natural images. Finally, we apply our formalism to different attribute inference strategies, with which an adversary is able to recover the identity of writers in the PenDigits dataset.
Distributed Graph Coloring Made Easy
Venue: arXiv cs.DS 2023
Year: 2023

In this paper we present a deterministic CONGEST algorithm to compute an $O(kΔ)$-vertex coloring in $O(Δ/k)+\log^* n$ rounds, where $Δ$ is the maximum degree of the network graph and $1\leq k\leq O(Δ)$ can be freely chosen. The algorithm is extremely simple: Each node locally computes a sequence of colors and then it "tries colors" from the sequence in batches of size $k$. Our algorithm subsumes many important results in the history of distributed graph coloring as special cases, including Linial's color reduction [Linial, FOCS'87], the celebrated locally iterative algorithm from [Barenboim, Elkin, Goldenberg, PODC'18], and various algorithms to compute defective and arbdefective colorings. Our algorithm can smoothly scale between these and also simplifies the state of the art $(Δ+1)$-coloring algorithm. At the cost of losing the full algorithm's simplicity we also provide a $O(kΔ)$-coloring algorithm in $O(\sqrt{Δ/k})+\log^* n$ rounds. We also provide improved deterministic algorithms for ruling sets, and, additionally, we provide a tight characterization for one-round color reduction algorithms.
Boosting Light-Weight Depth Estimation Via Knowledge Distillation
Venue: arXiv cs.CV 2023
Year: 2023

Monocular depth estimation (MDE) methods are often either too computationally expensive or not accurate enough due to the trade-off between model complexity and inference performance. In this paper, we propose a lightweight network that can accurately estimate depth maps using minimal computing resources. We achieve this by designing a compact model architecture that maximally reduces model complexity. To improve the performance of our lightweight network, we adopt knowledge distillation (KD) techniques. We consider a large network as an expert teacher that accurately estimates depth maps on the target domain. The student, which is the lightweight network, is then trained to mimic the teacher's predictions. However, this KD process can be challenging and insufficient due to the large model capacity gap between the teacher and the student. To address this, we propose to use auxiliary unlabeled data to guide KD, enabling the student to better learn from the teacher's predictions. This approach helps fill the gap between the teacher and the student, resulting in improved data-driven learning. Our extensive experiments show that our method achieves comparable performance to state-of-the-art methods while using only 1% of their parameters. Furthermore, our method outperforms previous lightweight methods regarding inference accuracy, computational efficiency, and generalizability.
Multilink and AUV-Assisted Energy-Efficient Underwater Emergency Communications
Venue: arXiv cs.NI 2023
Year: 2023

Recent development in wireless communications has provided many reliable solutions to emergency response issues, especially in scenarios with dysfunctional or congested base stations. Prior studies on underwater emergency communications, however, remain under-studied, which poses a need for combining the merits of different underwater communication links (UCLs) and the manipulability of unmanned vehicles. To realize energy-efficient underwater emergency communications, we develop a novel underwater emergency communication network (UECN) assisted by multiple links, including underwater light, acoustic, and radio frequency links, and autonomous underwater vehicles (AUVs) for collecting and transmitting underwater emergency data. First, we determine the optimal emergency response mode for an underwater sensor node (USN) using greedy search and reinforcement learning (RL), so that isolated USNs (I-USNs) can be identified. Second, according to the distribution of I-USNs, we dispatch AUVs to assist I-USNs in data transmission, i.e., jointly optimizing the locations and controls of AUVs to minimize the time for data collection and underwater movement. Finally, an adaptive clustering-based multi-objective evolutionary algorithm is proposed to jointly optimize the number of AUVs and the transmit power of I-USNs, subject to a given set of constraints on transmit power, signal-to-interference-plus-noise ratios (SINRs), outage probabilities, and energy, which achieves the best tradeoff between the maximum emergency response time (ERT) and the total energy consumption (EC). Simulation results indicate that our proposed approach outperforms benchmark schemes in terms of energy efficiency (EE), contributing to underwater emergency communications.
Hybrid Device-to-Device and Device-to-Vehicle Networks for Energy-Efficient Emergency Communications
Venue: arXiv cs.NI 2023
Year: 2023

Recovering postdisaster communications has become a major challenge for search and rescue. Device-to-device (D2D) and device-to-vehicle (D2V) networks have drawn attention. However, due to the limited D2D coverage and onboard energy, establishing a hybrid D2D and D2V network is promising. In this article, we jointly establish, optimize, and fuse D2D and D2V networks to support energy-efficient emergency communications. First, we establish a D2D network by optimally dividing ground devices (GDs) into multiple clusters and identifying temporary data caching centers (TDCCs) from GDs in clusters. Accordingly, emergency data returned from GDs is cached in TDCCs. Second, given the distribution of TDCCs, unmanned aerial vehicles (UAVs) are dispatched to fetch data from TDCCs. Therefore, we establish a UAV-assisted D2V network through path planning and network configuration optimization. Specifically, optimal path planning is implemented using cascaded waypoint and motion planning and optimal network configurations are determined by multiobjective optimization. Consequently, the best tradeoff between emergency response time and energy consumption is achieved, subject to a given set of constraints on signal-to-interference-plus-noise ratios, the number of UAVs, transmit power, and energy. Simulation results show that our proposed approach outperforms benchmark schemes in terms of energy efficiency, contributing to large-scale postdisaster emergency response.