arXiv Science⌕ Search

arXiv · 2610.16473

Some complete $ω$-powers of a one-counter language in the difference hierarchy

Abstract

Fix a finite alphabet $Σ$ having at least two letters, and natural numbers $n,k\geq 1$. We denote by $D_n(\mathbfΠ^0_k)$ the class of differences of $n$ subsets of the Cantor space $Σ^ω$ in $\mathbfΠ^0_k$, and by $\checked{D}_n(\mathbfΠ^0_k)$ the class of complements of sets in $D_n(\mathbfΠ^0_k)$. We prove, for any natural numbers $n,k\geq 1$, the existence of a finite alphabet $Σ$ having at least two letters and a finitary language $U_{n,k}$ over $Σ$ accepted by a one-counter automaton such that the $ω$-power $$U_{n,k}^\infty:=\{ w_0w_1\cdots\inΣ^ω\mid\forall i\inω~~w_i\in U_{n,k}\}$$ is $D_{2n-1}(\mathbfΠ^0_k)$-complete. We also prove a conditional result for the dual classes $\checked{D}\_{2n}(\mathbfΠ^0\_k)$: under the assumption that there exists a finitary language $V_{n,3}$ accepted by a one-counter automaton, such that its $ω$-power $V_{n,3}^\infty$ is $\checked{D}_{2n}(\mathbfΠ^0_3)$-complete, there would also exist, for any integer $k>3$, a finitary language $V_{n,k}$ accepted by a one-counter automaton, such that its $ω$-power $V_{n,k}^\infty$ is $\checked{D}_{2n}(\mathbfΠ^0_k)$-complete. Finally we add another conditionnal result about Wadge degrees of rational $\mathbfΔ^0_2$ omega powers, which completes the recent results of [FGL26].

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Jacques Duparc, Olivier Finkel, Dominique Lecomte. 2026-10-12. Some complete $ω$-powers of a one-counter language in the difference hierarchy. https://arxiv.org/abs/2610.16473

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

A Simple Obligation to Metric Interval Temporal Logic

Satisfiability of Metric Interval Temporal Logic (MITL) is a widely investigated subject. In this work, we present a new, and arguably simpler, approach for MITL satisfiability, based on an idea of tracking time-constrained obligations along a word. To check whether a Linear Temporal Logic (LTL) formula is true at a position of a word, it is natural to generate certain obligations that need to be satisfied at a later point. For instance, $a ~\mathcal{U}~ b$ (with strict Until semantics) is true at position $i$ if either $b$ or the set $\{a, a ~\mathcal{U}~ b\}$ is true at $i+1$. We enhance this idea in the context of MITL by introducing a notion of time inside these obligations. However, a naïve procedure could lead to more and more obligations getting generated along the word, with no bound on the number. We propose a simple mechanism to eliminate or merge redundant obligations. For MITL, this mechanism ensures that only a bounded number of obligations are maintained along the entire timed word. We develop this observation into a symbolic procedure for MITL satisfiability using regions.

cs.LO↗

Proofs Without Nominals: Gödel's Ontological Argument, its Shallow Embedding, and the Open Questions of the Monatshefte Notes

The shallow embedding of higher-order modal logic in classical higher-order logic, used in Benzmüller and Scott's Notes on Gödel's and Scott's variants of the ontological argument, reaches beyond the modal object language: its property quantifiers range over domains containing the nominals and satisfaction operators of hybrid logic. A proof using one proves a theorem of the embedding, not necessarily of the modal logic. That the framework affords this is not new. Whether a result is one of the modal logic can be settled by replaying it in an explicit calculus, one result at a time. More cheaply, and for all results at once, it can be approached by analysing what the embedding's proofs substitute. Every statement the Notes prove has a proof in the embedding substituting nothing outside the object language: 294 of them explicit proofs, machine-checked, none using a nominal. The Notes' own proofs substitute none either; what the check flags are terms a prover introduced. The three questions the Notes leave open are settled too, without nominals, but by the empty instance of the conjunction axiom, too cheaply to convince. As the Notes generalise it, to cover Gödel's "any number of summands", the axiom covers the empty conjunction and the singleton. This article restricts it to at least two different conjuncts, a non-degenerate reading of Gödel's footnote, and settles the questions again, without nominals. In effect the restriction excludes only the empty conjunction; the one-element case comes back with the other axioms. In one of the three variants the restriction refutes the possible existence of a God-like being; the answers return, with no side condition, once the Notes' non-emptiness clause is confined to Gödel's essence. Every theorem stated here is verified in Isabelle/HOL and independently in Lean 4; the countermodels are Nitpick's, checked by the build.

cs.LO↗

Certifying Almost-Sure Reachability in Unknown MDPs

{\em Specification-Guided Reinforcement Learning (RL)} has largely concerned itself with \emph{learning} an optimal policy against a formal specification in an unknown {\em Markov Decision Process (MDP)}. We take up the dual question. Given a policy already in hand, can one \emph{verify} that it is correct against a formal specification in an unknown MDP, using sampling access alone? Such a question arises naturally in safety-critical systems. We investigate it for the {\em almost-sure reachability property}, whose correctness is witnessed by a {\em ranking supermartingale (RSM)} certificate. Our first finding is negative. In the absence of any further information about the MDP, one can neither learn such a certificate nor verify a candidate one with probabilistic guarantees. On the positive side, we show that, under a mild restriction, a known lower bound $p_{\min}$ on nonzero transition probabilities, a correct certificate \emph{can} be learned with PAC-style guarantees. To the best of our knowledge, this is the first study of learning and verifying certificates for almost-sure reachability in unknown MDPs from sampling access alone. Finally, our experiments show that the $p_{\min}$-based sufficient condition, while sound, is conservative: the learned certificate often remains valid on the true MDP even when the condition fails.

cs.LO↗