OpenRaiser/Intern-Atlas huggingface dataset:
Module checking of pushdown multi-agent systems
Venue: arXiv cs.LO 2026
Year: 2026

In this paper, we investigate the module-checking problem of pushdown multi-agent systems (PMS) against ATL and ATL* specifications. We establish that for ATL, module checking of PMS is 2EXPTIME-complete, which is the same complexity as pushdown module-checking for CTL. On the other hand, we show that ATL* module-checking of PMS turns out to be 4EXPTIME-complete, hence exponentially harder than both CTL* pushdown module-checking and ATL* model-checking of PMS. Our result for ATL* provides a rare example of a natural decision problem that is elementary yet but with a complexity that is higher than triply exponential-time.
Probabilistic Counters for Privacy Preserving Data Aggregation
Venue: arXiv cs.CR 2026
Year: 2026

Probabilistic counters are well-known tools often used for space-efficient set cardinality estimation. In this paper, we investigate probabilistic counters from the perspective of preserving privacy. We use the standard, rigid differential privacy notion. The intuition is that the probabilistic counters do not reveal too much information about individuals but provide only general information about the population. Therefore, they can be used safely without violating the privacy of individuals. However, it turned out, that providing a precise, formal analysis of the privacy parameters of probabilistic counters is surprisingly difficult and needs advanced techniques and a very careful approach. We demonstrate that probabilistic counters can be used as a privacy protection mechanism without extra randomization. Namely, the inherent randomization from the protocol is sufficient for protecting privacy, even if the probabilistic counter is used multiple times. In particular, we present a specific privacy-preserving data aggregation protocol based on Morris Counter and MaxGeo Counter. Some of the presented results are devoted to counters that have not been investigated so far from the perspective of privacy protection. Another part is an improvement of previous results. We show how our results can be used to perform distributed surveys and compare the properties of counter-based solutions and a standard Laplace method.
Information Theoretic Limits of Cardinality Estimation: Fisher Meets Shannon
Venue: arXiv cs.DS 2026
Year: 2026

Estimating the cardinality (number of distinct elements) of a large multiset is a classic problem in streaming and sketching. In this paper we study the intrinsic tradeoff between the space complexity of the sketch and its estimation error. We define a new measure of efficiency for data sketches called the Fisher-Shannon (FiSh) number $\mathcal{H}/\mathcal{I}$. It captures the tension between the limiting Shannon entropy ($\mathcal{H}$) of the sketch and its normalized Fisher information ($\mathcal{I}$) that characterizes the variance of a statistically efficient, asymptotically unbiased estimator. Our aim in introducing the FiSh-number is to build the mathematical machinery necessary to argue for precise optimality, rather than asymptotic optimality, up to large constant factors. Our results are as follows. [1] We prove that all base-$q$ variants of Flajolet and Martin's PCSA sketch have FiSh-number $H_0/I_0 \approx 1.98016$ and that every base-$q$ variant of HyperLogLog has FiSh-number worse than $H_0/I_0$, but that they tend to $H_0/I_0$ in the limit as $q\rightarrow \infty$. Here $H_0,I_0$ are precisely defined constants. [2] We describe a sketch called Fishmonger that is based on a smoothed, entropy-compressed variant of PCSA with a different estimator function. Fishmonger processes a multiset of $[U]$ such that at all times, w.h.p., its space is $(1+o(1))(H_0/I_0)m \approx 1.98m$ bits and its standard error is $1/\sqrt{m}$. For example, to achieve a 1% standard error, one needs a little more than 19,800 bits, or $\approx 2.42$ kilobytes. [3] Finally, we give circumstantial evidence that $H_0/I_0$ is the optimum FiSh-number of mergeable sketches for Cardinality Estimation. We define a natural subset of mergeable sketches called linearizable sketches and prove that no member of this class can beat $H_0/I_0$. The popular mergeable sketches are, in fact, also linearizable.
Verifying the Hashgraph Consensus Algorithm
Venue: arXiv cs.LO 2026
Year: 2026

The Hashgraph consensus algorithm is an algorithm for asynchronous Byzantine fault tolerance intended for distributed shared ledgers. Its main distinguishing characteristic is it achieves consensus without exchanging any extra messages; each participant's votes can be determined from public information, so votes need not be transmitted. In this paper, we discuss our experience formalizing the Hashgraph algorithm and its correctness proof using the Rocq proof assistant. The paper is self-contained; it includes a complete discussion of the algorithm and its correctness argument in English.
On the logical structure of choice and bar induction principles
Venue: arXiv cs.LO 2026
Year: 2026

We develop an approach to choice principles and their contrapositive bar-induction principles as extensionality schemes connecting an ''intensional'' or ''effective'' view of respectively ill-and well-foundedness properties to an ''extensional'' or ''ideal'' view of these properties. After classifying and analysing the relations between different intensional definitions of ill-foundedness and well-foundedness, we introduce, for a domain $A$, a codomain $B$ and a ''filter'' $T$ on finite approximations of functions from $A$ to $B$, a generalised form GDC$_{A,B,T}$ of the axiom of dependent choice and dually a generalised bar induction principle GBI$_{A,B,T}$ such that: - GDC$_{A,B,T}$ intuitionistically captures the strength of $\bullet$ the general axiom of choice expressed as $\forall a\existsβR(a, b) \Rightarrow\existsα\forall a R(α,(a α(a)))$ when $T$ is a filter that derives point-wise from a relation $R$ on $A x B$ without introducing further constraints, $\bullet$ the Boolean Prime Filter Theorem / Ultrafilter Theorem if $B$ is the two-element set $\mathbb{B}$ (for a constructive definition of prime filter), $\bullet$ the axiom of dependent choice if $A = \mathbb{N}$, $\bullet$ Weak K{ö}nig's Lemma if $A = \mathbb{N}$ and $B = \mathbb{B}$ (up to weak classical reasoning) - GBI$_{A,B,T}$ intuitionistically captures the strength of $\bullet$ G{ö}del's completeness theorem in the form validity implies provability for entailment relations if $B = \mathbb{B}$, $\bullet$ bar induction when $A = \mathbb{N}$, $\bullet$ the Weak Fan Theorem when $A = \mathbb{N}$ and $B = \mathbb{B}$. Contrastingly, even though GDC$_{A,B,T}$ and GBI$_{A,B,T}$ smoothly capture several variants of choice and bar induction, some instances are inconsistent, e.g. when $A$ is $\mathbb{B}^\mathbb{N}$ and $B$ is $\mathbb{N}$.
Transitions in Dynamic Point Labeling
Venue: arXiv cs.CG 2026
Year: 2026

The labeling of point features on a map is a well-studied topic. In a static setting, the goal is to find a non-overlapping label placement for (a subset of) point features. In a dynamic setting, the set of point features and their corresponding labels change, and the labeling has to adapt to such changes. To aid the user in tracking these changes, we can use morphs, here called transitions, to indicate how a labeling changes. Such transitions have not gained much attention yet, and we investigate different types of transitions for labelings of points, most notably consecutive transitions and simultaneous transitions. We give (tight) upper bounds on the number of overlaps that can occur during these transitions. When each label has a non-negative weight associated to it, and each overlap imposes a penalty proportional to the weight of the overlapping labels, we show that it is NP-complete to decide whether the penalty during a simultaneous transition has weight at most $k$. Finally, we consider geotagged data on a map, by labeling points with rectangular or square labels. We developed a prototype implementation to evaluate different transition styles in practice, measuring both number of overlaps and transition duration.
How Interest-Driven Content Creation Shapes Opportunities for Informal Learning in Scratch: A Case Study on Novices' Use of Data Structures
Venue: arXiv cs.HC 2026
Year: 2026

Through a mixed-method analysis of data from Scratch, we examine how novices learn to program with simple data structures by using community-produced learning resources. First, we present a qualitative study that describes how community-produced learning resources create archetypes that shape exploration and may disadvantage some with less common interests. In a second quantitative study, we find broad support for this dynamic in several hypothesis tests. Our findings identify a social feedback loop that we argue could limit sources of inspiration, pose barriers to broadening participation, and confine learners' understanding of general concepts. We conclude by suggesting several approaches that may mitigate these dynamics.
Finite-Time Accuracy of Temporal-Difference Learning Under Schur-Stable Recursions
Venue: arXiv cs.LG 2026
Year: 2026

Temporal difference (TD) learning is a cornerstone reinforcement learning (RL) method for policy evaluation, where the goal is to estimate the value function of a Markov decision process under a fixed policy. While a substantial body of work has established its convergence and stability properties, more recent efforts have focused on its statistical efficiency through finite-time error bounds. In this paper, we advance this line of research by developing a new finite-time error analysis for tabular TD learning that directly exploits a discrete-time stochastic linear system representation and leverages Schur stability of the associated matrices. Beyond the specific bounds obtained, the proposed framework provides a reusable template for analyzing TD learning and related RL algorithms, and it offers control-theoretic insights that may guide future developments in finite-sample RL theory.
Generic Dijkstra
Venue: arXiv cs.NI 2026
Year: 2026

The recently-proposed generic Dijkstra algorithm finds shortest paths in networks with continuous and contiguous resources. While the algorithm was proposed in the context of optical networks (and is applicable to other networks with finite and discrete resources), we present the stated problem in a broader algorithmic setting of the greedy approach. The algorithm was published without a proof of correctness, and with a minor shortcoming. We provide that missing proof and offer a correction to the shortcoming. To prove the algorithm correct, we generalize the greedy approach and the Bellman principle of optimality to algebraic structures with a partial ordering. By analyzing the size of the search space in the worst-case, we argue the stated problem is tractable. Thus we definitely answer a long-standing fundamental question of whether we can efficiently find a shortest path in a network with discrete resources subject to the continuity and contiguity constraints: yes, we can.
Bankrupting DoS Attackers
Venue: arXiv cs.CR 2026
Year: 2026

Can we make a denial-of-service attacker pay more than the server and honest clients? Consider a model where a server sees a stream of jobs sent by either honest clients or an adversary. The server sets a price for servicing each job with the aid of an estimator, which provides approximate statistical information about the distribution of previously occurring good jobs. We describe and analyze pricing algorithms for the server under different models of synchrony, with total cost parameterized by the accuracy of the estimator. Given a reasonably accurate estimator, the algorithm's cost provably grows more slowly than the attacker's cost, as the attacker's cost grows large. Additionally, we prove a lower bound, showing that our pricing algorithm yields asymptotically tight results when the estimator is accurate within constant factors.
Budget Pacing in Repeated Auctions: Regret and Efficiency without Convergence
Venue: arXiv cs.GT 2026
Year: 2026

We study the aggregate welfare and individual regret guarantees of dynamic \emph{pacing algorithms} in the context of repeated auctions with budgets. Such algorithms are commonly used as bidding agents in Internet advertising platforms, adaptively learning to shade bids by a tunable linear multiplier in order to match a specified budget. We show that when agents simultaneously apply a natural form of gradient-based pacing, the liquid welfare obtained over the course of the learning dynamics is at least half the optimal expected liquid welfare obtainable by any allocation rule. Crucially, this result holds \emph{without requiring convergence of the dynamics}, allowing us to circumvent known complexity-theoretic obstacles of finding equilibria. This result is also robust to the correlation structure between agent valuations and holds for any \emph{core auction}, a broad class of auctions that includes first-price, second-price, and generalized second-price auctions as special cases. For individual guarantees, we further show such pacing algorithms enjoy \emph{dynamic regret} bounds for individual utility- and value-maximization, with respect to the sequence of budget-pacing bids, for any auction satisfying a monotone bang-for-buck property. To complement our theoretical findings, we provide semi-synthetic numerical simulations based on auction data from the Bing Advertising platform.
The Mutual Visibility Problem for Fat Robots with Lights
Venue: arXiv cs.CG 2026
Year: 2026

Given a set of $n\geq 1$ unit disk robots in the Euclidean plane, we consider the fundamental problem of providing mutual visibility to them: the robots must reposition themselves to reach a configuration where they all see each other. This problem arises under obstructed visibility, where a robot cannot see another robot if there is a third robot on the straight line segment between them. This problem was solved by Sharma et al. [ICDCN, 2018] in the luminous robots model, where each robot is equipped with an externally visible light that can assume colors from a fixed set of colors, using 9 colors and $O(n)$ rounds. In this work, we present an algorithm that requires only 2 colors and $O(n)$ rounds. The number of colors is optimal since at least two colors are required even for point robots [Di Luna et al., Information and Computation, 2017].
Semantic Image Synthesis via Diffusion Models
Venue: arXiv cs.CV 2026
Year: 2026

Denoising Diffusion Probabilistic Models (DDPMs) have achieved remarkable success in various image generation tasks compared with Generative Adversarial Nets (GANs). Recent work on semantic image synthesis mainly follows the de facto GAN-based approaches, which may lead to unsatisfactory quality or diversity of generated images. In this paper, we propose a novel framework based on DDPM for semantic image synthesis. Unlike previous conditional diffusion model directly feeds the semantic layout and noisy image as input to a U-Net structure, which may not fully leverage the information in the input semantic mask, our framework processes semantic layout and noisy image differently. It feeds noisy image to the encoder of the U-Net structure while the semantic layout to the decoder by multi-layer spatially-adaptive normalization operators. To further improve the generation quality and semantic interpretability in semantic image synthesis, we introduce the classifier-free guidance sampling strategy, which acknowledge the scores of an unconditional model for sampling process. Extensive experiments on four benchmark datasets demonstrate the effectiveness of our proposed method, achieving state-of-the-art performance in terms of fidelity (FID) and diversity (LPIPS). Our code and pretrained models are available at https://github.com/WeilunWang/semantic-diffusion-model.
Robotic Depowdering for Additive Manufacturing Via Pose Tracking
Venue: arXiv cs.RO 2026
Year: 2026

With the rapid development of powder-based additive manufacturing, depowdering, a process of removing unfused powder that covers 3D-printed parts, has become a major bottleneck to further improve its productiveness. Traditional manual depowdering is extremely time-consuming and costly, and some prior automated systems either require pre-depowdering or lack adaptability to different 3D-printed parts. To solve these problems, we introduce a robotic system that automatically removes unfused powder from the surface of 3D-printed parts. The key component is a visual perception system, which consists of a pose-tracking module that tracks the 6D pose of powder-occluded parts in real-time, and a progress estimation module that estimates the depowdering completion percentage. The tracking module can be run efficiently on a laptop CPU at up to 60 FPS. Experiments show that our depowdering system can remove unfused powder from the surface of various 3D-printed parts without causing any damage. To the best of our knowledge, this is one of the first vision-based robotic depowdering systems that adapt to parts with various shapes without the need for pre-depowdering.
On the Representation of Pairwise Causal Background Knowledge and Its Applications in Causal Inference
Venue: arXiv cs.AI 2026
Year: 2026

Pairwise causal background knowledge about the existence or absence of causal edges and paths is frequently encountered in observational studies. Such constraints allow the shared directed and undirected edges in the constrained subclass of Markov equivalent DAGs to be represented as a causal maximally partially directed acyclic graph (MPDAG). In this paper, we first provide a sound and complete graphical characterization of causal MPDAGs and introduce a minimal representation of a causal MPDAG. Then, we give a unified representation for three types of pairwise causal background knowledge, including direct, ancestral and non-ancestral causal knowledge, by introducing a novel concept called direct causal clause (DCC). Using DCCs, we study the consistency and equivalence of pairwise causal background knowledge and show that any pairwise causal background knowledge set can be uniquely and equivalently decomposed into the causal MPDAG representing the refined Markov equivalence class and a minimal residual set of DCCs. Polynomial-time algorithms are also provided for checking consistency and equivalence, as well as for finding the decomposed MPDAG and the residual DCCs. Finally, with pairwise causal background knowledge, we prove a sufficient and necessary condition to identify causal effects and surprisingly find that the identifiability of causal effects only depends on the decomposed MPDAG. We also develop a local IDA-type algorithm to estimate the possible values of an unidentifiable effect. Simulations suggest that pairwise causal background knowledge can significantly improve the identifiability of causal effects.
Optimal Computation in Anonymous Dynamic Networks
Venue: arXiv cs.DC 2026
Year: 2026

We give a simple characterization of the functions that can be computed deterministically by anonymous processes in dynamic networks, depending on the number of leaders in the network. In addition, we provide efficient distributed algorithms for computing all such functions assuming minimal or no knowledge about the network. Each of our algorithms comes in two versions: one that terminates with the correct output and a faster one that stabilizes on the correct output without explicit termination. Notably, these are the first deterministic algorithms whose running times scale linearly with both the number of processes and a parameter of the network which we call "dynamic disconnectivity" (meaning that our dynamic networks do not necessarily have to be connected at all times). We also provide matching lower bounds, showing that all our algorithms are asymptotically optimal for any fixed number of leaders. While most of the existing literature on anonymous dynamic networks relies on classic mass-distribution techniques, our work makes use of a novel combinatorial structure called "history tree", which is of independent interest. Among other contributions, our results make conclusive progress on two popular fundamental problems for anonymous dynamic networks: leaderless Average Consensus (i.e., computing the mean value of input numbers distributed among the processes) and multi-leader Counting (i.e., determining the exact number of processes in the network). Our contribution not only opens a promising line of research on applications of history trees, but also demonstrates that computation in anonymous dynamic networks is practically feasible and far less demanding than previously conjectured.
Functional Rule Extraction Method for Artificial Neural Networks
Venue: arXiv cs.LG 2026
Year: 2026

The idea I propose in this paper is a method that is based on comprehensive functions for directed and undirected rule extraction from artificial neural network operations. Firstly, I defined comprehensive functions, then constructed a comprehensive multilayer network (denoted as N). Each activation function of N is parametrized to a comprehensive function.
On Probabilistic $ω$-Pushdown Systems, and $ω$-Probabilistic Computational Tree Logic
Venue: arXiv cs.LO 2026
Year: 2026

In this paper, we define the notion of {\em probabilistic $ω$-pushdown automaton} and study its model-checking problem against the logic of $ω$-probabilistic computational tree logic ($ω$-PCTL) and its bounded version from a computational complexity view. Specifically, we obtain the following equally important new results: We define {\em probabilistic $ω$-pushdown automaton} for the first time and study the model-checking question of {\em stateless probabilistic $ω$-pushdown system ($ω$-pBPA)} against $ω$-PCTL (defined by Chatterjee, Sen, and Henzinger in \cite{CSH08}), showing that model-checking of {\em stateless probabilistic $ω$-pushdown systems ($ω$-pBPA)} against $ω$-PCTL is generally undecidable. Our approach is to construct $ω$-PCTL formulas encoding the {\em Post Correspondence Problem}. We then study in which case there exists an algorithm for model-checking {\it stateless probabilistic $ω$-pushdown systems} and show that the problem of model-checking {\it stateless probabilistic $ω$-pushdown systems} against $ω$-{\it bounded probabilistic computational tree logic} ($ω$-bPCTL) is decidable, and further show that this problem is $\mathit{NP}$-hard.
OA-Bug: An Olfactory-Auditory Augmented Bug Algorithm for Swarm Robots in a Denied Environment
Venue: arXiv cs.RO 2026
Year: 2026

Searching in a denied environment is challenging for swarm robots as no assistance from GNSS, mapping, data sharing, and central processing is allowed. However, using olfactory and auditory signals to cooperate like animals could be an important way to improve the collaboration of swarm robots. In this paper, an Olfactory-Auditory augmented Bug algorithm (OA-Bug) is proposed for a swarm of autonomous robots to explore a denied environment. A simulation environment is built to measure the performance of OA-Bug. The coverage of the search task can reach 96.93% using OA-Bug, which is significantly improved compared with a similar algorithm, SGBA. Furthermore, experiments are conducted on real swarm robots to prove the validity of OA-Bug. Results show that OA-Bug can improve the performance of swarm robots in a denied environment. Video: https://youtu.be/vj9cRiSm9eM.