11 Search Results for "Bradfield, Julian"

Document
DOI: 10.4230/LIPIcs.STACS.2026.63
Generalised Quantifiers Based on Rabin-Mostowski Index

Authors: Denis Kuperberg, Damian Niwiński, Paweł Parys, and Michał Skrzypczak

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)

Abstract
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 ω-words and infinite trees. As it turns out, the pictures in these two cases are very different. In the case of ω-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 ω-regular games with monadic parameters.
Cite as

Denis Kuperberg, Damian Niwiński, Paweł Parys, and Michał Skrzypczak. Generalised Quantifiers Based on Rabin-Mostowski Index. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 63:1-63:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{kuperberg_et_al:LIPIcs.STACS.2026.63,
  author =	{Kuperberg, Denis and Niwi\'{n}ski, Damian and Parys, Pawe{\l} and Skrzypczak, Micha{\l}},
  title =	{{Generalised Quantifiers Based on Rabin-Mostowski Index}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{63:1--63:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.63},
  URN =		{urn:nbn:de:0030-drops-255526},
  doi =		{10.4230/LIPIcs.STACS.2026.63},
  annote =	{Keywords: monadic quantifiers, decidability, quantifier elimination, parity automata, game quantifier, Rabin-Mostowski index}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.23
A Logic for Fresh Labelled Transition Systems

Authors: Mohamed H. Bandukara and Nikos Tzevelekos

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We introduce a Hennessy-Milner logic with recursion for Fresh Labelled Transition Systems (FLTSs). These are nominal labelled transition systems which keep track of the history, i.e. of data values seen so far, and can model fresh data generation. In particular, FLTSs generalise the computations of Fresh-Register Automata, which in turn can be seen as a "regular" class of history-tracking automata operating on infinite input alphabets. The logic we introduce is a modal mu-calculus equipped with infinite disjunctions over arbitrary and fresh data values respectively, while its recursion is parameterised on vectors of data values. It can express a variety of properties, such as the existence of an infinite path of distinct data values, the absence of paths where values are repeated, or the existence of a finite path where some taint property is violated. We study the model-checking problem and its complexity via a reduction to parity games and, using nominal sets techniques, provide an exponential upper bound for it.
Cite as

Mohamed H. Bandukara and Nikos Tzevelekos. A Logic for Fresh Labelled Transition Systems. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 23:1-23:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bandukara_et_al:LIPIcs.CSL.2026.23,
  author =	{Bandukara, Mohamed H. and Tzevelekos, Nikos},
  title =	{{A Logic for Fresh Labelled Transition Systems}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{23:1--23:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.23},
  URN =		{urn:nbn:de:0030-drops-254478},
  doi =		{10.4230/LIPIcs.CSL.2026.23},
  annote =	{Keywords: Nominal Transition Systems, Hennessy-Milner Logic, Modal Mu-Calculus, Register Automata, Nominal Sets, Parity Games}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.4
Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory

Authors: Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Runtime verification consists in checking whether a system satisfies a given specification by observing the execution trace it produces. In the regular setting, the modal μ-calculus provides a versatile formalism for expressing specifications of the control flow of the system. This paper focuses on the data flow and studies an extension of that logic that allows it to express data-dependent properties, identifying fragments that can be verified at runtime and with what correctness guarantees. The logic studied here is closely related with register automata with guessing. That correspondence yields a monitor synthesis algorithm, and a strict hierarchy among the various fragments of the logic, in contrast to the regular setting. We then exhibit a fragment of the logic that can express all monitorable formulae in the logic without greatest fixed-points but not in the full logic, and show this is the best we can get.
Cite as

Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2025.4,
  author =	{Aceto, Luca and Achilleos, Antonis and Attard, Duncan Paul and Exibard, L\'{e}o and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna and Lehtinen, Karoliina},
  title =	{{Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.4},
  URN =		{urn:nbn:de:0030-drops-239546},
  doi =		{10.4230/LIPIcs.CONCUR.2025.4},
  annote =	{Keywords: Runtime verification, monitorability, \muHML with data, register automata}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CONCUR.2025.3
On-The-Fly Verification: Advancements in Dependency Graphs (Invited Talk)

Authors: Jiří Srba

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Dependency graphs have emerged as a versatile and powerful formalism with wide-ranging applications in formal verification. In this extended abstract, we provide an overview of selected advancements in on-the-fly verification techniques based on dependency graphs, focusing on the recent developments, optimizations and generalizations of this generic verification framework.
Cite as

Jiří Srba. On-The-Fly Verification: Advancements in Dependency Graphs (Invited Talk). In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 3:1-3:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{srba:LIPIcs.CONCUR.2025.3,
  author =	{Srba, Ji\v{r}{\'\i}},
  title =	{{On-The-Fly Verification: Advancements in Dependency Graphs}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{3:1--3:5},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.3},
  URN =		{urn:nbn:de:0030-drops-239534},
  doi =		{10.4230/LIPIcs.CONCUR.2025.3},
  annote =	{Keywords: dependency graphs, Boolean equation systems, on-the-fly algorithms, fixed-point computation, applications}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.160
Using Games and Universal Trees to Characterise the Nondeterministic Index of Tree Languages

Authors: Olivier Idir and Karoliina Lehtinen

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
The parity index problem of tree automata asks, given a regular tree language L and a set of priorities J, is L J-feasible, that is, recognised by a nondeterministic parity automaton with priorities J? This is a long-standing open problem, of which only a few sub-cases and variations are known to be decidable. In a significant but technically difficult step, Colcombet and Löding reduced the problem to the uniform universality of distance-parity automata. In this article, we revisit the index problem using tools from the parity game literature. We add some counters to Lehtinen’s register game, originally used to solve parity games in quasipolynomial time, and use this novel game to characterise J-feasibility. This provides a alternative proof to Colcombet and Löding’s reduction. We then provide a second characterisation, based on the notion of attractor decompositions and the complexity of their structure, as measured by a parameterised version of their Strahler number, which we call n-Strahler number. Finally, we rephrase this result using the notion of universal tree extended to automata: a guidable automaton recognises a [1,2j]-feasible language if and only if it admits a universal tree with n-Strahler number j, for some n. In particular, a language recognised by a guidable automaton {A} is Büchi-feasible if and only if there is a uniform bound n ∈ ℕ such that all trees in the language admit an accepting run with an attractor decomposition of width bounded by n. Equivalently, the language is Büchi-feasible if and only if {A} admits a finite universal tree. While we do not solve the decidability of the index problem, our work makes the state-of-the-art more accessible and brings to light the deep relationships between the J-feasibility of a language and attractor decompositions, universal trees and Lehtinen’s register game.
Cite as

Olivier Idir and Karoliina Lehtinen. Using Games and Universal Trees to Characterise the Nondeterministic Index of Tree Languages. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 160:1-160:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{idir_et_al:LIPIcs.ICALP.2025.160,
  author =	{Idir, Olivier and Lehtinen, Karoliina},
  title =	{{Using Games and Universal Trees to Characterise the Nondeterministic Index of Tree Languages}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{160:1--160:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.160},
  URN =		{urn:nbn:de:0030-drops-235377},
  doi =		{10.4230/LIPIcs.ICALP.2025.160},
  annote =	{Keywords: Tree automata, parity automata, Mostowski index, Strahler number, attractor decomposition, universal trees}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.162
Positive and Monotone Fragments of FO and LTL

Authors: Simon Iosti, Denis Kuperberg, and Quentin Moreau

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
We study the positive logic FO^+ on finite words, and its fragments, pursuing and refining the work initiated in [Denis Kuperberg, 2023]. First, we transpose notorious logic equivalences into positive first-order logic: FO^+ is equivalent to LTL^+, and its two-variable fragment FO^{2+} 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 [Denis Kuperberg, 2023] with 3 predicates. Moreover, we show that such a counter-example cannot be FO²-definable. Finally, we provide a new example distinguishing the positive and monotone versions of FO² without quantifier alternation. This does not rely on a variant of the previously known counter-example, and witnesses a new phenomenon.
Cite as

Simon Iosti, Denis Kuperberg, and Quentin Moreau. Positive and Monotone Fragments of FO and LTL. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 162:1-162:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{iosti_et_al:LIPIcs.ICALP.2025.162,
  author =	{Iosti, Simon and Kuperberg, Denis and Moreau, Quentin},
  title =	{{Positive and Monotone Fragments of FO and LTL}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{162:1--162:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.162},
  URN =		{urn:nbn:de:0030-drops-235398},
  doi =		{10.4230/LIPIcs.ICALP.2025.162},
  annote =	{Keywords: Positive logic, LTL, separation, first-order, monotone}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.164
A Collapse of the Parity Index Hierarchy of Tree Automata, Based on Cantor-Bendixson Ranks

Authors: Karoliina Lehtinen and Nathan Lhote

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
Over words, nondeterministic Büchi automata and alternating weak automata are as expressive as parity automata with any number of priorities. Over trees, the Büchi acceptance condition is strictly weaker and the more priorities we allow, the more languages parity automata can recognise. We say that on words, the parity-index hierarchies of nondeterministic and alternating automata collapse to the Büchi and weak level, respectively, while both are infinite over trees. We ask when is Büchi enough?, that is, on which classes of trees are nondeterministc Büchi automata as expressive as parity automata. Similarly for alternating weak automata. We work in the setting of unranked unordered trees, in which there is no order among the children of nodes. We find that for nondeterministic and alternating automata, the parity-index hierarchy collapses to the Büchi level and weak level, respectively, for any class of trees of finitely bounded Cantor-Bendixson rank, a topological measure of tree complexity. Over trees of countable Cantor-Bendixson rank, (a.k.a. thin trees) the parity-index hierarchy of both nondeterministic and alternating automata collapses to the level [1,2,3], as was already known for ordered trees. These results are in some sense optimal: on the class of trees of finite but unbounded Cantor-Bendixson rank, two priorities do not suffice to recognise all parity-recognisable languages, even for alternating automata.
Cite as

Karoliina Lehtinen and Nathan Lhote. A Collapse of the Parity Index Hierarchy of Tree Automata, Based on Cantor-Bendixson Ranks. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 164:1-164:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lehtinen_et_al:LIPIcs.ICALP.2025.164,
  author =	{Lehtinen, Karoliina and Lhote, Nathan},
  title =	{{A Collapse of the Parity Index Hierarchy of Tree Automata, Based on Cantor-Bendixson Ranks}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{164:1--164:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.164},
  URN =		{urn:nbn:de:0030-drops-235418},
  doi =		{10.4230/LIPIcs.ICALP.2025.164},
  annote =	{Keywords: Parity tree automata, alternating automata, Cantor-Bendixson rank}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.145
Reducing Stochastic Games to Semidefinite Programming

Authors: Manuel Bodirsky, Georg Loho, and Mateusz Skomra

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
We present a polynomial-time reduction from max-average constraints to the feasibility problem for semidefinite programs. This shows that Condon’s simple stochastic games, stochastic mean payoff games, and in particular mean payoff games and parity games can all be reduced to semidefinite programming.
Cite as

Manuel Bodirsky, Georg Loho, and Mateusz Skomra. Reducing Stochastic Games to Semidefinite Programming. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 145:1-145:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bodirsky_et_al:LIPIcs.ICALP.2025.145,
  author =	{Bodirsky, Manuel and Loho, Georg and Skomra, Mateusz},
  title =	{{Reducing Stochastic Games to Semidefinite Programming}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{145:1--145:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.145},
  URN =		{urn:nbn:de:0030-drops-235224},
  doi =		{10.4230/LIPIcs.ICALP.2025.145},
  annote =	{Keywords: Mean-payoff games, stochastic games, semidefinite programming, max-average constraints, max-atom problem}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.168
Nondeterministic Tree-Walking Automata Are Not Closed Under Complementation

Authors: Olga Martynova and Alexander Okhotin

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
It is proved that the family of tree languages recognized by nondeterministic tree-walking automata is not closed under complementation, solving a problem raised by Bojańczyk and Colcombet (https://doi.org/10.1137/050645427, SIAM J. Comp. 38 (2008) 658-701). In addition, it is shown that nondeterministic tree-walking automata are stronger than unambiguous tree-walking automata.
Cite as

Olga Martynova and Alexander Okhotin. Nondeterministic Tree-Walking Automata Are Not Closed Under Complementation. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 168:1-168:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{martynova_et_al:LIPIcs.ICALP.2025.168,
  author =	{Martynova, Olga and Okhotin, Alexander},
  title =	{{Nondeterministic Tree-Walking Automata Are Not Closed Under Complementation}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{168:1--168:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.168},
  URN =		{urn:nbn:de:0030-drops-235459},
  doi =		{10.4230/LIPIcs.ICALP.2025.168},
  annote =	{Keywords: Finite automata, tree-walking automata, complementation}
}
Document
DOI: 10.4230/LIPIcs.STACS.2025.69
A Dichotomy Theorem for Ordinal Ranks in MSO

Authors: Damian Niwiński, Paweł Parys, and Michał Skrzypczak

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
We focus on formulae ∃X.φ(Y, X) of monadic second-order logic over the full binary tree, such that the witness X is a well-founded set. The ordinal rank rank(X) < ω₁ of such a set X measures its depth and branching structure. We search for the least upper bound for these ranks, and discover the following dichotomy depending on the formula φ. Let η_φ be the minimal ordinal such that, whenever an instance Y satisfies the formula, there is a witness X with rank(X) ≤ η_φ. Then η_φ is either strictly smaller than ω² or it reaches the maximal possible value ω₁. Moreover, it is decidable which of the cases holds. The result has potential for applications in a variety of ordinal-related problems, in particular it entails a result about the closure ordinal of a fixed-point formula.
Cite as

Damian Niwiński, Paweł Parys, and Michał Skrzypczak. A Dichotomy Theorem for Ordinal Ranks in MSO. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 69:1-69:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{niwinski_et_al:LIPIcs.STACS.2025.69,
  author =	{Niwi\'{n}ski, Damian and Parys, Pawe{\l} and Skrzypczak, Micha{\l}},
  title =	{{A Dichotomy Theorem for Ordinal Ranks in MSO}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{69:1--69:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.69},
  URN =		{urn:nbn:de:0030-drops-228942},
  doi =		{10.4230/LIPIcs.STACS.2025.69},
  annote =	{Keywords: dichotomy result, limit ordinal, countable ordinals, nondeterministic tree automata}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.116
Team building in dependence

Authors: Julian Bradfield

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
Hintikka and Sandu's Independence-Friendly Logic was introduced as a logic for partially ordered quantification, in which the independence of (existential) quantifiers from previous (universal) quantifiers is written by explicit syntax. It was originally given a semantics by games of imperfect information; Hodges then gave a (necessarily) second-order Tarskian semantics. More recently, Väänänen (2007) has proposed that the many curious features of IF logic can be better understood in his Dependence Logic, in which the (in)dependence of variables is stated in atomic formula, rather than by changing the definition of quantifier; he gives semantics in Tarskian form, via imperfect information games, and via a routine second-order perfect information game. He then defines Team Logic, where classical negation is added to the mix, resulting in a full second-order expressive logic. He remarks that no game semantics appears possible (other than by playing at second order). In this article, we explore an alternative approach to game semantics for DL, where we avoid imperfect information, yet stay locally apparently first-order, by sweeping the second-order information into longer games (infinite games in the case of countable models). Extending the game to Team Logic is not possible in standard games, but we conjecture a move to transfinite games may achieve a 'natural' game for Team Logic.
Cite as

Julian Bradfield. Team building in dependence. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 116-128, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{bradfield:LIPIcs.CSL.2013.116,
  author =	{Bradfield, Julian},
  title =	{{Team building in dependence}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{116--128},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.116},
  URN =		{urn:nbn:de:0030-drops-41935},
  doi =		{10.4230/LIPIcs.CSL.2013.116},
  annote =	{Keywords: partially ordered quantification, independence-friendly logic, game semantics}
}
  • Refine by Type
  • 11 Document/PDF
  • 10 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 8 2025
  • 1 2013

  • Refine by Author
  • 3 Lehtinen, Karoliina
  • 2 Kuperberg, Denis
  • 2 Niwiński, Damian
  • 2 Parys, Paweł
  • 2 Skrzypczak, Michał
  • Show More...

  • Refine by Series/Journal
  • 11 LIPIcs

  • Refine by Classification
  • 5 Theory of computation → Automata over infinite objects
  • 3 Theory of computation → Logic and verification
  • 3 Theory of computation → Modal and temporal logics
  • 2 Theory of computation → Formal languages and automata theory
  • 2 Theory of computation → Tree languages
  • Show More...

  • Refine by Keyword
  • 2 parity automata
  • 1 Boolean equation systems
  • 1 Cantor-Bendixson rank
  • 1 Finite automata
  • 1 Hennessy-Milner Logic
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact