arXane › Computer Science › Computer Science
Wednesday, 4 November 2026: 4 new papers, 5 cross-lists and 21 replacements in Logic in Computer Science (cs.LO), in arXiv's order, with full abstracts. The same papers as arXiv's own listing, set as a newspaper; every title links to arXiv.
This volume contains the proceedings of the 23rd International Conference on Quantum Physics and Logic (QPL 2026), which was held from August 17 to August 21 2026, in Amsterdam, The Netherlands, organized by the University of Amsterdam. QPL is an annual conference that brings together academic and industry researchers working on topics ranging from basic research in the foundations of physics to applications in quantum computing and communication, both for near-term quantum hardware and future large-scale, fault-tolerant devices. The conference places particular emphasis on the application of formal algebraic, logical, compositional, and categorical structures to quantum theory and related areas. Work applying quantum-inspired techniques and structures to other fields such as (classical) computation, linguistics, artificial intelligence, and causality is also welcome.
Markov decision process over vector addition system with states (VASS MDP) is a finite state model combining non-deterministic and probabilistic behavior, augmented with non-negative integer counters that can be incremented or decremented during each state transition. VASS MDPs can serve as abstractions of probabilistic programs, offering many decidable properties. In this paper, we develop techniques for analyzing the polynomiality of asymptotic estimates for VASS MDPs. That is, for every initial configuration of size \(n\), we consider the number of transitions needed to reach a configuration with some counter negative. We show that for any VASS MDP, either for all \(\epsilon>0 \) and all sufficiently large \(n\) the number of transitions is at least \(2^{n^{\frac{1}{2}-\epsilon}} \) with probability at least \(1-\epsilon \), or for any superpolynomial function \(f \), all \(\epsilon>0 \) and all sufficiently large \(n\) the number of transitions is upper bounded by \(f(n) \) with probability at least \(1-\epsilon \). Furthermore, if the VASS MDP is DAG-like then we can replace \(f(n)\) with \(n^{k+\epsilon} \), where \(k=2\cdot 3^{w\cdot d+|T|} \) and \(w,d\) and \(T \) are the number of MECs, counters and transitions of the VASS MDP, respectively. It is decidable in polynomial time which case holds.
Vision-Language-Action (VLA) models generalize across tasks, but their autoregressive decoders need sequential forward passes in proportion to the action horizon, each bounded below on embedded aerial platforms by streaming billions of parameters from memory. We present Aero-VPA, a lightweight Vision-Predictor-Action architecture for 3D navigation on edge hardware. A compact RGB-D Vision Transformer and a five-head ensemble predictor, trained without pixel reconstruction, forecast the next latent state; a Conditional Flow Matching solver generates a velocity and yaw-rate chunk in two Euler steps, so each decision takes five sequential network evaluations; and the ensemble dispersion drives an uncertainty fallback. Version 1 specified the architecture, deployment and protocol without results. This version reports the first closed-loop evaluation: PX4 software-in-the-loop simulation of quadrotor missions in procedurally generated forests. Behaviour cloning failed on all 60 missions despite open-loop errors of 0.02-0.04 m/s: the policy copies its last command, a copycat form of causal confusion. DAgger with a privileged, safety-gated supervisor gave the first successes but plateaued at 11.1-21.1% across six checkpoints. A map-free runtime shield with a 15 s depth memory, barrier constraints, a cap on motion outside the 73-degree field of view and backoff along the flown path raised the first DAgger policy's success on 180 paired missions from 21.1% to 52.2% (95% CI [45.0, 59.4]; exact McNemar p = 1.2 x 10^-10) and cut its crashes from 72.2% to 22.2%, while timeouts rose from 2.8% to 23.3%. All six checkpoints gained 30.0-34.4 percentage points, at mean speeds of 1.16-1.36 m/s. The code (https://github.com/ylee-sling/Aero-VPA), the trained policy (72.6 MB, https://huggingface.co/ylee-sling/aero-vpa) and the full benchmark dataset are public.
We formulate the global trace condition, GTC, for cyclic proofs as a particular case of the size-change termination condition, or SCT. We express cyclic proofs through a variant of size-change graphs, called transition graphs, whose edges are labelled by (finite) bipartite relations. We show that injective transition graphs suffice to encode cyclic pre-proofs for a variant of Brotherston and Simpson's sequent calculus with inductive definitions. The injectivity of transition graphs corresponds to restricting SCT to fan-in-free graphs. Then we prove that an essentially weaker condition implies SCT in this case, and hence GTC.
This paper considers online intrusion-risk assessment and graded warning for unmanned aerial vehicles under bounded measurement attacks. To address this problem, we develop a monitoring framework that combines trusted state estimation, attack-aware risk assessment, and probabilistic signal temporal logic (PrSTL). Trusted observations support recursive state estimation, while potentially attacked observations inform integrity testing and intrusion-risk assessment. The key contribution is a confidence-set construction that combines normalized innovation statistics with physical attack bounds to characterize admissible measurement biases. The resulting family of bias-corrected Gaussian posteriors yields an upper bound on the probability of occupying a no-fly zone or its surrounding safety margin. Confidence guarantees and finite-cover numerical certificates quantify the reliability of this risk envelope, which is evaluated with or without an integrity alarm. The PrSTL monitor analyzes the resulting risk sequence to distinguish ordered, persistent, and repeated risk and produces graded warnings with explicit robustness margins and supporting windows. We validate the monitor in flight experiments with a Crazyflie quadrotor tracked by a Vicon motion capture system. Controlled comparisons quantify the contributions of individual monitoring components. Prescribed risk profiles verify the temporal semantics and illustrate how distinct risk patterns produce different warning levels.
In this paper, we develop a semantic model for the parallel execution of quantum circuits, providing a formal foundation for studying shared-qubit concurrency in quantum computing. As in classical shared-memory concurrency, parallel quantum circuits may interfere with one another through operations on shared qubits. However, quantum entanglement and the noncommutativity of quantum operations introduce additional challenges for reasoning about their correctness. To address these challenges, we generalise the classical Owicki-Gries method to quantum computing at the level of quantum circuits. Our approach enables compositional reasoning about parallel quantum circuits by separating the verification of individual components from the analysis of interference between them. We formulate proof rules for establishing the correctness of parallel quantum circuits and prove their soundness with respect to the proposed semantic model.
A closed path can return to its starting point while analytic continuation reaches another branch. We construct a finite computational calculus in which retained logarithmic branches supply memory, analytic observations select operations, and descent through a covering exposes deeper memory. Three branch coordinates suffice, and every finite observation uses the same cubic power covering. Each program defines a globally real analytic return map whose integer-lattice execution is realized by actual path lifting. Our first theorem simulates every finite-alphabet, finite-control Post--Turing machine, preserving complete configurations, halting, and divergence. Our second theorem identifies the partial numeric functions of the calculus, under fixed primitive-recursive input and output maps, with exactly the partial recursive functions. Deleting descent leaves a Forward language with a syntax-derived finite observation quotient and a primitive-recursive halting predicate. This yields a strict separation within the calculus and identifies access to deeper memory as its decisive additional operation. The constructions and semantic correspondences are formalized in Lean 4 with Mathlib.
Language models are accurate on most long-arithmetic problems, but their accuracy is estimated on samples and carries no guarantee for an unseen input; tool use is exact but moves the computation outside the network. We show that exactness at all input lengths becomes a finite, checkable property of a network when each of its steps reads only a bounded view of an external working memory. In Sketchpad, Qwen3.5-0.8B with a low-rank adapter executes arithmetic procedures on a rendered sheet. Each forward pass reads a three-cell view and emits one step: a digit, a carry or borrow, and the next operation. A fixed runtime moves the view and writes no digit of a result. We prove in Lean that the model is then exact on all inputs of any length if and only if it is exact on the finite set of views the runtime presents, that no finite test suffices when steps also read earlier steps, and that the guarantee tolerates bounded numerical perturbation and extends to compositions of procedures. All 2,446 views pass on the deployment device, a laptop GPU running the model in a web browser. The certified model performs signed addition and subtraction, long multiplication and division, square roots and greatest common divisors at arbitrary length. It solved 200 of 200 pre-registered problems in the browser, and 220 of 220 sums of up to 1,000 digits and products of up to 20 digits, of which GPT-6.1 Sol, the strongest of ten other models, solved 217. A symbolic runtime built on these procedures solves, expands and factors polynomials with every number computed by the model, and a multiplicative gate on the adapter recovers the base model exactly when the sheet is not in use.
Reactive synthesis is the problem of generating a program that produces outputs satisfying a logical specification for every input stream. We study distributed synthesis for two processes communicating in rounds over unreliable links, with at least one message delivered in every round. Despite this delivery guarantee, we show that synthesis from linear temporal logic specifications is undecidable, even when messages carry the processes' complete causal histories. More generally, we give a complete characterization of the communication restrictions that make synthesis decidable. Restrictions are described by a message adversary $A$, a set of allowed infinite graph histories: sequences of communication graphs, each specifying which messages are delivered in a round. Iterated chromatic subdivision associates these histories with points in the unit interval, yielding an image $\pi(A) \subseteq [0,1]$. For every $\omega$-regular message adversary $A$, synthesis is decidable if and only if $\pi(A)$ is nowhere dense. In the decidable cases, our procedure takes a deterministic parity automaton for $A$ and a specification, decides realizability, and constructs a realizing distributed algorithm whenever one exists. Further, our topological arguments shed new light on the fundamental requirements of synthesis. They show that, for $\omega$-regular message adversaries, synthesis is decidable if and only if consensus is repeatedly solvable in bounded time. This links two previously unrelated problems from formal verification and distributed computing through the processes' uncertainty about communication.