35 Search Results for "Pin, Jean-Éric"


Document
Strategy Repair in Reachability Games via a Graph Quotientation

Authors: Tiziana Calamoneri, Pierre Gaillard, Giacomo Paesani, and Giuseppe Perelli

Published in: LIPIcs, Volume 370, 20th Scandinavian Symposium on Algorithm Theory (SWAT 2026)


Abstract
Reachability Games over graphs (RGs) are a powerful modelling tool for synthesis and planning. The solutions to RGs are strategies that are used in program design. Sometimes, due to model deviation at execution time, specification updates, or simply a bug, the strategy provided as a solution to an RG no longer works. Strategy Repair aims to solve this problem by adjusting strategies with a minimum number of modifications. Such a minimisation requirement is motivated by the costs that one may incur when implementing the new strategy. To minimise implementation costs, one wants to reuse as much of the provided strategy as possible. In the literature, Strategy Repair has been investigated from both theoretical and practical perspectives. First, it has been shown to be NP-complete. Second, two algorithmic approaches have been proposed to tackle the problem in practice, one provides an optimal solution, the other an approximated solution. Both approaches underutilise the graph-theoretical properties of games, which could significantly improve their performance and accuracy (in the case of approximation algorithms). This paper provides a graph-theoretic characterisation of Strategy Repair that provably improves every algorithmic approach to solving the problem. It does so by introducing a new notion of quotient graph that allows us to identify and merge those vertices that are equivalent from the perspective of every solution to the problem. This way, solving Strategy Repair can be done in a reduced instance, which we call the quotient game. The approach not only reduces the problem’s input size, but also improves the effectiveness of MustFix, an optimisation condition previously introduced for the problem. Besides the theoretical characterisation, we test our approach empirically by running experiments to demonstrate improvements over the quotient graph approach.

Cite as

Tiziana Calamoneri, Pierre Gaillard, Giacomo Paesani, and Giuseppe Perelli. Strategy Repair in Reachability Games via a Graph Quotientation. In 20th Scandinavian Symposium on Algorithm Theory (SWAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 370, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{calamoneri_et_al:LIPIcs.SWAT.2026.12,
  author =	{Calamoneri, Tiziana and Gaillard, Pierre and Paesani, Giacomo and Perelli, Giuseppe},
  title =	{{Strategy Repair in Reachability Games via a Graph Quotientation}},
  booktitle =	{20th Scandinavian Symposium on Algorithm Theory (SWAT 2026)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-421-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{370},
  editor =	{Fraigniaud, Pierre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SWAT.2026.12},
  URN =		{urn:nbn:de:0030-drops-260481},
  doi =		{10.4230/LIPIcs.SWAT.2026.12},
  annote =	{Keywords: Reachability Games, Strategy Repair, Strategic Reasoning, Automated Reasoning}
}
Document
View-Based Query Determinacy for Walk-Based Semantics

Authors: Nadime Francis

Published in: LIPIcs, Volume 365, 29th International Conference on Database Theory (ICDT 2026)


Abstract
The view-based query determinacy problem asks, given a view 𝒱 and a query Q whether the information contained in 𝒱 always suffices to answer the query Q. It is a notoriously hard problem that is known to be undecidable even in very restricted settings. Here, we study it in the context of graph databases and regular path queries and views evaluated under several "walk-based semantics", that is, semantics in which queries and views return the matched walks in full as opposed to the classical "endpoint semantics". Our main finding is that view-based query determinacy is decidable for regular path queries under both trail and shortest walk semantics.

Cite as

Nadime Francis. View-Based Query Determinacy for Walk-Based Semantics. In 29th International Conference on Database Theory (ICDT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 365, pp. 22:1-22:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{francis:LIPIcs.ICDT.2026.22,
  author =	{Francis, Nadime},
  title =	{{View-Based Query Determinacy for Walk-Based Semantics}},
  booktitle =	{29th International Conference on Database Theory (ICDT 2026)},
  pages =	{22:1--22:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-413-0},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{365},
  editor =	{ten Cate, Balder and Funk, Maurice},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2026.22},
  URN =		{urn:nbn:de:0030-drops-256362},
  doi =		{10.4230/LIPIcs.ICDT.2026.22},
  annote =	{Keywords: graph databases, regular path queries, trail semantics, shortest walk semantics, view-based query determinacy}
}
Document
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
Algebraic Characterizations of Classes of Regular Languages in DynFO

Authors: Corentin Barloy, Felix Tschirbs, Nils Vortmeier, and Thomas Zeume

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


Abstract
This paper explores the fine-grained structure of classes of regular languages maintainable in fragments of first-order logic within the dynamic descriptive complexity framework of Patnaik and Immerman. A result by Hesse states that the class of regular languages is maintainable by first-order formulas even if only unary auxiliary relations can be used. Another result by Gelade, Marquardt, and Schwentick states that the class of regular languages coincides with the class of languages maintainable by quantifier-free formulas with binary auxiliary relations. We refine Hesse’s result and show that with unary auxiliary data ∃^*∀^*-formulas can maintain all regular languages. We then obtain precise algebraic characterizations of the classes of languages maintainable with quantifier-free formulas and positive ∃^*-formulas in the presence of unary auxiliary relations.

Cite as

Corentin Barloy, Felix Tschirbs, Nils Vortmeier, and Thomas Zeume. Algebraic Characterizations of Classes of Regular Languages in DynFO. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{barloy_et_al:LIPIcs.STACS.2026.9,
  author =	{Barloy, Corentin and Tschirbs, Felix and Vortmeier, Nils and Zeume, Thomas},
  title =	{{Algebraic Characterizations of Classes of Regular Languages in DynFO}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{9:1--9:19},
  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.9},
  URN =		{urn:nbn:de:0030-drops-254986},
  doi =		{10.4230/LIPIcs.STACS.2026.9},
  annote =	{Keywords: Dynamic descriptive complexity, formal languages, monoid theory}
}
Document
Invited Paper
Inconsistency-Tolerant Semantics Based on (Preferred) Repairs (Invited Paper)

Authors: Camille Bourgaux

Published in: OASIcs, Volume 138, Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025)


Abstract
Real-world datasets are plagued by data quality issues which may render the data inconsistent w.r.t. a set of constraints, be they given by database integrity constraints or ontologies. A prominent way to handle such inconsistent data is to use inconsistency-tolerant semantics to obtain meaningful answers to queries. Most of these semantics are based on some notion of repairs, which represent ways of restoring the data consistency. The most basic kind of repairs is that of subset repairs, which are maximal consistent subsets of the dataset. However, in many scenarios, one can define preferred repairs based on some preference information. These lecture notes present inconsistency-tolerant semantics, focusing on the repair-based ones, then review different kinds of preferred repairs that have been considered in the literature. We present in particular the relationships between different kinds of preferred repairs and other notions related to inconsistency handling, the computational complexity of reasoning with (preferred) repairs, and some implementations.

Cite as

Camille Bourgaux. Inconsistency-Tolerant Semantics Based on (Preferred) Repairs (Invited Paper). In Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 & RW 2025). Open Access Series in Informatics (OASIcs), Volume 138, pp. 5:1-5:67, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{bourgaux:OASIcs.RW.2024/2025.5,
  author =	{Bourgaux, Camille},
  title =	{{Inconsistency-Tolerant Semantics Based on (Preferred) Repairs}},
  booktitle =	{Joint Proceedings of the 20th and 21st Reasoning Web Summer Schools (RW 2024 \& RW 2025)},
  pages =	{5:1--5:67},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-405-5},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{138},
  editor =	{Artale, Alessandro and Bienvenu, Meghyn and Garc{\'\i}a, Yazm{\'\i}n Ib\'{a}\~{n}ez and Murlak, Filip},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.RW.2024/2025.5},
  URN =		{urn:nbn:de:0030-drops-250504},
  doi =		{10.4230/OASIcs.RW.2024/2025.5},
  annote =	{Keywords: Knowledge bases, databases, inconsistency handling, repairs, preferences}
}
Document
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
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
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
Minimization of Deterministic Finite Automata Modulo the Edit Distance

Authors: Jakub Michaliszyn and Jan Otop

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


Abstract
We propose a novel approach to minimization of deterministic finite automata (DFA), in which the DFA is further minimized at the expense of relaxing equality of languages to merely a similarity. As the notion of similarity of languages, we consider the edit distance between languages ℒ, ℒ', i.e., the minimal number of edits necessary to transform any word from ℒ to some word from ℒ' and vice versa. In this paper we address two problems: minimization up to a predetermined edit distance given in the input, and minimization up to a bounded edit distance, in which there has to be an upper bound on the number of edits, but it is not specified. We show the first problem to be PSpace {}-complete and that the second problem is in Σ₂^p, and both NP-hard and coNP-hard. We show that if we limit how many strongly connected components can be visited by a single run (i.e., bounded SCC-depth), the problem becomes NP-complete. We also establish maximal subclasses of DFA over which minimization up to a bounded edit distance can be performed in polynomial time. Additionally, we provide a succinct overview of alternative metrics for assessing language similarity.

Cite as

Jakub Michaliszyn and Jan Otop. Minimization of Deterministic Finite Automata Modulo the Edit Distance. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 77:1-77:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{michaliszyn_et_al:LIPIcs.MFCS.2025.77,
  author =	{Michaliszyn, Jakub and Otop, Jan},
  title =	{{Minimization of Deterministic Finite Automata Modulo the Edit Distance}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{77:1--77:17},
  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.77},
  URN =		{urn:nbn:de:0030-drops-241843},
  doi =		{10.4230/LIPIcs.MFCS.2025.77},
  annote =	{Keywords: automata theory, automata minimization, edit distance}
}
Document
Characterizations of Fragments of Temporal Logic over Mazurkiewicz Traces

Authors: Bharat Adsul, Paul Gastin, and Shantanu Kulkarni

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


Abstract
We study fragments of temporal logics over Mazurkiewicz traces which are well known and established partial-order models of concurrent behaviours. We focus on concurrent versions of "strict past" and "strict future" modalities. Over words, the corresponding fragments have been shown to coincide with natural algebraic conditions on the recognizing monoids. We provide non-trivial generalizations of these classical results to traces. We exploit the local nature of the temporal modalities and obtain modular translations of specifications into asynchronous automata. More specifically, we provide novel characterizations of these fragments via local cascade products of a very simple two-state asynchronous automaton operating on a single process.

Cite as

Bharat Adsul, Paul Gastin, and Shantanu Kulkarni. Characterizations of Fragments of Temporal Logic over Mazurkiewicz Traces. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{adsul_et_al:LIPIcs.CONCUR.2025.5,
  author =	{Adsul, Bharat and Gastin, Paul and Kulkarni, Shantanu},
  title =	{{Characterizations of Fragments of Temporal Logic over Mazurkiewicz Traces}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{5:1--5:20},
  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.5},
  URN =		{urn:nbn:de:0030-drops-239551},
  doi =		{10.4230/LIPIcs.CONCUR.2025.5},
  annote =	{Keywords: Mazurkiewicz traces, temporal logics, asynchronous automata, cascade product, Green’s relations, algebraic automata theory}
}
Document
(Co)algebraic pearl
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
Higher-Dimensional Automata: Extension to Infinite Tracks

Authors: Luc Passemard, Amazigh Amrane, and Uli Fahrenberg

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


Abstract
We introduce higher-dimensional automata for infinite interval ipomsets (ω-HDAs). We define key concepts from different points of view, inspired from their finite counterparts. Then we explore languages recognized by ω-HDAs under Büchi and Muller semantics. We show that Muller acceptance is more expressive than Büchi acceptance and, in contrast to the finite case, both semantics do not yield languages closed under subsumption. Then, we adapt the original rational operations to deal with ω-HDAs and show that while languages of ω-HDAs are ω-rational, not all ω-rational languages can be expressed by ω-HDAs.

Cite as

Luc Passemard, Amazigh Amrane, and Uli Fahrenberg. Higher-Dimensional Automata: Extension to Infinite Tracks. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 31:1-31:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{passemard_et_al:LIPIcs.FSCD.2025.31,
  author =	{Passemard, Luc and Amrane, Amazigh and Fahrenberg, Uli},
  title =	{{Higher-Dimensional Automata: Extension to Infinite Tracks}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{31:1--31:23},
  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.31},
  URN =		{urn:nbn:de:0030-drops-236466},
  doi =		{10.4230/LIPIcs.FSCD.2025.31},
  annote =	{Keywords: Higher-dimensional automata, concurrency theory, omega pomsets, B\"{u}chi acceptance, Muller acceptance, interval pomsets, pomsets with interfaces}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Algebraic Language Theory with Effects

Authors: Fabian Lenke, Stefan Milius, Henning Urbat, and Thorsten Wißmann

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


Abstract
Regular languages - the languages accepted by deterministic finite automata - are known to be precisely the languages recognized by finite monoids. This characterization is the origin of algebraic language theory. In this paper, we generalize the correspondence between automata and monoids to automata with generic computational effects given by a monad, providing the foundations of an effectful algebraic language theory. We show that, under suitable conditions on the monad, a language is computable by an effectful automaton precisely when it is recognizable by (1) an effectful monoid morphism into an effect-free finite monoid, and (2) a monoid morphism into a monad-monoid bialgebra whose carrier is a finitely generated algebra for the monad, the former mode of recognition being conceptually completely new. Our prime application is a novel algebraic approach to languages computed by probabilistic finite automata. Additionally, we derive new algebraic characterizations for nondeterministic probabilistic finite automata and for weighted finite automata over unrestricted semirings, generalizing previous results on weighted algebraic recognition over commutative rings.

Cite as

Fabian Lenke, Stefan Milius, Henning Urbat, and Thorsten Wißmann. Algebraic Language Theory with Effects. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 165:1-165:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{lenke_et_al:LIPIcs.ICALP.2025.165,
  author =	{Lenke, Fabian and Milius, Stefan and Urbat, Henning and Wi{\ss}mann, Thorsten},
  title =	{{Algebraic Language Theory with Effects}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{165:1--165: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.165},
  URN =		{urn:nbn:de:0030-drops-235423},
  doi =		{10.4230/LIPIcs.ICALP.2025.165},
  annote =	{Keywords: Automaton, Monoid, Monad, Effect, Algebraic language theory}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
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
Saturation Problems for Families of Automata

Authors: León Bohn, Yong Li, Christof Löding, and Sven Schewe

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


Abstract
Families of deterministic finite automata (FDFA) represent regular ω-languages through their ultimately periodic words (UP-words). An FDFA accepts pairs of words, where the first component corresponds to a prefix of the UP-word, and the second component represents a period of that UP-word. An FDFA is termed saturated if, for each UP-word, either all or none of the pairs representing that UP-word are accepted. We demonstrate that determining whether a given FDFA is saturated can be accomplished in polynomial time, thus improving the known PSPACE upper bound by an exponential. We illustrate the application of this result by presenting the first polynomial learning algorithms for representations of the class of all regular ω-languages. Furthermore, we establish that deciding a weaker property, referred to as almost saturation, is PSPACE-complete. Since FDFAs do not necessarily define regular ω-languages when they are not saturated, we also address the regularity problem and show that it is PSPACE-complete. Finally, we explore a variant of FDFAs called families of deterministic weak automata (FDWA), where the semantics for the periodic part of the UP-word considers ω-words instead of finite words. We demonstrate that saturation for FDWAs is also decidable in polynomial time, that FDWAs always define regular ω-languages, and we compare the succinctness of these different models.

Cite as

León Bohn, Yong Li, Christof Löding, and Sven Schewe. Saturation Problems for Families of Automata. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 146:1-146:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{bohn_et_al:LIPIcs.ICALP.2025.146,
  author =	{Bohn, Le\'{o}n and Li, Yong and L\"{o}ding, Christof and Schewe, Sven},
  title =	{{Saturation Problems for Families of Automata}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{146:1--146: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.146},
  URN =		{urn:nbn:de:0030-drops-235239},
  doi =		{10.4230/LIPIcs.ICALP.2025.146},
  annote =	{Keywords: Families of Automata, automata learning, FDFAs}
}
  • Refine by Type
  • 35 Document/PDF
  • 20 Document/HTML

  • Refine by Publication Year
  • 4 2026
  • 16 2025
  • 1 2021
  • 3 2020
  • 1 2019
  • Show More...

  • Refine by Author
  • 7 Pin, Jean-Eric
  • 4 Kuperberg, Denis
  • 3 Selivanov, Victor
  • 3 Thomas, Wolfgang
  • 2 Amarilli, Antoine
  • Show More...

  • Refine by Series/Journal
  • 28 LIPIcs
  • 1 OASIcs
  • 1 DagRep
  • 2 DagSemRep
  • 3 DagSemProc

  • Refine by Classification
  • 7 Theory of computation → Formal languages and automata theory
  • 7 Theory of computation → Regular languages
  • 4 Theory of computation → Automata over infinite objects
  • 3 Theory of computation → Algebraic language theory
  • 2 Theory of computation → Logic and verification
  • Show More...

  • Refine by Keyword
  • 2 Automata theory
  • 2 Profinite topology
  • 2 Regular languages
  • 2 combinatorics
  • 2 complexity
  • 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