40 Search Results for "Löding, Christof"

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.24
Well-Founded Coalgebras Meet Kőnig’s Lemma

Authors: Henning Urbat and Thorsten Wißmann

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

Abstract
Kőnig’s lemma is a fundamental result about trees with countless applications in mathematics and computer science. In contrapositive form, it states that if a tree is finitely branching and well-founded (i.e. has no infinite paths), then it is finite. We present a coalgebraic version of Kőnig’s lemma featuring two dimensions of generalization: from finitely branching trees to coalgebras for a finitary endofunctor H, and from the base category of sets to a locally finitely presentable category ℂ, such as the category of posets, nominal sets, or convex sets. Our coalgebraic Kőnig’s lemma states that, under mild assumptions on ℂ and H, every well-founded coalgebra for H is the directed join of its well-founded subcoalgebras with finitely generated state space - in particular, the category of well-founded coalgebras is locally presentable. As applications, we derive versions of Kőnig’s lemma for graphs in a topos as well as for nominal and convex transition systems. Additionally, we show that the key construction underlying the proof gives rise to two simple constructions of the initial algebra (equivalently, the final recursive coalgebra) for the functor H: The initial algebra is both the colimit of all well-founded and of all recursive coalgebras with finitely presentable state space. Remarkably, this result holds even in settings where well-founded coalgebras form a proper subclass of recursive ones. The first construction of the initial algebra is entirely new, while for the second one our approach yields a short and transparent new correctness proof.
Cite as

Henning Urbat and Thorsten Wißmann. Well-Founded Coalgebras Meet Kőnig’s Lemma. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{urbat_et_al:LIPIcs.CSL.2026.24,
  author =	{Urbat, Henning and Wi{\ss}mann, Thorsten},
  title =	{{Well-Founded Coalgebras Meet K\H{o}nig’s Lemma}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{24:1--24:19},
  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.24},
  URN =		{urn:nbn:de:0030-drops-254485},
  doi =		{10.4230/LIPIcs.CSL.2026.24},
  annote =	{Keywords: K\H{o}nig’s Lemma, Well-Foundedness, Coalgebra}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.47
Useful Call-by-Value: A Semantic Interpretation via Quantitative Types

Authors: Pablo Barenbaum, Delia Kesner, and Mariana Milicich

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

Abstract
Useful evaluation is an optimised evaluation mechanism for functional programming languages. It relies on representing terms with sharing and imposing a restricted notion of useful substitutions, that intuitively disallows copying subterms that do not contribute to the progress of the computation. In particular, useful call-by-value evaluation optimises the standard call-by-value strategy by preserving its original semantics. This preservation result has been shown by means of syntactical rewriting techniques, difficult to adapt to alternative variants of the calculi at play. In this work, we present the first semantic model of useful call-by-value evaluation through the non-idempotent intersection type system 𝒰. Our first contribution is a characterisation of termination for useful call-by-value evaluation via system 𝒰. That is, a term is typable in system 𝒰 if and only if it terminates in the useful call-by-value strategy. As a second contribution, we show that system 𝒰 provides a quantitative interpretation for useful call-by-value evaluation, offering exact step-count information for program evaluation. Our third contribution is that termination in call-by-value and useful call-by-value are equivalent. This ensures in particular that call-by-value, which is (potentially) erasing, and useful call-by-value, which is non-erasing, are observationally equivalent. Even though the specification of the operational semantics of useful evaluation is highly complex, system 𝒰 is notably simple. As far as we know, system 𝒰 is one of the scarce quantitative type systems capturing exactly the substitution step-count for variables and abstractions in an open call-by-value strategy.
Cite as

Pablo Barenbaum, Delia Kesner, and Mariana Milicich. Useful Call-by-Value: A Semantic Interpretation via Quantitative Types. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 47:1-47:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{barenbaum_et_al:LIPIcs.CSL.2026.47,
  author =	{Barenbaum, Pablo and Kesner, Delia and Milicich, Mariana},
  title =	{{Useful Call-by-Value: A Semantic Interpretation via Quantitative Types}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{47:1--47: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.47},
  URN =		{urn:nbn:de:0030-drops-254721},
  doi =		{10.4230/LIPIcs.CSL.2026.47},
  annote =	{Keywords: Lambda calculus, Evaluation strategies, Call-by-Value, Useful Evaluation, Intersection types, Quantitative models}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2025.1
Quantum Circuit Verification - A Potential Roadmap (Invited Talk)

Authors: Parosh Aziz Abdulla, Yu-Fang Chen, Michal Hečko, Lukáš Holík, Ondřej Lengál, Jyun-Ao Lin, and Ramanathan Thinniyam Srinivasan

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
Quantum technologies are progressing at an extraordinary pace and are poised to transform numerous sectors both nationally and globally. Among them, quantum computing stands out for its potential to revolutionize areas such as cryptography, optimization, and the simulation of quantum systems, offering dramatic speed-ups for specific classes of problems. As quantum devices evolve and become increasingly pervasive, guaranteeing their correctness is of paramount importance. This necessitates the development of rigorous methods and tools to analyze and verify their behavior. However, the construction of such verification frameworks presents fundamental challenges. Quantum phenomena such as superposition and entanglement give rise to computational behaviors that differ profoundly from those of classical systems, leading to inherently probabilistic models and exponentially large state spaces, even for relatively small programs. Addressing these challenges requires building on the extensive expertise of the formal methods community in classical program verification, while incorporating recent advances and collaborative efforts in quantum systems. An interesting challenge for the verification community is to design and implement novel verification frameworks that transfer the key strengths of classical verification, such as expressive specification, precise error detection, automation, and scalability, to the quantum domain. We expect that the results of this research will play a crucial role in enabling the dependable deployment of quantum technologies across a wide range of future applications.
Cite as

Parosh Aziz Abdulla, Yu-Fang Chen, Michal Hečko, Lukáš Holík, Ondřej Lengál, Jyun-Ao Lin, and Ramanathan Thinniyam Srinivasan. Quantum Circuit Verification - A Potential Roadmap (Invited Talk). In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 1:1-1:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.FSTTCS.2025.1,
  author =	{Abdulla, Parosh Aziz and Chen, Yu-Fang and He\v{c}ko, Michal and Hol{\'\i}k, Luk\'{a}\v{s} and Leng\'{a}l, Ond\v{r}ej and Lin, Jyun-Ao and Srinivasan, Ramanathan Thinniyam},
  title =	{{Quantum Circuit Verification - A Potential Roadmap}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{1:1--1:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.1},
  URN =		{urn:nbn:de:0030-drops-250806},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.1},
  annote =	{Keywords: Quantum Circuits, Quantum Computing, Program Verification, Automata, Model Checking}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.18
Iterating Non-Aggregative Structure Compositions

Authors: Marius Bozga, Radu Iosif, and Florian Zuleger

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
An aggregative composition is a binary operation obeying the principle that the whole is determined by the sum of its parts. The development of graph algebras, on which the theory of formal graph languages is built, relies on aggregative compositions that behave like disjoint union, except for a set of well-marked interface vertices from both sides, that are joined. The same style of composition has been considered in the context of relational structures, that generalize graphs and use constant symbols to label the interface. In this paper, we study a non-aggregative composition operation, called fusion, that joins non-deterministically chosen elements from disjoint structures. The sets of structures obtained by iteratively applying fusion do not always have bounded tree-width, even when starting from a tree-width bounded set. First, we prove that the problem of the existence of a bound on the tree-width of the closure of a given set under fusion is decidable, when the input set is described inductively by a finite hyperedge-replacement (HR) grammar, written using the operations of aggregative composition, forgetting and renaming of constants. Such sets are usually called context-free. Second, assuming that the closure under fusion of a context-free set has bounded tree-width, we show that it is the language of an effectively constructible HR grammar. A possible application of the latter result is the possiblity of checking whether all structures from a non-aggregatively closed set having bounded tree-width satisfy a given monadic second order logic formula.
Cite as

Marius Bozga, Radu Iosif, and Florian Zuleger. Iterating Non-Aggregative Structure Compositions. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bozga_et_al:LIPIcs.FSTTCS.2025.18,
  author =	{Bozga, Marius and Iosif, Radu and Zuleger, Florian},
  title =	{{Iterating Non-Aggregative Structure Compositions}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{18:1--18:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.18},
  URN =		{urn:nbn:de:0030-drops-250997},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.18},
  annote =	{Keywords: Hyperedge replacement, Tree-width}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.35
Scalable Learning of One-Counter Automata via State-Merging Algorithms

Authors: Shibashis Guha, Anirban Majumdar, Prince Mathew, and A.V. Sreejith

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
We propose One-counter Positive Negative Inference (OPNI), a passive learning algorithm for deterministic real-time one-counter automata (DROCA). Inspired by the RPNI algorithm for regular languages, OPNI constructs a DROCA consistent with any given valid sample set. We further present a semi-algorithm for active learning of DROCA using OPNI, and provide an implementation of the approach. Our experimental results demonstrate that this approach scales more effectively than existing state-of-the-art algorithms. We also evaluate the performance of the proposed approach for learning visibly one-counter automata.
Cite as

Shibashis Guha, Anirban Majumdar, Prince Mathew, and A.V. Sreejith. Scalable Learning of One-Counter Automata via State-Merging Algorithms. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{guha_et_al:LIPIcs.FSTTCS.2025.35,
  author =	{Guha, Shibashis and Majumdar, Anirban and Mathew, Prince and Sreejith, A.V.},
  title =	{{Scalable Learning of One-Counter Automata via State-Merging Algorithms}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{35:1--35:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.35},
  URN =		{urn:nbn:de:0030-drops-251168},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.35},
  annote =	{Keywords: active learning, passive learning, one-counter automata, RPNI}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.8
Dynamic Membership for Regular Tree Languages

Authors: Antoine Amarilli, Corentin Barloy, Louis Jachiet, and Charles Paperman

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We study the dynamic membership problem for regular tree languages under relabeling updates: we fix an alphabet Σ and a regular tree language L over Σ (expressed, e.g., as a tree automaton), we are given a tree T with labels in Σ, and we must maintain the information of whether the tree T belongs to L while handling relabeling updates that change the labels of individual nodes in T. Our first contribution is to show that this problem admits an O(log n / log log n) algorithm for any fixed regular tree language, improving over known O(log n) algorithms. This generalizes the known O(log n / log log n) upper bound over words, and it matches the lower bound of Ω(log n / log log n) from dynamic membership to some word languages and from the existential marked ancestor problem. Our second contribution is to introduce a class of regular languages, dubbed almost-commutative tree languages, and show that dynamic membership to such languages under relabeling updates can be decided in constant time per update. Almost-commutative languages generalize both commutative languages and finite languages: they are the analogue for trees of the ZG languages enjoying constant-time dynamic membership over words. Our main technical contribution is to show that this class is conditionally optimal when we assume that the alphabet features a neutral letter, i.e., a letter that has no effect on membership to the language. More precisely, we show that any regular tree language with a neutral letter which is not almost-commutative cannot be maintained in constant time under the assumption that the prefix-U1 problem from [Antoine Amarilli et al., 2021] also does not admit a constant-time algorithm.
Cite as

Antoine Amarilli, Corentin Barloy, Louis Jachiet, and Charles Paperman. Dynamic Membership for Regular Tree Languages. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{amarilli_et_al:LIPIcs.MFCS.2025.8,
  author =	{Amarilli, Antoine and Barloy, Corentin and Jachiet, Louis and Paperman, Charles},
  title =	{{Dynamic Membership for Regular Tree Languages}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.8},
  URN =		{urn:nbn:de:0030-drops-241155},
  doi =		{10.4230/LIPIcs.MFCS.2025.8},
  annote =	{Keywords: automaton, dynamic membership, incremental maintenance, forest algebra}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.50
Lexicographic Transductions of Finite Words

Authors: Emmanuel Filiot, Nathan Lhote, and Pierre-Alain Reynier

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
Regular transductions over finite words have linear input-to-output growth. This class of transductions enjoys many characterizations, such as transductions computable by two-way transducers as well as transductions definable in MSO (in the sense of Courcelle). Recently, regular transductions have been extended by Bojańczyk to polyregular transductions, which have polynomial growth, and are characterized by pebble transducers and MSO interpretations. Another class of interest is that of transductions defined by streaming string transducers or marble transducers, which have exponential growth and are incomparable with polyregular transductions. In this paper, we consider MSO set interpretations (MSOSI) over finite words, that were introduced by Colcombet and Loeding. MSOSI are a natural candidate for the class of "regular transductions with exponential growth", and are rather well behaved. However, MSOSI for now lacks two desirable properties that regular and polyregular transductions have. The first property is to have an automata description. This property is closely related to a second property, that of being regularity preserving, meaning preserving regular languages under inverse image. We first show that if MSOSI are (effectively) regularity preserving then any automatic ω-word has a decidable MSO theory, an almost 20 years old conjecture of Bárány. Our main contribution is the introduction of a class of transductions of exponential growth, which we call lexicographic transductions. We provide three different presentations for this class: first, as the closure of simple transductions (recognizable transductions) under a single operator called maplex; second, as a syntactic fragment of MSOSI (but the regular languages are given by automata instead of formulas); and third, we give an automaton based model called nested marble transducers, which generalize both marble transducers and pebble transducers. We show that this class enjoys many nice properties including being regularity preserving.
Cite as

Emmanuel Filiot, Nathan Lhote, and Pierre-Alain Reynier. Lexicographic Transductions of Finite Words. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 50:1-50:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.MFCS.2025.50,
  author =	{Filiot, Emmanuel and Lhote, Nathan and Reynier, Pierre-Alain},
  title =	{{Lexicographic Transductions of Finite Words}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{50:1--50:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.50},
  URN =		{urn:nbn:de:0030-drops-241572},
  doi =		{10.4230/LIPIcs.MFCS.2025.50},
  annote =	{Keywords: Transducers, Automata, MSO, Logical interpretations, Automatic structures}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.31
Games with ω-Automatic Preference Relations

Authors: Véronique Bruyère, Christophe Grandmont, and Jean-François Raskin

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
This paper investigates Nash equilibria (NEs) in multi-player turn-based games on graphs, where player preferences are modeled as ω-automatic relations via deterministic parity automata. Unlike much of the existing literature, which focuses on specific reward functions, our results apply to any preference relation definable by an ω-automatic relation. We analyze the computational complexity of determining the existence of an NE (possibly under some constraints), verifying whether a given strategy profile forms an NE, and checking whether a specific outcome can be realized by an NE. When a (constrained) NE exists, we show that there always exists one with finite-memory strategies. Finally, we explore fundamental properties of ω-automatic relations and their implications in the existence of equilibria.
Cite as

Véronique Bruyère, Christophe Grandmont, and Jean-François Raskin. Games with ω-Automatic Preference Relations. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bruyere_et_al:LIPIcs.MFCS.2025.31,
  author =	{Bruy\`{e}re, V\'{e}ronique and Grandmont, Christophe and Raskin, Jean-Fran\c{c}ois},
  title =	{{Games with \omega-Automatic Preference Relations}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{31:1--31:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.31},
  URN =		{urn:nbn:de:0030-drops-241381},
  doi =		{10.4230/LIPIcs.MFCS.2025.31},
  annote =	{Keywords: Games played on graphs, Nash equilibrium, \omega-automatic relations, \omega-recognizable relations, constrained Nash equilibria existence problem}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.21
Quantitative Language Automata

Authors: Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi, and N. Ege Saraç

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

Abstract
A quantitative word automaton (QWA) defines a function from infinite words to values. For example, every infinite run of a limit-average QWA 𝒜 obtains a mean payoff, and every word w ∈ Σ^ω is assigned the maximal mean payoff obtained by nondeterministic runs of 𝒜 over w. We introduce quantitative language automata (QLAs) that define functions from language generators (i.e., implementations) to values, where a language generator can be nonprobabilistic, defining a set of infinite words, or probabilistic, defining a probability measure over infinite words. A QLA consists of a QWA and an aggregator function. For example, given a QWA 𝒜, the infimum aggregator maps each language L ⊆ Σ^ω to the greatest lower bound assigned by 𝒜 to any word in L. For boolean value sets, QWAs define boolean properties of traces, and QLAs define boolean properties of sets of traces, i.e., hyperproperties. For more general value sets, QLAs serve as a specification language for a generalization of hyperproperties, called quantitative hyperproperties. A nonprobabilistic (resp. probabilistic) quantitative hyperproperty assigns a value to each set (resp. distribution) G of traces, e.g., the minimal (resp. expected) average response time exhibited by the traces in G. We give several examples of quantitative hyperproperties and investigate three paradigmatic problems for QLAs: evaluation, nonemptiness, and universality. In the evaluation problem, given a QLA 𝔸 and an implementation G, we ask for the value that 𝔸 assigns to G. In the nonemptiness (resp. universality) problem, given a QLA 𝔸 and a value k, we ask whether 𝔸 assigns at least k to some (resp. every) language. We provide a comprehensive picture of decidability for these problems for QLAs with common aggregators as well as their restrictions to ω-regular languages and trace distributions generated by finite-state Markov chains.
Cite as

Thomas A. Henzinger, Pavol Kebis, Nicolas Mazzocchi, and N. Ege Saraç. Quantitative Language Automata. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 21:1-21:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{henzinger_et_al:LIPIcs.CONCUR.2025.21,
  author =	{Henzinger, Thomas A. and Kebis, Pavol and Mazzocchi, Nicolas and Sara\c{c}, N. Ege},
  title =	{{Quantitative Language Automata}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{21:1--21:24},
  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.21},
  URN =		{urn:nbn:de:0030-drops-239718},
  doi =		{10.4230/LIPIcs.CONCUR.2025.21},
  annote =	{Keywords: Quantitative hyperproperties, quantitative automata, automata-based verification}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.38
Reachability in Vector Addition System with States Parameterized by Geometric Dimension

Authors: Yangluo Zheng

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

Abstract
The geometric dimension of a vector addition system with states (VASS), emerged in Leroux and Schmitz (2019) and formalized by Fu, Yang, and Zheng (2024), quantifies the dimension of the vector space spanned by cycle effects in the system. This paper examines the VASS reachability problem through the lens of geometric dimension, revealing key differences from the traditional dimensional parameterization. Notably, we establish that the reachability problem for both geometrically 1-dimensional and 2-dimensional VASS is PSPACE-complete, achieved by extending the pumping technique initially proposed by Czerwiński et al. (2019).
Cite as

Yangluo Zheng. Reachability in Vector Addition System with States Parameterized by Geometric Dimension. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 38:1-38:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zheng:LIPIcs.CONCUR.2025.38,
  author =	{Zheng, Yangluo},
  title =	{{Reachability in Vector Addition System with States Parameterized by Geometric Dimension}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{38:1--38:18},
  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.38},
  URN =		{urn:nbn:de:0030-drops-239888},
  doi =		{10.4230/LIPIcs.CONCUR.2025.38},
  annote =	{Keywords: Petri net, vector addition system, reachability, geometric dimension, pumping}
}
Document
(Co)algebraic pearl
DOI: 10.4230/LIPIcs.CALCO.2025.16
Active Learning of Upward-Closed Sets of Words ((Co)algebraic pearl)

Authors: Quentin Aristote

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract
We give a new proof of a result from well quasi-order theory on the computability of bases for upwards-closed sets of words. This new proof is based on Angluin’s L* algorithm, that learns an automaton from a minimally adequate teacher. This relates in particular two results from the 1980s: Angluin’s L* algorithm, and a result from Valk and Jantzen on the computability of bases for upwards-closed sets of tuples of integers. Along the way, we describe an algorithm for learning quasi-ordered automata from a minimally adequate teacher, and extend a generalization of Valk and Jantzen’s result, encompassing both words and integers, to finitely generated monoids.
Cite as

Quentin Aristote. Active Learning of Upward-Closed Sets of Words ((Co)algebraic pearl). In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 16:1-16:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aristote:LIPIcs.CALCO.2025.16,
  author =	{Aristote, Quentin},
  title =	{{Active Learning of Upward-Closed Sets of Words}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{16:1--16:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.16},
  URN =		{urn:nbn:de:0030-drops-235751},
  doi =		{10.4230/LIPIcs.CALCO.2025.16},
  annote =	{Keywords: active learning, well quasi-orders, Valk-Jantzen lemma, piecewise-testable languages, monoids}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.5
The Cost of Skeletal Call-By-Need, Smoothly

Authors: Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot, and Claudio Sacerdoti Coen

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Skeletal call-by-need is an optimization of call-by-need evaluation also known as "fully lazy sharing": when the duplication of a value has to take place, it is first split into "skeleton", which is then duplicated, and "flesh" which is instead kept shared. Here, we provide two cost analyses of skeletal call-by-need. Firstly, we provide a family of terms showing that skeletal call-by-need can be asymptotically exponentially faster than call-by-need in both time and space; it is the first such evidence, to our knowledge. Secondly, we prove that skeletal call-by-need can be implemented efficiently, that is, with bi-linear overhead. This result is obtained by providing a new smooth presentation of ideas by Shivers and Wand for the reconstruction of skeletons, which is then smoothly plugged into the study of an abstract machine following the distillation technique by Accattoli et al.
Cite as

Beniamino Accattoli, Francesco Magliocca, Loïc Peyrot, and Claudio Sacerdoti Coen. The Cost of Skeletal Call-By-Need, Smoothly. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 5:1-5:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.FSCD.2025.5,
  author =	{Accattoli, Beniamino and Magliocca, Francesco and Peyrot, Lo\"{i}c and Sacerdoti Coen, Claudio},
  title =	{{The Cost of Skeletal Call-By-Need, Smoothly}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{5:1--5:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.5},
  URN =		{urn:nbn:de:0030-drops-236206},
  doi =		{10.4230/LIPIcs.FSCD.2025.5},
  annote =	{Keywords: \lambda-calculus, abstract machines, call-by-need, cost models}
}
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.155
Approximate Problems for Finite Transducers

Authors: Emmanuel Filiot, Ismaël Jecker, Khushraj Madnani, and Saina Sunny

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

Abstract
Finite (word) state transducers extend finite state automata by defining a binary relation over finite words, called rational relation. If the rational relation is the graph of a function, this function is said to be rational. The class of sequential functions is a strict subclass of rational functions, defined as the functions recognised by input-deterministic finite state transducers. The class membership problems between those classes are known to be decidable. We consider approximate versions of these problems and show they are decidable as well. This includes the approximate functionality problem, which asks whether given a rational relation (by a transducer), is it close to a rational function, and the approximate determinisation problem, which asks whether a given rational function is close to a sequential function. We prove decidability results for several classical distances, including Hamming and Levenshtein edit distance. Finally, we investigate the approximate uniformisation problem, which asks, given a rational relation R, whether there exists a sequential function that is close to some function uniformising R. As its exact version, we prove that this problem is undecidable.
Cite as

Emmanuel Filiot, Ismaël Jecker, Khushraj Madnani, and Saina Sunny. Approximate Problems for Finite Transducers. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 155:1-155:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{filiot_et_al:LIPIcs.ICALP.2025.155,
  author =	{Filiot, Emmanuel and Jecker, Isma\"{e}l and Madnani, Khushraj and Sunny, Saina},
  title =	{{Approximate Problems for Finite Transducers}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{155:1--155: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.155},
  URN =		{urn:nbn:de:0030-drops-235329},
  doi =		{10.4230/LIPIcs.ICALP.2025.155},
  annote =	{Keywords: Finite state transducers, Edit distance, Determinisation, Functionality}
}
  • Refine by Type
  • 40 Document/PDF
  • 21 Document/HTML

  • Refine by Publication Year
  • 3 2026
  • 18 2025
  • 2 2023
  • 1 2022
  • 2 2021
  • Show More...

  • Refine by Author
  • 18 Löding, Christof
  • 5 Filiot, Emmanuel
  • 4 Winter, Sarah
  • 3 Bohn, León
  • 3 Jecker, Ismaël
  • Show More...

  • Refine by Series/Journal
  • 39 LIPIcs
  • 1 DagSemProc

  • Refine by Classification
  • 13 Theory of computation → Automata over infinite objects
  • 5 Theory of computation → Formal languages and automata theory
  • 4 Theory of computation → Logic and verification
  • 4 Theory of computation → Quantitative automata
  • 3 Theory of computation → Logic
  • Show More...

  • Refine by Keyword
  • 4 Automata
  • 4 active learning
  • 4 parity automata
  • 3 Tree automata
  • 3 decidability
  • 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