arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 0706.3523

There Exist some Omega-Powers of Any Borel Rank

Dominique Lecomte·Olivier Finkel
View original source ↗Read source document ↗Export metadata ↓

Abstract

Omega-powers of finitary languages are languages of infinite words (omega-languages) in the form V^omega, where V is a finitary language over a finite alphabet X. They appear very naturally in the characterizaton of regular or context-free omega-languages. Since the set of infinite words over a finite alphabet X can be equipped with the usual Cantor topology, the question of the topological complexity of omega-powers of finitary languages naturally arises and has been posed by Niwinski (1990), Simonnet (1992) and Staiger (1997). It has been recently proved that for each integer n > 0, there exist some omega-powers of context free languages which are Pi^0_n-complete Borel sets, that there exists a context free language L such that L^omega is analytic but not Borel, and that there exists a finitary language V such that V^omega is a Borel set of infinite rank. But it was still unknown which could be the possible infinite Borel ranks of omega-powers. We fill this gap here, proving the following very surprising result which shows that omega-powers exhibit a great topological complexity: for each non-null countable ordinal alpha, there exist some Sigma^0_alpha-complete omega-powers, and some Pi^0_alpha-complete omega-powers.

Explore related subjects

cs.LOcs.CCmath.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Dominique Lecomte, Olivier Finkel. 2007-06-25. There Exist some Omega-Powers of Any Borel Rank. https://arxiv.org/abs/0706.3523

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

KEEP EXPLORING

Related papers

arXiv2026

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↗
arXiv2026

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↗
arXiv2026

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↗