arXiv subjects

Denis Kuperberg

Publications and source records attributed to Denis Kuperberg.

15 recordsLinked to original sources

arXiv2026

Generalised Quantifiers Based on Rabin-Mostowski Index

In this work we introduce new generalised quantifiers which allow us to express the Rabin-Mostowski index of automata. Our main results study expressive power and decidability of the monadic second-order (MSO) logic extended with these quantifiers. We study these problems in the realm of both $\omega$-words and infinite trees. As it turns out, the pictures in these two cases are very different. In the case of $\omega$-words the new quantifiers can be effectively expressed in pure MSO logic. In contrast, in the case of infinite trees, addition of these quantifiers leads to an undecidable formalism. To realise index-quantifier elimination, we consider the extension of MSO by game quantifiers. As a tool, we provide a specific quantifier-elimination procedure for them. Moreover, we introduce a novel construction of transducers realising strategies in $\omega$-regular games with monadic parameters.

cs.LO↗

arXiv2024

Explorable Parity Automata

We define the class of explorable automata on finite or infinite words. This is a generalization of History-Deterministic (HD) automata, where this time non-deterministic choices can be resolved by building finitely many simultaneous runs instead of just one. We show that recognizing HD parity automata of fixed index among explorable ones is in PTime, thereby giving a strong link between the two notions. We then show that recognizing explorable automata is ExpTime-complete, in the case of finite words or parity automata up to index [0, 2]. Additionally, we define the notion of {\omega}-explorable automata on infinite words, where countably many runs can be used to resolve the non-deterministic choices. We show ExpTime-completeness for {\omega}-explorability of automata on infinite words for the safety and coB\"uchi acceptance conditions. We finally characterize the expressivity of ({\omega}-)explorable automata with respect to the parity index hierarchy.

cs.FL↗

arXiv2024

On the Minimisation of Deterministic and History-Deterministic Generalised (co)B\"uchi Automata

We present a polynomial-time algorithm minimising the number of states of history-deterministic generalised coB\"uchi automata, building on the work of Abu Radi and Kupferman on coB\"uchi automata. On the other hand, we establish that the minimisation problem for both deterministic and history-deterministic generalised B\"uchi automata is NP-complete, as well as the problem of minimising at the same time the number of states and colours of history-deterministic generalised coB\"uchi automata.

cs.FL↗

arXiv2024

Tree algebras and bisimulation-invariant MSO on finite graphs

We establish that the bisimulation invariant fragment of MSO over finite transition systems is expressively equivalent over finite transition systems to modal mu-calculus, a question that had remained open for several decades. The proof goes by translating the question to an algebraic framework, and showing that the languages of regular trees that are recognized by finitary tree algebras are the regular ones, ie. the ones expressible in mu-calculus. This corresponds for trees to a weak form of the key translation of Wilke algebras to omega-semigroup over infinite words, and was also a missing piece in the algebraic theory of regular languages of infinite trees for twenty years.

cs.LO↗

arXiv2024

Positive and monotone fragments of FO and LTL

We study the positive logic FO+ on finite words, and its fragments, pursuing and refining the work initiated in [Kuperberg 2023]. First, we transpose notorious logic equivalences into positive first-order logic: FO+ is equivalent to LTL+ , and its two-variable fragment FO2+ with (resp. without) successor available is equivalent to UTL+ with (resp. without) the "next" operator X available. This shows that despite previous negative results, the class of FO+-definable languages exhibits some form of robustness. We then exhibit an example of an FO-definable monotone language on one predicate, that is not FO+-definable, refining the example from [Kuperberg 2023] with 3 predicates. Moreover, we show that such a counter-example cannot be FO2-definable.

cs.LO↗

arXiv2022

Positive First-order Logic on Words and Graphs

We study FO+, a fragment of first-order logic on finite words, where monadic predicates can only appear positively. We show that there is an FO-definable language that is monotone in monadic predicates but not definable in FO+. This provides a simple proof that Lyndon's preservation theorem fails on finite structures. We lift this example language to finite graphs, thereby providing a new result of independent interest for FO-definable graph classes: negation might be needed even when the class is closed under addition of edges. We finally show that the problem of whether a given regular language of finite words is definable in FO+ is undecidable.

cs.FL↗

arXiv2021

Positive first-order logic on words

We study FO+, a fragment of first-order logic on finite words, where monadic predicates can only appear positively. We show that there is a FO-definable language that is monotone in monadic predicates but not definable in FO+. This provides a simple proof that Lyndon's preservation theorem fails on finite structures. We additionally show that given a regular language, it is undecidable whether it is definable in FO+.

cs.FL↗

arXiv2020

On the Succinctness of Alternating Parity Good-for-Games Automata

We study alternating parity good-for-games (GFG) automata, i.e., alternating parity automata where both conjunctive and disjunctive choices can be resolved in an online manner, without knowledge of the suffix of the input word still to be read. We show that they can be exponentially more succinct than both their nondeterministic and universal counterparts. Furthermore, we present a single exponential determinisation procedure and an Exptime upper bound to the problem of recognising whether an alternating automaton is GFG. We also study the complexity of deciding "half-GFGness", a property specific to alternating automata that only requires nondeterministic choices to be resolved in an online manner. We show that this problem is PSpace-hard already for alternating automata on finite words.

cs.FL↗

arXiv2020

Bouncing threads for infinitary and circular proofs

We generalize the validity criterion for the infinitary proof system of the multiplicative additive linear logic with fixed points. Our criterion is designed to take into account axioms and cuts. We show that it is sound and enjoys the cut elimination property. We finally study its decidability properties, and prove that it is undecidable in general but becomes decidable under some restrictions.

cs.LO↗

arXiv2020

Regular resynchronizability of origin transducers is undecidable

We study the relation of containment up to unknown regular resynchronization between two-way non-deterministic transducers. We show that it constitutes a preorder, and that the corresponding equivalence relation is properly intermediate between origin equivalence and classical equivalence. We give a syntactical characterization for containment of two transducers up to resynchronization, and use it to show that this containment relation is undecidable already for one-way non-deterministic transducers, and for simple classes of resynchronizations. This answers the open problem stated in recent works, asking whether this relation is decidable for two-way non-deterministic transducers.

cs.FL↗

arXiv2020

On Succinctness and Recognisability of Alternating Good-for-Games Automata

We study alternating good-for-games (GFG) automata, i.e., alternating automata where both conjunctive and disjunctive choices can be resolved in an online manner, without knowledge of the suffix of the input word still to be read. We show that they can be exponentially more succinct than both their nondeterministic and universal counterparts. Furthermore, we lift many results from nondeterministic parity GFG automata to alternating ones: a single exponential determinisation procedure, an Exptime upper bound to the GFGness problem, a PTime algorithm for the GFGness problem of weak automata, and a reduction from a positive solution to the $G_2$ conjecture to a PTime algorithm for the GFGness problem of parity automata with a fixed index. The $G_2$ conjecture states that a nondeterministic parity automaton A is GFG if and only if a token game, known as the $G_2$ game, played on A is won by the first player. So far, it had only been proved for B\"uchi automata; we provide further evidence for it by proving it for coB\"uchi automata. We also study the complexity of deciding "half-GFGness", a property specific to alternating automata that only requires nondeterministic choices to be resolved in an online manner. We show that this problem is strictly more difficult than GFGness check, already for alternating automata on finite words.

cs.FL↗

arXiv2018

Computing the Width of Non-deterministic Automata

We introduce a measure called width, quantifying the amount of nondeterminism in automata. Width generalises the notion of good-for-games (GFG) automata, that correspond to NFAs of width 1, and where an accepting run can be built on-the-fly on any accepted input. We describe an incremental determinisation construction on NFAs, which can be more efficient than the full powerset determinisation, depending on the width of the input NFA. This construction can be generalised to infinite words, and is particularly well-suited to coB\"uchi automata. For coB\"uchi automata, this procedure can be used to compute either a deterministic automaton or a GFG one, and it is algorithmically more efficient in the last case. We show this fact by proving that checking whether a coB\"uchi automaton is determinisable by pruning is NP-complete. On finite or infinite words, we show that computing the width of an automaton is EXPTIME-complete. This implies EXPTIME-completeness for multipebble simulation games on NFAs.

cs.FL↗

arXiv2017

Trading Bounds for Memory in Games with Counters

We study two-player games with counters, where the objective of the first player is that the counter values remain bounded. We investigate the existence of a trade-off between the size of the memory and the bound achieved on the counters, which has been conjectured by Colcombet and Loeding. We show that unfortunately this conjecture does not hold: there is no trade-off between bounds and memory, even for finite arenas. On the positive side, we prove the existence of a trade-off for the special case of thin tree arenas. This allows to extend the theory of regular cost functions over thin trees, and obtain as a corollary the decidability of cost monadic second-order logic over thin trees.

cs.FL↗

arXiv2017

Soundness in negotiations

Negotiations are a formalism for describing multiparty distributed cooperation. Alternatively, they can be seen as a model of concurrency with synchronized choice as communication primitive. Well-designed negotiations must be sound, meaning that, whatever its current state, the negotiation can still be completed. In earlier work, Esparza and Desel have shown that deciding soundness of a negotiation is Pspace-complete, and in Ptime if the negotiation is deterministic. They have also extended their polynomial soundness algorithm to an intermediate class of acyclic, non-deterministic negotiations. However, they did not analyze the runtime of the extended algorithm, and also left open the complexity of the soundness problem for the intermediate class. In the first part of this paper we revisit the soundness problem for deterministic negotiations, and show that it is Nlogspace-complete, improving on the earlier algorithm, which requires linear space. In the second part we answer the question left open by Esparza and Desel. We prove that the soundness problem can be solved in polynomial time for acyclic, weakly non- deterministic negotiations, a more general class than the one considered by them. In the third and final part, we show that the techniques developed in the first two parts of the paper can be applied to analysis problems other than soundness, including the problem of detecting race conditions, and several classical static analysis problems. More specifically, we show that, while these problems are intractable for arbitrary acyclic deterministic negotiations, they become tractable in the sound case. So soundness is not only a desirable behavioral property in itself, but also helps to analyze other properties.

cs.FL↗

arXiv2017

Linear Temporal Logic for Regular Cost Functions

Regular cost functions have been introduced recently as an extension to the notion of regular languages with counting capabilities, which retains strong closure, equivalence, and decidability properties. The specificity of cost functions is that exact values are not considered, but only estimated. In this paper, we define an extension of Linear Temporal Logic (LTL) over finite words to describe cost functions. We give an explicit translation from this new logic to two dual form of cost automata, and we show that the natural decision problems for this logic are PSPACE-complete, as it is the case in the classical setting. We then algebraically characterize the expressive power of this logic, using a new syntactic congruence for cost functions introduced in this paper.

cs.LO↗