19 Search Results for "Endrullis, Jörg"

Volume

LIPIcs, Volume 326

33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

CSL 2025, February 10-14, 2025, Amsterdam, Netherlands

Editors: Jörg Endrullis and Sylvain Schmitz

Document
DOI: 10.4230/LIPIcs.STACS.2026.25
Homomorphism Indistinguishability, Multiplicity Automata Equivalence, and Polynomial Identity Testing

Authors: Marek Černý and Tim Seppelt

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

Abstract
Two graphs G and H are homomorphism indistinguishable over a graph class ℱ if they admit the same number of homomorphisms from every graph F ∈ ℱ. Many graph isomorphism relaxations such as (quantum) isomorphism and cospectrality can be characterised as homomorphism indistinguishability over specific graph classes. Thereby, the problems HomInd(ℱ) of deciding homomorphism indistinguishability over ℱ subsume diverse graph isomorphism relaxations whose complexities range from logspace to undecidable. Establishing the first general result on the complexity of HomInd(ℱ), Seppelt (MFCS 2024) showed that HomInd(ℱ) is in randomised polynomial time for every graph class ℱ of bounded treewidth that can be defined in counting monadic second-order logic CMSO₂. We show that this algorithm is conditionally optimal, i.e. it cannot be derandomised unless polynomial identity testing is in P. For CMSO₂-definable graph classes ℱ of bounded pathwidth, we improve the previous complexity upper bound for HomInd(ℱ) from P to C_ = L and show that this is tight. Secondarily, we establish a connection between homomorphism indistinguishability and multiplicity automata equivalence which allows us to pinpoint the complexity of the latter problem as C_ = L-complete.
Cite as

Marek Černý and Tim Seppelt. Homomorphism Indistinguishability, Multiplicity Automata Equivalence, and Polynomial Identity Testing. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{cerny_et_al:LIPIcs.STACS.2026.25,
  author =	{\v{C}ern\'{y}, Marek and Seppelt, Tim},
  title =	{{Homomorphism Indistinguishability, Multiplicity Automata Equivalence, and Polynomial Identity Testing}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{25:1--25:20},
  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.25},
  URN =		{urn:nbn:de:0030-drops-255144},
  doi =		{10.4230/LIPIcs.STACS.2026.25},
  annote =	{Keywords: treewidth, Courcelle’s theorem, logspace, multiplicity automata, polynomial identity testing}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.18
A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light

Authors: Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi

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

Abstract
We extend the existing HOL Light Library for Modal Systems (HOLMS) to support a modular implementation of modal reasoning within the HOL Light proof assistant. We deeply embed axiomatic calculi and relational semantics for seven normal modal logics (K, T, B, K4, S4, S5, GL) and formalise modal adequacy theorems for these systems. We then leverage those formalisations to implement a mechanism for automated reasoning via proof-search in the associated labelled sequent calculi, which we shallowly embed in HOL Light’s goal-stack mechanism. This way, we equip the general-purpose proof assistant with (semi)decision procedures for these logics that, in case of failure to construct a proof for the input formula, return a certified countermodel within the appropriate class for the logic under consideration. On the methodological side, we propose a precise measure of the modularity of our approach by systematically adopting Christopher Strachey’s distinction between ad hoc and parametric polymorphism throughout the library.
Cite as

Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi. A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 18:1-18:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bilotta_et_al:LIPIcs.CSL.2026.18,
  author =	{Bilotta, Antonella and Maggesi, Marco and Perini Brogi, Cosimo},
  title =	{{A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{18:1--18:29},
  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.18},
  URN =		{urn:nbn:de:0030-drops-254427},
  doi =		{10.4230/LIPIcs.CSL.2026.18},
  annote =	{Keywords: Modal logic, HOL Light, Labelled sequent calculi, Logical verification, Interactive theorem proving, Automated proof-search}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.20
On Left Adjoints Preserving Colimits in HoTT

Authors: Perry Hart

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

Abstract
We examine how the standard proof that left adjoints preserve colimits behaves in the setting of wild categories, a natural setting for synthetic homotopy theory inside homotopy type theory. We prove that the proof may fail for adjunctions between wild categories. Our core contribution, however, is a sufficient condition on the left adjoint for the proof to go through. The condition, called 2-coherence, expresses that the naturality structure of the hom-isomorphism commutes with composition of morphisms. We present two useful examples of this condition in action. First, we use it, along with a new version of a known trick for homogeneous types, to show that the suspension functor preserves graph-indexed colimits. Second, we show that every modality, viewed as a functor on coslices of a type universe, is 2-coherent as a left adjoint to the forgetful functor from the subcategory of modal types, thereby proving this subcategory is cocomplete. We have formalized our main results in Agda.
Cite as

Perry Hart. On Left Adjoints Preserving Colimits in HoTT. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 20:1-20:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{hart:LIPIcs.CSL.2026.20,
  author =	{Hart, Perry},
  title =	{{On Left Adjoints Preserving Colimits in HoTT}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{20:1--20:17},
  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.20},
  URN =		{urn:nbn:de:0030-drops-254442},
  doi =		{10.4230/LIPIcs.CSL.2026.20},
  annote =	{Keywords: wild categories, colimits, adjunctions, homotopy type theory, category theory, synthetic homotopy theory, higher inductive types, modalities}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.13
Barendregt’s Theory of the λ-Calculus, Refreshed and Formalized

Authors: Adrienne Lancelot, Beniamino Accattoli, and Maxime Vemclefs

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

Abstract
Barendregt’s book on the untyped λ-calculus refines the inconsistent view of β-divergence as representation of the undefined via the key concept of head reduction. In this paper, we put together recent revisitations of some key theorems laid out in Barendregt’s book, and we formalize them in the Abella proof assistant. Our work provides a compact and refreshed presentation of the core of the book. The formalization faithfully mimics pen-and-paper proofs. Two interesting aspects are the manipulation of contexts for the study of contextual equivalence and a formal alternative to the informal trick at work in Takahashi’s proof of the genericity lemma. As a by-product, we obtain an alternative definition of contextual equivalence that does not mention contexts.
Cite as

Adrienne Lancelot, Beniamino Accattoli, and Maxime Vemclefs. Barendregt’s Theory of the λ-Calculus, Refreshed and Formalized. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lancelot_et_al:LIPIcs.ITP.2025.13,
  author =	{Lancelot, Adrienne and Accattoli, Beniamino and Vemclefs, Maxime},
  title =	{{Barendregt’s Theory of the \lambda-Calculus, Refreshed and Formalized}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{13:1--13:22},
  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.13},
  URN =		{urn:nbn:de:0030-drops-246114},
  doi =		{10.4230/LIPIcs.ITP.2025.13},
  annote =	{Keywords: lambda-calculus, head reduction, equational theory}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2025.12
Cancellative Convex Semilattices

Authors: Ana Sokolova and Harald Woracek

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

Abstract
Convex semilattices are algebras that are at the same time a convex algebra and a semilattice, together with a distributivity axiom. These algebras have attracted some attention in the last years as suitable algebras for probability and nondeterminism, in particular by being the Eilenberg-Moore algebras of the nonempty finitely-generated convex subsets of the distributions monad. A convex semilattice is cancellative if the underlying convex algebra is cancellative. Cancellative convex algebras have been characterized by M. H. Stone and by H. Kneser: A convex algebra is cancellative if and only if it is isomorphic to a convex subset of a vector space (with canonical convex algebra operations). We prove an analogous theorem for convex semilattices: A convex semilattice is cancellative if and only if it is isomorphic to a convex subset of a Riesz space, i.e., a lattice-ordered vector space (with canonical convex semilattice operations).
Cite as

Ana Sokolova and Harald Woracek. Cancellative Convex Semilattices. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{sokolova_et_al:LIPIcs.CALCO.2025.12,
  author =	{Sokolova, Ana and Woracek, Harald},
  title =	{{Cancellative Convex Semilattices}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{12:1--12:15},
  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.12},
  URN =		{urn:nbn:de:0030-drops-235714},
  doi =		{10.4230/LIPIcs.CALCO.2025.12},
  annote =	{Keywords: convex semilattice, cancellativity, Riesz space}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.12
Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!

Authors: Rémy Cerda, Giulio Manzonetto, and Alexis Saurin

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

Abstract
Although the λI-calculus is a natural fragment of the λ-calculus, obtained by forbidding the erasure, its equational theories did not receive much attention. The reason is that all proper denotational models studied in the literature equate all non-normalizable λI-terms, whence the associated theory is not very informative. The goal of this paper is to introduce a previously unknown theory of the λI-calculus, induced by a notion of evaluation trees that we call "Ohana trees". The Ohana tree of a λI-term is an annotated version of its Böhm tree, remembering all free variables that are hidden within its meaningless subtrees, or pushed into infinity along its infinite branches. We develop the associated theories of program approximation: the first approach - more classic - is based on finite trees and continuity, the second adapts Ehrhard and Regnier’s Taylor expansion. We then prove a Commutation Theorem stating that the normal form of the Taylor expansion of a λI-term coincides with the Taylor expansion of its Ohana tree. As a corollary, we obtain that the equality induced by Ohana trees is compatible with abstraction and application. We conclude by discussing the cases of Lévy-Longo and Berarducci trees, and generalizations to the full λ-calculus.
Cite as

Rémy Cerda, Giulio Manzonetto, and Alexis Saurin. Ohana Trees and Taylor Expansion for the λI-Calculus: No variable gets left behind or forgotten!. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cerda_et_al:LIPIcs.FSCD.2025.12,
  author =	{Cerda, R\'{e}my and Manzonetto, Giulio and Saurin, Alexis},
  title =	{{Ohana Trees and Taylor Expansion for the \lambdaI-Calculus: No variable gets left behind or forgotten!}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{12:1--12:20},
  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.12},
  URN =		{urn:nbn:de:0030-drops-236277},
  doi =		{10.4230/LIPIcs.FSCD.2025.12},
  annote =	{Keywords: \lambda-calculus, program approximation, Taylor expansion, \lambdaI-calculus, persistent free variables, B\"{o}hm trees, Ohana trees}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.25
Completeness of the Decreasing Diagrams Method for Proving Confluence of Rewriting Systems of the Least Uncountable Cardinality

Authors: Ievgen Ivanov

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

Abstract
We show that every confluent abstract rewriting system (ARS) of the cardinality that does not exceed the first uncountable cardinal belongs to the class DCR₃, i.e. the class of confluent ARS for which confluence can be proved with the the help of the decreasing diagrams method using the set of labels {0,1,2} ordered in such a way that 0<1<2 (in the general case, the decreasing diagrams method with two labels is not sufficient for proving confluence of such ARS). Under the Continuum Hypothesis this result implies that the decreasing diagrams method is sufficient for establishing confluence of ARS on many structures of interest to applied mathematics and various interdisciplinary fields (confluence of ARS on real numbers, continuous real functions, etc.). We provide a machine-checked formal proof of a formalized version of the main result in Isabelle proof assistant using HOL logic and the HOL-Cardinals theory. An extended version of this formalization is available in the Archive of Formal Proofs.
Cite as

Ievgen Ivanov. Completeness of the Decreasing Diagrams Method for Proving Confluence of Rewriting Systems of the Least Uncountable Cardinality. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 25:1-25:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ivanov:LIPIcs.FSCD.2025.25,
  author =	{Ivanov, Ievgen},
  title =	{{Completeness of the Decreasing Diagrams Method for Proving Confluence of Rewriting Systems of the Least Uncountable Cardinality}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{25:1--25:20},
  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.25},
  URN =		{urn:nbn:de:0030-drops-236404},
  doi =		{10.4230/LIPIcs.FSCD.2025.25},
  annote =	{Keywords: confluence, decreasing diagrams method, rewriting systems, reduction, formal methods, formal proofs, formal verification, non-discrete models, nondeterministic models, interval models}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.8
The Parameterized Complexity of Learning Monadic Second-Order Logic

Authors: Steffen van Bergerem, Martin Grohe, and Nina Runde

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Within the model-theoretic framework for supervised learning introduced by Grohe and Turán (TOCS 2004), we study the parameterized complexity of learning concepts definable in monadic second-order logic (MSO). We show that the problem of learning an MSO-definable concept from a training sequence of labeled examples is fixed-parameter tractable on graphs of bounded clique-width, and that it is hard for the parameterized complexity class para-NP on general graphs. It turns out that an important distinction to be made is between 1-dimensional and higher-dimensional concepts, where the instances of a k-dimensional concept are k-tuples of vertices of a graph. For the higher-dimensional case, we give a learning algorithm that is fixed-parameter tractable in the size of the graph, but not in the size of the training sequence, and we give a hardness result showing that this is optimal. By comparison, in the 1-dimensional case, we obtain an algorithm that is fixed-parameter tractable in both.
Cite as

Steffen van Bergerem, Martin Grohe, and Nina Runde. The Parameterized Complexity of Learning Monadic Second-Order Logic. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanbergerem_et_al:LIPIcs.CSL.2025.8,
  author =	{van Bergerem, Steffen and Grohe, Martin and Runde, Nina},
  title =	{{The Parameterized Complexity of Learning Monadic Second-Order Logic}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{8:1--8:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.8},
  URN =		{urn:nbn:de:0030-drops-227651},
  doi =		{10.4230/LIPIcs.CSL.2025.8},
  annote =	{Keywords: monadic second-order definable concept learning, agnostic probably approximately correct learning, parameterized complexity, clique-width, fixed-parameter tractable, Boolean classification, supervised learning, monadic second-order logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.12
First-Order Logic with Equicardinality in Random Graphs

Authors: Simi Haber, Tal Hershko, Mostafa Mirabi, and Saharon Shelah

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We answer a question of Blass and Harary about the validity of the zero-one law in random graphs for extensions of first-order logic (FOL). For a given graph property P, the Lindström extension of FOL by P is defined as the minimal (regular) extension of FOL able to express P. For several graph properties P (e.g. Hamiltonicity), it is known that the Lindström extension by P is also able to interpret a segment of arithmetic, and thus strongly disobeys the zero-one law. Common to all these properties is the ability to express the Härtig quantifier, a natural extension of FOL testing if two definable sets are of the same size. We prove that the Härtig quantifier is sufficient for the interpretation of arithmetic, thus providing a general result which implies all known cases of Lindström extensions which are able to interpret a segment of arithmetic.
Cite as

Simi Haber, Tal Hershko, Mostafa Mirabi, and Saharon Shelah. First-Order Logic with Equicardinality in Random Graphs. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{haber_et_al:LIPIcs.CSL.2025.12,
  author =	{Haber, Simi and Hershko, Tal and Mirabi, Mostafa and Shelah, Saharon},
  title =	{{First-Order Logic with Equicardinality in Random Graphs}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.12},
  URN =		{urn:nbn:de:0030-drops-227694},
  doi =		{10.4230/LIPIcs.CSL.2025.12},
  annote =	{Keywords: finite model theory, first-order logic, monadic second-order logic, random graphs, zero-one laws, generalized quantifiers, equicardinality}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.16
Undefinability of Approximation of 2-To-2 Games

Authors: Anuj Dawar and Bálint Molnár

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Recent work by Atserias and Dawar [Albert Atserias and Anuj Dawar, 2019] and Tucker-Foltz [Jamie Tucker-Foltz, 2024] has established undefinability results in fixed-point logic with counting (FPC) corresponding to many classical complexity results from the hardness of approximation. In this line of work, NP-hardness results are turned into unconditional FPC undefinability results. We extend this work by showing the FPC undefinability of any constant factor approximation of weighted 2-to-2 games, based on the NP-hardness results of Khot, Minzer and Safra. Our result shows that the completely satisfiable 2-to-2 games are not FPC-separable from those that are not ε-satisfiable, for arbitrarily small ε. The perfect completeness of our inseparability is an improvement on the complexity result, as the NP-hardness of such a separation is still only conjectured. This perfect completeness enables us to show the FPC undefinability of other problems whose NP-hardness is conjectured. In particular, we are able to show that no FPC formula can separate the 3-colourable graphs from those that are not t-colourable, for any constant t.
Cite as

Anuj Dawar and Bálint Molnár. Undefinability of Approximation of 2-To-2 Games. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 16:1-16:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dawar_et_al:LIPIcs.CSL.2025.16,
  author =	{Dawar, Anuj and Moln\'{a}r, B\'{a}lint},
  title =	{{Undefinability of Approximation of 2-To-2 Games}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{16:1--16:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.16},
  URN =		{urn:nbn:de:0030-drops-227735},
  doi =		{10.4230/LIPIcs.CSL.2025.16},
  annote =	{Keywords: Hardness of Approximation, Unique Games, Descriptive Complexity, Fixed-Point Logic with Counting}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CSL.2025
LIPIcs, Volume 326, CSL 2025, Complete Volume

Authors: Jörg Endrullis and Sylvain Schmitz

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
LIPIcs, Volume 326, CSL 2025, Complete Volume
Cite as

33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 1-988, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Proceedings{endrullis_et_al:LIPIcs.CSL.2025,
  title =	{{LIPIcs, Volume 326, CSL 2025, Complete Volume}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{1--988},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025},
  URN =		{urn:nbn:de:0030-drops-228130},
  doi =		{10.4230/LIPIcs.CSL.2025},
  annote =	{Keywords: LIPIcs, Volume 326, CSL 2025, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CSL.2025.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Jörg Endrullis and Sylvain Schmitz

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{endrullis_et_al:LIPIcs.CSL.2025.0,
  author =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{0:i--0:xiv},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.0},
  URN =		{urn:nbn:de:0030-drops-228128},
  doi =		{10.4230/LIPIcs.CSL.2025.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.26
The Complexity of Deciding Characteristic Formulae in Van Glabbeek’s Branching-Time Spectrum

Authors: Luca Aceto, Antonis Achilleos, Aggeliki Chalki, and Anna Ingólfsdóttir

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Characteristic formulae give a complete logical description of the behaviour of processes modulo some chosen notion of behavioural semantics. They allow one to reduce equivalence or preorder checking to model checking, and are exactly the formulae in the modal logics characterizing classic behavioural equivalences and preorders for which model checking can be reduced to equivalence or preorder checking. This paper studies the complexity of determining whether a formula is characteristic for some process in each of the logics providing modal characterizations of the simulation-based semantics in van Glabbeek’s branching-time spectrum. Since characteristic formulae in each of those logics are exactly the satisfiable and prime ones, this article presents complexity results for the satisfiability and primality problems, and investigates the boundary between modal logics for which those problems can be solved in polynomial time and those for which they become computationally hard. Amongst other contributions, this article also studies the complexity of constructing characteristic formulae in the modal logics characterizing simulation-based semantics, both when such formulae are presented in explicit form and via systems of equations.
Cite as

Luca Aceto, Antonis Achilleos, Aggeliki Chalki, and Anna Ingólfsdóttir. The Complexity of Deciding Characteristic Formulae in Van Glabbeek’s Branching-Time Spectrum. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CSL.2025.26,
  author =	{Aceto, Luca and Achilleos, Antonis and Chalki, Aggeliki and Ing\'{o}lfsd\'{o}ttir, Anna},
  title =	{{The Complexity of Deciding Characteristic Formulae in Van Glabbeek’s Branching-Time Spectrum}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{26:1--26:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.26},
  URN =		{urn:nbn:de:0030-drops-227836},
  doi =		{10.4230/LIPIcs.CSL.2025.26},
  annote =	{Keywords: Characteristic formulae, prime formulae, bisimulation, simulation relations, modal logics, complexity theory, satisfiability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.23
Permissive Equilibria in Multiplayer Reachability Games

Authors: Aline Goeminne and Benjamin Monmege

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We study multi-strategies in multiplayer reachability games played on finite graphs. A multi-strategy prescribes a set of possible actions, instead of a single action as usual strategies: it represents a set of all strategies that are consistent with it. We aim for profiles of multi-strategies (a multi-strategy per player), where each profile of consistent strategies is a Nash equilibrium, or a subgame perfect equilibrium. The permissiveness of two multi-strategies can be compared with penalties, as already used in the two-player zero-sum setting by Bouyer, Duflot, Markey and Renault [Patricia Bouyer et al., 2009]. We show that we can decide the existence of a multi-strategy profile that is a Nash equilibrium or a subgame perfect equilibrium, while satisfying some upper-bound constraints on the penalties in PSPACE, if the upper-bound penalties are given in unary. The same holds when we search for multi-strategies where certain players are asked to win in at least one play or in all plays.
Cite as

Aline Goeminne and Benjamin Monmege. Permissive Equilibria in Multiplayer Reachability Games. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{goeminne_et_al:LIPIcs.CSL.2025.23,
  author =	{Goeminne, Aline and Monmege, Benjamin},
  title =	{{Permissive Equilibria in Multiplayer Reachability Games}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.23},
  URN =		{urn:nbn:de:0030-drops-227801},
  doi =		{10.4230/LIPIcs.CSL.2025.23},
  annote =	{Keywords: multiplayer reachability games, penalties, permissive equilibria}
}
  • Refine by Type
  • 18 Document/PDF
  • 12 Document/HTML
  • 1 Volume

  • Refine by Publication Year
  • 3 2026
  • 12 2025
  • 1 2018
  • 2 2015
  • 1 2013

  • Refine by Author
  • 6 Endrullis, Jörg
  • 2 Polonsky, Andrew
  • 2 Schmitz, Sylvain
  • 1 Accattoli, Beniamino
  • 1 Aceto, Luca
  • Show More...

  • Refine by Series/Journal
  • 18 LIPIcs

  • Refine by Classification
  • 4 Theory of computation → Logic and verification
  • 3 Theory of computation → Complexity theory and logic
  • 3 Theory of computation → Finite Model Theory
  • 3 Theory of computation → Logic
  • 2 Theory of computation → Equational logic and rewriting
  • Show More...

  • Refine by Keyword
  • 2 coinduction
  • 2 confluence
  • 2 infinitary rewriting
  • 2 monadic second-order logic
  • 1 Automated proof-search
  • 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