https://arxiv.org/api/6luUnoCshEN1jhgmQTSLvVwX/qo 2026-11-12T03:27:36Z 20626 0 15 http://arxiv.org/abs/2611.14408v1 2026-11-10T17:51:39Z

We introduce intuitionistic public announcement logics Lmin and Lequ determined by classes of birelational frames where the intuitionistic preorder and the modal accessibility relation do not need to satisfy the confluence conditions traditionally considered within the framework of IPAL. Our logics can be seen as generalisations of IPAL seeing that their language is based on a binary epistemic modality of "relativised knowledge" that allows us to define valid reduction axioms. Our main results are the soundness and completeness of Lmin with respect to the class of all birelational frames and the soundness and completeness of Lequ with respect to the class of all birelational frames where the modal accessibility relation is an equivalence relation.

2026-11-10T17:51:39Z Philippe Balbiani Hans van Ditmarsch Cigdem Gencer Clara Lerouvillois http://arxiv.org/abs/2611.14094v1 2026-11-10T13:53:07Z

Semantic communication, near-field operation, and integrated sensing and communication (ISAC) are often considered separately in terrestrial and non-terrestrial networks (TN--NTN). We show how a large electromagnetic aperture can connect them. \textcolor{black}{Nonlocal metasurfaces and holographic apertures act on the spatial spectrum of an incident field and can execute linear projections, which form an early stage of semantic feature extraction, directly in the wave domain before digitisation, thereby reducing the corresponding digital processing burden.} Near-field focusing also provides position-dependent sensing features, allowing the aperture to serve as an analog semantic-ISAC front end on resource-constrained aerial and satellite platforms. We describe the underlying physics, the co-design of constrained analog projections with lightweight digital decoders, and a case study in which a data-adaptive projection outperforms a fully digital baseline in the simulated energy-limited regime while transmitting four times fewer coefficients and using 11.4 times fewer decoder MACs. Finally, we identify relevant 3GPP, ITU-R, and ETSI activities and the remaining standardisation gaps.

2026-11-10T13:53:07Z 8 pages, 3 figures, accepted for publication in IEEE Communications Standards Magazine Shadi Danesh Pooria Salami Hesaam Zaravashan Abdulkadir Köse Ayhan Akbas Chuan Heng Foh Mohsen Khalily http://arxiv.org/abs/2405.20057v2 2026-11-10T12:23:05Z

First-order linear temporal logic (FO-LTL) is a flexible and expressive formalism capable of naturally describing complex behaviors and properties. Although the logic is in general highly undecidable, the idea of using it as a specification language for the verification of complex infinite-state systems is appealing. However, a missing piece, which has proved to be an invaluable tool in dealing with other temporal logics, is an automaton model capable of capturing the logic. In this paper we address this issue, by defining and studying such a model, which we call first-order automaton. We define this very general class of automata, and the corresponding notion of regular first-order language (of finite words), showing their closure under most language-theoretic operations. We show how they can capture any FO-LTL formula over finite words, over any signature and theory, and provide sufficient conditions for the semi-decidability of their non-emptiness problem. Then, to show the usefulness of the formalism, we prove the decidability of monodic FO-LTL, a classic result known in the literature, with a simpler and direct proof.

2024-05-30T13:45:23Z Luca Geatti, Alessandro Gianola, Nicola Gigante. First-Order Automata. Proceedings of AAAI 2025: 14940-14948 Luca Geatti Alessandro Gianola Nicola Gigante 10.1609/AAAI.V39I14.33638 http://arxiv.org/abs/2609.10114v2 2026-11-10T11:44:52Z

We study the policy change problem that arises in the runtime verification of long-running systems. The online monitors typically used in this context are generally treelike, in that they maintain substates that monitor subformulae of the target policy. We consider when and how the policy can be changed while the monitored system is running by only exploiting the information stored in the monitor's state. This is relevant, for example, to account for new system functionality or changes in regulatory requirements. We formally define the policy change problem in a general setting, independent of any specific (treelike) monitor implementation. We then show that policy change for past-time metric temporal logic (pMTL) is decidable but has tight non-primitive recursive lower and upper bounds, while with discrete-time semantics it is EXPSPACE-complete.

2026-09-09T12:47:28Z 39 pages, 5 figures François Hublet Dhruv Nevatia Joshua Schneider http://arxiv.org/abs/2601.19426v3 2026-11-10T10:06:05Z

Generalised algebraic theories (GATs) allow multiple sorts indexed over each other. Categories have two sorts, objects and morphisms, and the latter are double-indexed over the former. Martin-Löf type theory has four sorts: contexts, substitutions, types and terms. For example, types are indexed over contexts, and terms are indexed over both contexts and types. In this paper we show that any GAT can be reduced to a GAT involving only two sorts: a first one without dependencies, and another one indexed over the former. We show that a model of the reduced GAT is equivalently given by a pair consisting of a model of the original GAT, which we call the core model, and a "cartesian" morphism from the family of sets induced by this core model. In a type-theoretic metatheory, the initial model of a GAT is called a quotient inductive-inductive type (QIIT). The above characterisation justifies soundness of the reduction, in the sense that the QIIT of the original GAT can be simulated from the QIIT of the reduced GAT, by taking its core model. A particular case of our reduction is the well-known method of reducing mutual inductive types to a single indexed family. Other instances of this reduction can be found in the literature to simulate sophisticated QIITs in Cubical Agda. Indeed, the reduced GAT is simpler than the original GAT in the following aspects: it does not have sort equalities; it does not have interleaved sorts and operations; if the original GAT did not have interleaved sorts and operations, then the reduced GAT won't have operations interleaved between different sorts. Our approach is semantic in that it does not rely on a syntactic description of GATs, but instead, on Uemura's bi-initial characterisation of the category of (finite) GATs in the 2-category of finitely complete categories with a chosen exponentiable morphism.

2026-01-27T10:05:11Z Samy Avrillon Ambrus Kaposi Ambroise Lafont Niyousha Najmaei Johann Rosain http://arxiv.org/abs/2609.03472v2 2026-11-10T08:44:11Z

We study the override and update operators on partial functions from the perspective of restriction categories. We propose a definition of override restriction categories, in which both of the operators in question exist. We prove a number of results concerning these operators and their relationship to the structure of the ambient restriction category, as well as relating them to the existing literature on the override and update operators. We provide various examples of override restriction categories and in particular show that every classical restriction category is an override restriction category.

2026-09-03T07:29:09Z To appear in the proceedings of CSL 2027 (LIPIcs, Volume 403) Jean-Simon Pacaud Lemay Chad Nester http://arxiv.org/abs/2611.13697v1 2026-11-10T07:43:34Z

Reflective Grounded Arithmetic (RGA) is a paracomplete arithmetic in which every term is a program and truth is grounded evaluation. RGA discharges a hypothesis only when it proves the hypothesis decided. This paper shows, in a machine-checked Isabelle/HOL development, how Gödel's incompleteness theorems hold for RGA and for systems built on it. RGA's implication is material and RGA has the disjunction property, so the implications the textbook proof of the second theorem uses fail while its entailments and rules hold: Gödel's proof survives as entailments. RGA does not prove its consistency sentence Con, and RGA derives its own second theorem as the entailment $\mathit{Con}\vdash\neg\mathit{Pr}(\ulcorner\mathit{Con}\urcorner)$ and as one sentence quantified over proofs. The second theorem is then proved once, for every Gödel extension of RGA: an entailment relation on RGA's language, closed under RGA's rules, with a checker that meets three structural conditions, NEC, D3 and EXPL as proof transformers, D1 as closed acceptance, and consistency. D2 is not among the conditions. RGA with its checker is one instance. Inductive Grounded Arithmetic (IGA), RGA with ground induction, is another, its checker adding one rule detector, and IGA does not derive its consistency sentence for it. Adoption, a reflection rule whose premise is a derived warrant that the checker accepts computed proofs of every instance of a universal, gives consistent extensions RGA$^+$ and IGA$^+$. RGA$^+$ derives RGA's consistency sentence and IGA$^+$ derives RGA's and IGA's, so each strictly extends its base, and IGA$^+$ both. The second theorem holds at every adopted notation claim, and adopting Turing's code for that claim's checker derives its consistency sentence, so no claim certifies itself. Whether IGA alone derives RGA's consistency sentence is open, and the paper names what two routes to an answer need.

2026-11-10T07:43:34Z 103 pages; splits the Goedel incompleteness material out of Internal Reasoning companion paper 2608.16140, which is getting a corresponding major update Bryan Ford http://arxiv.org/abs/2611.13471v1 2026-11-10T02:31:13Z

Most type systems are designed to verify safety properties: the judgement $e : τ$ holds if $e$ may evaluate to any value contained in the denotation of $τ$, but nothing more. More recent type systems have considered the complementary class of reachability properties: in these systems, the typing judgment holds if $e$ must be able to evaluate to every value denoted by $τ$, and possibly more. This paper introduces a refinement type system for higher-order functional programs where types can capture both safety and reachability properties. Simultaneously supporting both is challenging because each imposes different constraints on how variable bindings in a typing context are interpreted. We address this challenge by treating typing contexts as a kind of resource that mediates which capabilities are available when typing a program. We formalize this notion by developing a resource algebra of contextual capabilities and a bunched modal context logic over this algebra. We then interpret our type system in this logic, establishing soundness with respect to a denotational semantics that unifies safety and reachability guarantees within a single typing judgement.

2026-11-10T02:31:13Z Zhe Zhou Benjamin Delaware Suresh Jagannathan http://arxiv.org/abs/2611.08685v2 2026-11-10T01:23:23Z

This paper introduces a categorical framework for models of higher-order separation logic including the weakest precondition modality. Weakest preconditions are interpreted by strong monads on a category fibered over a model of Moggi's computational lambda calculus. The fibered categories in question are termed bunched fibrations and shown to be equivalent to BI hyperdoctrines. Well-known heuristic techniques for obtaining weakest preconditions are shown to be expressible in categorical terms and are proved sound. The ``baking in the frame rule'' trick is shown to satisfy a universal property. Constructions are given for extending a program logic with cost credits. Our largest case study is parametrized by a category having local independent product (LIP) structure, a notion due to Simpson that axiomatizes name generation, randomness, and local state. From an LIP category, we construct an allocation monad, a bunched fibration, and a monad lifting. We instantiate our construction to obtain a novel probabilistic separation logic for measure-theoretic probability that both simplifies and clarifies prior work.

2026-11-05T20:43:57Z 41 pages, 5 figures John M. Li Ryan Doenges Pedro H. Azevedo de Amorim http://arxiv.org/abs/2610.37534v2 2026-11-09T20:29:17Z

Assume-guarantee contracts provide a set of algebraic operations that enable the efficient compositional design and analysis of complex engineering systems. The explicit computation of these operations at component interfaces is currently supported only for some logics lacking a notion of time. This paper develops theory and algorithms to compute these operations when the contracts are expressed in the GR(1) modulo theory. The key challenge is the computation of two quantifier elimination problems for temporal formulas. We develop context-aided variable elimination procedures on GR(1)-modulo formulas, establish their soundness, characterize subproblem-wise optimal solutions within an admissible class of formulas, and use the procedures to compute contract operations, including composition and quotient. We implement the resulting framework in Pacti, automating compositional reasoning over GR(1) contracts. Finally, we demonstrate the framework on an automated emergency-braking case study, where we compute system-level contracts and expose compatibility conditions arising from the interaction of component specifications. Experiments on synthetic families show that the cost is governed by the number of eliminated variables and liveness conjuncts, and a comparison with exact automata-based elimination shows complementary scaling.

2026-10-27T16:53:25Z 55 pages, 10 figures Yigit Narter Emily Zhao Inigo Incer http://arxiv.org/abs/2611.12761v1 2026-11-09T17:38:04Z

Programming language researchers have developed a wide array of tools to reason about probabilistic programs, but it remains unclear how to apply these proof techniques to continuous-time stochastic processes. To bridge this gap, we propose a verification method for properties of continuous-time stochastic processes by reasoning about them as standard programs. To demonstrate our approach, we define a continuous semantics for a probabilistic imperative language $\mathrm{pWhile}^{\mathrm{dt}}$ by taking the Kuratowski limit of the standard semantics, which collects limit points of the standard program semantics as the time-step approaches zero. Then, we present a Hoare-style logic that uses loop invariants and decreasing functions to verify properties of continuous programs. To establish soundness, we identify a broad class of assertions that are preserved from the standard semantics to the continuous semantics. To demonstrate our approach, we verify properties of ten continuous-time stochastic processes modeled in $\mathrm{pWhile}^{\mathrm{dt}}$, including variants of Brownian motion and a stochastic hybrid system.

2026-11-09T17:38:04Z Kei Imada Justin Hsu http://arxiv.org/abs/2501.18404v5 2026-11-09T17:12:24Z

We introduce string diagrams for graded symmetric monoidal categories. Our approach includes a definition of graded monoidal theory and the corresponding freely generated syntactic category. The para construction on monoidal actegories is a motivating example for our framework, and we show how an axiomatic presentation of the resulting category $\mathbf{Para}(\mathbb{G},\mathbf{C})$ may be modularly obtained from presentations for $\mathbb{G}$ and $\mathbf{C}$. We demonstrate three different applications of our diagrammatic language under the same theme: probabilistic reasoning. First, we show how to axiomatise a variant of the graded category $\mathbf{ImP}$, recently introduced by Liell-Cock and Staton to model imprecise probability. This culminates in a representation, as string diagrams with grading wires, of programs with primitives for nondeterministic and probabilistic choices and conditioning. Second, we exploit our modular presentation result to provide a new proof for a presentation of $\mathbf{Gauss}$, the category of Gaussian stochastic maps. Third, we use grading wires to represent causal interventions on Bayesian networks.

2025-01-30T15:00:36Z New Section 3.3 on quotient up to regrading. New Section 7 on presentation of Gaussian maps. Old Section 7 is now Section 8 with added Section 8.5 on identifiability. Implemented many suggestions from reviewers Ralph Sarkis Fabio Zanasi http://arxiv.org/abs/2611.12618v1 2026-11-09T16:01:49Z

We show that type-logical grammars with the standard rules for product, associativity, extraction and infixation have an NP-complete fixed recognition problem, adapting a construction for first-order linear logic from Pshenitsyn (2025), who already showed that grammars in first-order linear logic are closed under intersection and therefore not semilinear and not mildly context-sensitive. We strengthen these results and shown that grammars in first-order linear logic can simulate the quasi-linear grammars of Book \& Greibach (1970), the grammars recognised in non-deterministic linear time (NSPACE(n) or. NLIN). I argue that NLIN is an interesting class of formal languages as well, and a useful upper bound on the time complexity of formalisms used for natural language, just like LOGCFL is a useful upper bound on the space complexity. Taken together this means that first-order linear logic can be seen as the logic of non-deterministic linear-time string languages, graph languages and automata.

2026-11-09T16:01:49Z Richard Moot LIRMM,CNRS,LIRMM | PIPL,UM http://arxiv.org/abs/2608.12206v3 2026-11-09T14:48:22Z

The amalgamation decision problem asks whether the finite models of a given universal first-order sentence have the amalgamation property. We prove that this problem is ExpTime-hard for universal Horn sentences of maximum relation arity three, and 2ExpTime-hard when the arity is unbounded, thereby strengthening the previous best lower bounds for universal Horn sentences. The first reduction simulates runs of nondeterministic tree automata using a single ternary relation and unary and binary auxiliary relations. The second simulates finite winning strategies in an exponential corridor game. As a secondary contribution, we prove that deciding the winner remains 2ExpTime-complete for the game normal form used in our reduction, in which each move label determines a unique legal successor from every non-winning legal row.

2026-08-12T16:01:25Z The upper-bound claims in v2 have been withdrawn due to an error in the proof. This version focuses on the new lower bounds Jakub Rydval http://arxiv.org/abs/2610.19940v2 2026-11-09T14:16:48Z

We construct countable, stable, $ω$-categorical structures with at most two binary relations whose CSPs exhibit three complexity regimes: NP-complete, decidable but not in NP, and undecidable. The templates arise from a controlled Hrushovski construction of stable $ω$-categorical graphs $M_α$ for suitable irrational parameters $α>1$. Some of these graphs have NP-complete CSPs. Expanding the graphs $M_α$ by the non-edge relation turns age membership into a restriction of the CSP. For every time-constructible bound $t$, there is such an expansion whose CSP is decidable but not in DTIME$(t)$. For an explicit parameter $α$, the restriction to complete instances belongs to $\mathrm{coNP}$ and the full CSP belongs to $Σ_2^{\mathrm P}$. Separating the ages of the $M_α$ using graphs with large girth and prescribed density yields $2^{\aleph_0}$ distinct CSPs of these expansions, all but countably many of which are undecidable.

2026-10-14T10:24:20Z 36 pages Manuel Bodirsky David Bradley-Williams Ehud Hrushovski Christoph Spiess