18 Search Results for "Zeitoun, Marc"

Document
DOI: 10.4230/LIPIcs.STACS.2026.9
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
DOI: 10.4230/LIPIcs.CSL.2026.45
Reasoning About Quality in Hyperproperties

Authors: Samuel Graepler, Benjamin Monmege, and Jean-Marc Talbot

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

Abstract
Hyperproperties allow one to specify properties of systems that inherently involve not single executions of the system, but several of them at once: observational determinism and non-inference are two examples of such properties used to study the security of systems. Logics like HyperLTL have been studied in the past to model check hyperproperties of systems. However, most of the time, requiring strict security properties is actually ineffective as systems do not meet such requirements. To overcome this issue, we introduce qualitative reasoning in HyperLTL, inspired by a similar work on LTL by Almagor, Boker and Kupferman [Almagor et al., 2016] where a formula has a value in the interval [0, 1], obtained by considering either a propositional quality (how much the specification is satisfied), or a temporal quality (when the specification is satisfied). We show decidability of the approximated model checking problem, as well as the model checking of large fragments.
Cite as

Samuel Graepler, Benjamin Monmege, and Jean-Marc Talbot. Reasoning About Quality in Hyperproperties. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 45:1-45:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{graepler_et_al:LIPIcs.CSL.2026.45,
  author =	{Graepler, Samuel and Monmege, Benjamin and Talbot, Jean-Marc},
  title =	{{Reasoning About Quality in Hyperproperties}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{45:1--45:18},
  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.45},
  URN =		{urn:nbn:de:0030-drops-254704},
  doi =		{10.4230/LIPIcs.CSL.2026.45},
  annote =	{Keywords: Hyperlogics, Automata-based model checking, Quantitative verification}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2025.2
Unboundedness Problems for Formal Languages (Invited Talk)

Authors: Georg Zetzsche

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

Abstract
Informally, unboundedness problems are decision problems that ask about the existence of infinitely many words (satisfying certain properties) in a formal language. For example: Is a given language infinite? Or: Does a given language have super-polynomial growth? These came into focus in recent years because of their connections to downward closure computation and separability problems. Although unboundedness problems may seem difficult at first, it turns out that there are techniques that are at the same time conceptually very simple, but also apply to a surprisingly wide variety of language classes. The talk will survey recent results (and techniques) concerning unboundedness problems.
Cite as

Georg Zetzsche. Unboundedness Problems for Formal Languages (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. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zetzsche:LIPIcs.FSTTCS.2025.2,
  author =	{Zetzsche, Georg},
  title =	{{Unboundedness Problems for Formal Languages}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{2:1--2:10},
  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.2},
  URN =		{urn:nbn:de:0030-drops-250810},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.2},
  annote =	{Keywords: Decidability, formal languages, unifying frameworks, downward closure, separability}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.5
Distributed Games with a Central Decision Maker

Authors: Bharat Adsul and Nehul Jain

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

Abstract
We study distributed games played on non-deterministic asynchronous automata which feature a central decision maker process that participates in all key decision making tasks. In these partial-information games, processes use their causal past to respond to scheduling choices made by the scheduler and cooperatively strategize as a team to achieve the winning objective. We show that the problem of deciding the existence of a distributed winning strategy is efficiently solvable for global safety and local parity objectives. We provide algorithmic solutions that match their computational hardness. We formulate the notion of a finite-state distributed strategy which allows to quantify its distributed memory requirements. For the aforementioned objectives, we establish that finite-state distributed winning strategies always exist. In fact, we provide novel constructions of such winning strategies which are shown to have almost optimal amount of distributed memory. We also show that a natural extension of the model with two decision making processes is undecidable.
Cite as

Bharat Adsul and Nehul Jain. Distributed Games with a Central Decision Maker. 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. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{adsul_et_al:LIPIcs.FSTTCS.2025.5,
  author =	{Adsul, Bharat and Jain, Nehul},
  title =	{{Distributed Games with a Central Decision Maker}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{5:1--5: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.5},
  URN =		{urn:nbn:de:0030-drops-250843},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.5},
  annote =	{Keywords: Mazurkiewicz traces, models of concurrency, distributed synthesis, game-theoretic models, asynchronous automata, distributed decision-making}
}
Document
DOI: 10.4230/LIPIcs.DISC.2025.12
Distributed Computation with Local Advice

Authors: Alkida Balliu, Sebastian Brandt, Fabian Kuhn, Krzysztof Nowicki, Dennis Olivetti, Eva Rotenberg, and Jukka Suomela

Published in: LIPIcs, Volume 356, 39th International Symposium on Distributed Computing (DISC 2025)

Abstract
Algorithms with advice have received ample attention in the distributed and online settings, and they have recently proven useful also in dynamic settings. In this work we study local computation with advice: the goal is to solve a graph problem Π with a distributed algorithm in T(Δ) communication rounds, for some function T that only depends on the maximum degree Δ of the graph, and the key question is how many bits of advice per node are needed. Some of our results regard Locally Checkable Labeling problems (LCLs), which is an important family of problems that includes various coloring and orientation problems on finite-degree graphs. These are constraint-satisfaction graph problems that can be defined with a finite set of valid input/output-labeled neighborhoods. Our main results are: 1) Any locally checkable labeling problem can be solved with only 1 bit of advice per node in graphs with sub-exponential growth (the number of nodes within radius r is sub-exponential in r; for example, grids are such graphs). Moreover, we can make the set of nodes that carry advice bits arbitrarily sparse. As a corollary, any locally checkable labeling problem admits a locally checkable proof with 1 bit per node in graphs with sub-exponential growth. 2) The assumption of sub-exponential growth is complemented by a conditional lower bound: assuming the Exponential-Time Hypothesis, there are locally checkable labeling problems that cannot be solved in general with any constant number of bits per node. 3) In any graph we can find an almost-balanced orientation (indegrees and outdegrees differ by at most one) with 1 bit of advice per node, and again we can make the advice arbitrarily sparse. As a corollary, we can also compress an arbitrary subset of edges so that a node of degree d stores only d/2 + 2 bits, and we can decompress it locally, in T(Δ) rounds. 4) In any graph of maximum degree Δ, we can find a Δ-coloring (if it exists) with 1 bit of advice per node, and again, we can make the advice arbitrarily sparse. 5) In any 3-colorable graph, we can find a 3-coloring with 1 bit of advice per node. As a corollary, in bounded-degree graphs there is a locally checkable proof that certifies 3-colorability with 1 bit of advice per node, while prior work shows that this is not possible with a proof labeling scheme (PLS), which is a more restricted setting where the verifier can only see up to distance 1. Our work shows that for many problems the key threshold is not whether we can achieve 1 bit of advice per node, but whether we can make the advice arbitrarily sparse. To formalize this idea, we develop a general framework of composable schemas that enables us to build algorithms for local computation with advice in a modular fashion: once we have (1) a schema for solving Π₁ and (2) a schema for solving Π₂ assuming an oracle for Π₁, we can also compose them and obtain (3) a schema that solves Π₂ without the oracle. It turns out that many natural problems admit composable schemas, all of them can be solved with only 1 bit of advice, and we can make the advice arbitrarily sparse.
Cite as

Alkida Balliu, Sebastian Brandt, Fabian Kuhn, Krzysztof Nowicki, Dennis Olivetti, Eva Rotenberg, and Jukka Suomela. Distributed Computation with Local Advice. In 39th International Symposium on Distributed Computing (DISC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 356, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{balliu_et_al:LIPIcs.DISC.2025.12,
  author =	{Balliu, Alkida and Brandt, Sebastian and Kuhn, Fabian and Nowicki, Krzysztof and Olivetti, Dennis and Rotenberg, Eva and Suomela, Jukka},
  title =	{{Distributed Computation with Local Advice}},
  booktitle =	{39th International Symposium on Distributed Computing (DISC 2025)},
  pages =	{12:1--12:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-402-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{356},
  editor =	{Kowalski, Dariusz R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2025.12},
  URN =		{urn:nbn:de:0030-drops-248295},
  doi =		{10.4230/LIPIcs.DISC.2025.12},
  annote =	{Keywords: Distributed graph algorithms, LOCAL model, computation with advice, locally checkable labeling problems, proof labeling schemes, locally checkable proofs, graph coloring, exponential-time hypothesis}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.TIME.2025.1
Interpolation and Separation Problems for Linear Temporal Logics (Invited Talk)

Authors: Michael Zakharyaschev

Published in: LIPIcs, Volume 355, 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)

Abstract
The talk gives a survey of recent results on two types of problems for linear temporal logics: one is related to the existence of a Craig interpolant for a given implication in a temporal logic, the other to the existence of a temporal query separating two given sets of temporal data instances.
Cite as

Michael Zakharyaschev. Interpolation and Separation Problems for Linear Temporal Logics (Invited Talk). In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zakharyaschev:LIPIcs.TIME.2025.1,
  author =	{Zakharyaschev, Michael},
  title =	{{Interpolation and Separation Problems for Linear Temporal Logics}},
  booktitle =	{32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-401-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{355},
  editor =	{Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.1},
  URN =		{urn:nbn:de:0030-drops-244473},
  doi =		{10.4230/LIPIcs.TIME.2025.1},
  annote =	{Keywords: Linear temporal logic, Craig interpolation, query-by-example}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.15
Certified Implementability of Global Multiparty Protocols

Authors: Elaine Li and Thomas Wies

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Implementability is the decision problem at the heart of top-down approaches to protocol verification. In this paper, we present a mechanization of a recently proposed precise implementability characterization by Li et al. for a large class of protocols that subsumes many existing formalisms in the literature. Our protocols and implementations model asynchronous commmunication, and can exhibit infinite behavior. We improve upon their pen-and-paper results by unifying distinct formalisms, simplifying existing proof arguments, elaborating on the construction of canonical implementations, and even uncovering a subtle bug in the semantics for infinite words. As a corollary of our mechanization, we show that the original characterization of implementability applies even to protocols with infinitely many participants. We also contribute a reusable library for reasoning about generic communicating state machines. Our mechanization consists of about 15k lines of Rocq code. We believe that our mechanization can provide the foundation for deductively proving the implementability of protocols beyond the reach of prior work, extracting certified implementations for finite protocols, and investigating implementability under alternative asynchronous communication models.
Cite as

Elaine Li and Thomas Wies. Certified Implementability of Global Multiparty Protocols. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 15:1-15:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.ITP.2025.15,
  author =	{Li, Elaine and Wies, Thomas},
  title =	{{Certified Implementability of Global Multiparty Protocols}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{15:1--15:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.15},
  URN =		{urn:nbn:de:0030-drops-246139},
  doi =		{10.4230/LIPIcs.ITP.2025.15},
  annote =	{Keywords: Asynchronous protocols, communicating state machines, labeled transition systems, infinite semantics, realizability, multiparty session types, choreographies, deadlock freedom}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.165
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
DOI: 10.4230/LIPIcs.STACS.2025.55
Modal Separation of Fixpoint Formulae

Authors: Jean Christoph Jung and Jędrzej Kołodziejski

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

Abstract
Modal separability for modal fixpoint formulae is the problem to decide for two given modal fixpoint formulae φ,φ' whether there is a modal formula ψ that separates them, in the sense that φ ⊧ ψ and ψ ⊧ ¬φ'. We study modal separability and its special case modal definability over various classes of models, such as arbitrary models, finite models, trees, and models of bounded outdegree. Our main results are that modal separability is PSpace-complete over words, that is, models of outdegree ≤ 1, ExpTime-complete over unrestricted and over binary models, and 2-ExpTime-complete over models of outdegree bounded by some d ≥ 3. Interestingly, this latter case behaves fundamentally different from the other cases also in that modal logic does not enjoy the Craig interpolation property over this class. Motivated by this we study also the induced interpolant existence problem as a special case of modal separability, and show that it is coNExpTime-complete and thus harder than validity in the logic. Besides deciding separability, we also investigate the problem of efficient construction of separators. Finally, we consider in a case study the extension of modal fixpoint formulae by graded modalities and investigate separability by modal formulae and graded modal formulae.
Cite as

Jean Christoph Jung and Jędrzej Kołodziejski. Modal Separation of Fixpoint Formulae. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 55:1-55:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{jung_et_al:LIPIcs.STACS.2025.55,
  author =	{Jung, Jean Christoph and Ko{\l}odziejski, J\k{e}drzej},
  title =	{{Modal Separation of Fixpoint Formulae}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{55:1--55:20},
  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.55},
  URN =		{urn:nbn:de:0030-drops-228804},
  doi =		{10.4230/LIPIcs.STACS.2025.55},
  annote =	{Keywords: Modal Logic, Fixpoint Logic, Separability, Interpolation}
}
Document
DOI: 10.4230/LIPIcs.CSL.2024.45
A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic

Authors: Thomas Place and Marc Zeitoun

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
We study an operator on classes of languages. For each class 𝒞, it produces a new class FO²(𝕀_𝒞) associated with a variant of two-variable first-order logic equipped with a signature 𝕀_𝒞 built from 𝒞. For 𝒞 = {∅, A*}, we obtain the usual FO²(<)} logic, equipped with linear order. For 𝒞 = {∅,{ε},A+,A*}, we get the variant FO²(<,+1), which also includes the successor predicate. If 𝒞 consists of all Boolean combinations of languages A*aA*, where a is a letter, we get the variant FO²(< ,Bet), which includes "between" relations. We prove a generic algebraic characterization of the classes FO^2(𝕀_𝒞). It elegantly generalizes those known for all the cases mentioned above. Moreover, it implies that if 𝒞 has decidable separation (plus some standard properties), then FO²2(𝕀_𝒞) has a decidable membership problem. We actually work with an equivalent definition of FO²(𝕀_𝒞) in terms of unary temporal logic. For each class 𝒞, we consider a variant TL(𝒞) of unary temporal logic whose future/past modalities depend on 𝒞 and such that TL(𝒞) = FO²(𝕀_𝒞). Finally, we also characterize FL(𝒞) and PL(𝒞), the pure-future and pure-past restrictions of TL(𝒞). Like for TL(𝒞), these characterizations imply that if 𝒞 is a class with decidable separation, then FL(𝒞) and PL(𝒞) have decidable membership.
Cite as

Thomas Place and Marc Zeitoun. A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 45:1-45:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{place_et_al:LIPIcs.CSL.2024.45,
  author =	{Place, Thomas and Zeitoun, Marc},
  title =	{{A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{45:1--45:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.45},
  URN =		{urn:nbn:de:0030-drops-196888},
  doi =		{10.4230/LIPIcs.CSL.2024.45},
  annote =	{Keywords: Classes of regular languages, Generalized unary temporal logic, Generalized two-variable first-order logic, Generic decidable characterizations, Membership, Separation}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2022.43
A Generic Polynomial Time Approach to Separation by First-Order Logic Without Quantifier Alternation

Authors: Thomas Place and Marc Zeitoun

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)

Abstract
We look at classes of languages associated to fragments of first-order logic BΣ₁, in which quantifier alternations are disallowed. Each such fragment is fully determined by choosing the set of predicates on positions that may be used. Equipping first-order logic with the linear ordering and possibly the successor relation as predicates yields two natural fragments, which were investigated by Simon and Knast, who proved that these two variants have decidable membership: "does an input regular language belong to the class ?". We extend their results in two orthogonal directions. - First, instead of membership, we explore the more general separation problem: decide if two regular languages can be separated by a language from the class under study. - Second, we use more general inputs: classes 𝒢 of group languages (i.e., recognized by a DFA in which each letter induces a permutation of the states) and extensions thereof, written 𝒢^+. We rely on a characterization of BΣ₁ by the operator BPol: given an input class 𝒞, it outputs a class BPol(𝒞) that corresponds to a variant of BΣ₁ equipped with special predicates associated to 𝒞. The classes BPol(𝒢) and BPol(𝒢^+) capture many natural variants of BΣ₁ which use predicates such as the linear ordering, the successor, the modular predicates or the alphabetic modular predicates. We show that separation is decidable for BPol(𝒢) and BPol(𝒢^+) when this is the case for 𝒢. This was already known for BPol(𝒢) and for two particular classes of the form BPol(𝒢^+). Yet, the algorithms were indirect and relied on involved frameworks, yielding poor upper complexity bounds. In contrast, our approach is direct. We work only with elementary concepts (mainly, finite automata). Our main contribution consists in polynomial time Turing reductions from both BPol(𝒢)- and BPol(𝒢^+)-separation to 𝒢-separation. This yields polynomial time algorithms for several key variants of BΣ₁, including those equipped with the linear ordering and possibly the successor and/or the modular predicates.
Cite as

Thomas Place and Marc Zeitoun. A Generic Polynomial Time Approach to Separation by First-Order Logic Without Quantifier Alternation. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 43:1-43:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{place_et_al:LIPIcs.FSTTCS.2022.43,
  author =	{Place, Thomas and Zeitoun, Marc},
  title =	{{A Generic Polynomial Time Approach to Separation by First-Order Logic Without Quantifier Alternation}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{43:1--43:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.43},
  URN =		{urn:nbn:de:0030-drops-174356},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.43},
  annote =	{Keywords: Automata, Separation, Covering, Concatenation hierarchies, Group languages}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2019.126
On All Things Star-Free (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Thomas Place and Marc Zeitoun

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
We investigate the star-free closure, which associates to a class of languages its closure under Boolean operations and marked concatenation. We prove that the star-free closure of any finite class and of any class of groups languages with decidable separation (plus mild additional properties) has decidable separation. We actually show decidability of a stronger property, called covering. This generalizes many results on the subject in a unified framework. A key ingredient is that star-free closure coincides with another closure operator where Kleene stars are also allowed in restricted contexts.
Cite as

Thomas Place and Marc Zeitoun. On All Things Star-Free (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 126:1-126:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{place_et_al:LIPIcs.ICALP.2019.126,
  author =	{Place, Thomas and Zeitoun, Marc},
  title =	{{On All Things Star-Free}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{126:1--126:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.126},
  URN =		{urn:nbn:de:0030-drops-107028},
  doi =		{10.4230/LIPIcs.ICALP.2019.126},
  annote =	{Keywords: Regular languages, separation problem, star-free closure, group languages}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2018.47
The Complexity of Separation for Levels in Concatenation Hierarchies

Authors: Thomas Place and Marc Zeitoun

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

Abstract
We investigate the complexity of the separation problem associated to classes of regular languages. For a class C, C-separation takes two regular languages as input and asks whether there exists a third language in C which includes the first and is disjoint from the second. First, in contrast with the situation for the classical membership problem, we prove that for most classes C, the complexity of C-separation does not depend on how the input languages are represented: it is the same for nondeterministic finite automata and monoid morphisms. Then, we investigate specific classes belonging to finitely based concatenation hierarchies. It was recently proved that the problem is always decidable for levels 1/2 and 1 of any such hierarchy (with inefficient algorithms). Here, we build on these results to show that when the alphabet is fixed, there are polynomial time algorithms for both levels. Finally, we investigate levels 3/2 and 2 of the famous Straubing-Thérien hierarchy. We show that separation is PSpace-complete for level 3/2 and between PSpace-hard and EXPTime for level 2.
Cite as

Thomas Place and Marc Zeitoun. The Complexity of Separation for Levels in Concatenation Hierarchies. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 47:1-47:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{place_et_al:LIPIcs.FSTTCS.2018.47,
  author =	{Place, Thomas and Zeitoun, Marc},
  title =	{{The Complexity of Separation for Levels in Concatenation Hierarchies}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{47:1--47:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.47},
  URN =		{urn:nbn:de:0030-drops-99463},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.47},
  annote =	{Keywords: Regular languages, separation, concatenation hierarchies, complexity}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2018.137
Separating Without Any Ambiguity

Authors: Thomas Place and Marc Zeitoun

Published in: LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)

Abstract
We investigate a standard operator on classes of languages: unambiguous polynomial closure. We show that if C is a class of regular languages having some mild properties, the membership problem for its unambiguous polynomial closure UPol(C) reduces to the same problem for C. We give a new, self-contained and elementary proof of this result. We also show that unambiguous polynomial closure coincides with alternating left and right deterministic closure. Finally, if additionally C is finite, we show that the separation and covering problems are decidable for UPol(C).
Cite as

Thomas Place and Marc Zeitoun. Separating Without Any Ambiguity. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 137:1-137:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{place_et_al:LIPIcs.ICALP.2018.137,
  author =	{Place, Thomas and Zeitoun, Marc},
  title =	{{Separating Without Any Ambiguity}},
  booktitle =	{45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)},
  pages =	{137:1--137:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-076-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{107},
  editor =	{Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.137},
  URN =		{urn:nbn:de:0030-drops-91419},
  doi =		{10.4230/LIPIcs.ICALP.2018.137},
  annote =	{Keywords: Regular languages, separation problem, decidable characterizations}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2016.77
The Covering Problem: A Unified Approach for Investigating the Expressive Power of Logics

Authors: Thomas Place and Marc Zeitoun

Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)

Abstract
An important endeavor in computer science is to precisely understand the expressive power of logical formalisms over discrete structures, such as words. Naturally, "understanding" is not a mathematical notion. Therefore, this investigation requires a concrete objective to capture such a notion. In the literature, the standard choice for this objective is the membership problem, whose aim is to find a procedure deciding whether an input regular language can be defined in the logic under study. This approach was cemented as the "right" one by the seminal work of Schuetzenberger, McNaughton and Papert on first-order logic and has been in use since then. However, membership questions are hard: for several important fragments, researchers have failed in this endeavor despite decades of investigation. In view of recent results on one of the most famous open questions, namely the quantifier alternation hierarchy of first-order logic, an explanation may be that membership is too restrictive as a setting. These new results were indeed obtained by considering more general problems than membership, taking advantage of the increased flexibility of the enriched mathematical setting. This opens a promising avenue of research and efforts have been devoted at identifying and solving such problems for natural fragments. However, until now, these problems have been ad hoc, most fragments relying on a specific one. A unique new problem replacing membership as the right one is still missing. The main contribution of this paper is a suitable candidate to play this role: the Covering Problem. We motivate this problem with three arguments. First, it admits an elementary set theoretic formulation, similar to membership. Second, we are able to reexplain or generalize all known results with this problem. Third, we develop a mathematical framework as well as a methodology tailored to the investigation of this problem.
Cite as

Thomas Place and Marc Zeitoun. The Covering Problem: A Unified Approach for Investigating the Expressive Power of Logics. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 77:1-77:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{place_et_al:LIPIcs.MFCS.2016.77,
  author =	{Place, Thomas and Zeitoun, Marc},
  title =	{{The Covering Problem: A Unified Approach for Investigating the Expressive Power of Logics}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{77:1--77:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.77},
  URN =		{urn:nbn:de:0030-drops-64857},
  doi =		{10.4230/LIPIcs.MFCS.2016.77},
  annote =	{Keywords: membership problem, separation problem, covering problem, regular languages, logics, decidable characterizations}
}
  • Refine by Type
  • 18 Document/PDF
  • 9 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 7 2025
  • 1 2024
  • 1 2022
  • 1 2019
  • Show More...

  • Refine by Author
  • 9 Zeitoun, Marc
  • 8 Place, Thomas
  • 1 Adsul, Bharat
  • 1 Balliu, Alkida
  • 1 Barloy, Corentin
  • Show More...

  • Refine by Series/Journal
  • 18 LIPIcs

  • Refine by Classification
  • 6 Theory of computation → Formal languages and automata theory
  • 4 Theory of computation → Regular languages
  • 2 Theory of computation → Distributed computing models
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Modal and temporal logics
  • Show More...

  • Refine by Keyword
  • 4 separation problem
  • 3 Regular languages
  • 3 Separation
  • 3 decidable characterizations
  • 2 Automata
  • 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