Volume
LIPIcs, Volume 326
33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL)
Event
CSL 2025, February 10-14, 2025, Amsterdam, NetherlandsEditors
Publication Details
- published at: 2025-02-03
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-362-1
- DBLP: db/conf/csl/csl2025
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 326, CSL 2025, Complete Volume
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
Front Matter, Table of Contents, Preface, Conference Organization
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
Ackermann Award
The Ackermann Award 2024
Abstract
Report on the 2024 Ackermann Award.
Cite as
Maribel Fernández and Prakash Panangaden. The Ackermann Award 2024. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 1:1-1:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{fernandez_et_al:LIPIcs.CSL.2025.1,
author = {Fern\'{a}ndez, Maribel and Panangaden, Prakash},
title = {{The Ackermann Award 2024}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {1:1--1:5},
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.1},
URN = {urn:nbn:de:0030-drops-227581},
doi = {10.4230/LIPIcs.CSL.2025.1},
annote = {Keywords: finite automaton, string transducer, class membership problem, first-order logic, preservation theorem, finite model theory}
}
Document
Invited Talk
On the Probabilistic and Statistical Verification of Infinite Markov Chains (Invited Talk)
Abstract
The verification of infinite-state Markov chains is a challenging problem, even when those chains are described by structured high-level models. In 2007, Abdulla et al introduced the concept of decisiveness [Abdulla et al., 2007], and showed that a natural approximation scheme could be applied to infinite Markov chains that are decisive. This was, up to our knowledge, the unique generic scheme that could be widely applied to (decisive) infinite Markov chains providing guarantees on the computed values (under some mild assumptions for effectiveness). On the other hand, statistical model-checking is a very efficient method that can be used for estimating probabilities in stochastic systems [Younes and Simmons, 2006; H. L. S. Younes et al., 2010]. We explain in this talk that decisiveness is also a key concept that allows to apply such statistical methods to infinite Markov chains.
While decisiveness is a crucial property, not all Markov chains are decisive, and it is therefore desirable to propose methods to analyze non-decisive Markov chains. Importance sampling [Kahn and Harris, 1951] is a method which has been proposed to improve efficiency of statistical model-checking, in particular for estimating probabilities of rare events in stochastic systems. The idea is to biase the original chain, and to estimate the probabilities in the biased chain; guarantees can sometimes be given, as studied for instance in [B. Barbot et al., 2012].
In this talk, we will explain how we use the importance sampling idea to turn a non-decisive Markov chain into a biased decisive Markov chain, in which we can estimate probabilities (with guarantees). We apply the general approach to a class of probabilistic pushdown automata. Our algorithms have been implemented in the tool Cosmos [P. Ballarini et al., 2015], and we discuss the methodology for experiments as well as our (partial) conclusions.
Cite as
Patricia Bouyer. On the Probabilistic and Statistical Verification of Infinite Markov Chains (Invited Talk). In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bouyer:LIPIcs.CSL.2025.2,
author = {Bouyer, Patricia},
title = {{On the Probabilistic and Statistical Verification of Infinite Markov Chains}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {2:1--2:2},
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.2},
URN = {urn:nbn:de:0030-drops-227590},
doi = {10.4230/LIPIcs.CSL.2025.2},
annote = {Keywords: Markov Chains, Infinite state systems, Numerical and statistical Vverification}
}
Document
Invited Talk
Synthetic Mathematics for the Mechanisation of Computability Theory and Logic (Invited Talk)
Abstract
Mathematical practice in most areas of mathematics is based on the assumption that proofs could be made fully formal in a chosen foundation in principle. This assumption is backed by partial attempts at formalisation and by full mechanisation of various areas of mathematics in various proof assistants and various foundations. Areas that have been largely neglected for computer-assisted and machine-checked proofs are computability theory and logic: Fundamental results like Gödel’s second incompleteness theorem in its stronger forms due to Kleene and Rosser, Löb’s theorem, Post’s theorem connecting the arithmetical hierarchy and Turing jumps, or the Friedberg-Muĉnik theorem solving Post’s problem have not or only very recently been re-produced in proof assistants. This is due to the fact that making these arguments formal is several orders of magnitude more involved than formalising other areas of mathematics, due to the amount of invisible mathematics (a term coined by Andrej Bauer) involved.
In computability theory, invisible arguments occur mainly behind proofs that a certain intuitively sketched procedure is computable in - citing Emil Post - "forbidding, diverse and alien formalisms in which this [...] work of Gödel, Church, Turing, Kleene, Rosser [...] is embodied.". For instance, there have been various approaches of formalising Turing machines, all to the ultimate dissatisfaction of the respective authors, and none going further than constructing a universal machine and proving the halting problem undecidable. Professional computability theorist and teachers of computability theory thus rely on the informal Church Turing thesis to carry out their work and only argue the computability of described algorithms informally.
For computability theory, a way out was proposed in the 1980s by Fred Richman and developed during the last decade by Andrej Bauer: Synthetic computability theory, where one assumes axioms in a constructive foundation which essentially identify all (constructively definable) functions with computable functions. A drawback of the approach is that assuming such an axiom on top of the axiom of countable choice - which is routinely assumed in this branch of constructive mathematics and computable analysis - is that the law of excluded middle, i.e. classical logic, becomes invalid. Computability theory is however, as all mainstream branches of mathematics, making routine use of the axiom of excluded middle.
In the case of logic, the invisible mathematics usually is either centered around encoding formulas and proofs as numbers using Gödel or similar encodings or about provability arguments that certain results can be proved in restricted proof systems such as Peano arithmetic. In several settings, synthetic computability arguments can be employed to mechanise these proofs.
We observe that a slight foundational shift rectifies the situation: By basing synthetic computability theory in the Calculus of Inductive Constructions, the type theory underlying amongst others the Coq and Lean proof assistants, where countable choice is independent and thus not provable, axioms for synthetic computability are compatible with the law of excluded middle. This insight can be used to finally mechanise computability theory and logic, in an elegant, concise way where invisible arguments stay invisible: with Felix Jahn I have mechanised arguments related to many-one and truth-table reduction theory (published at CSL '23), Dominik Kirst and Benjamin Peters have presented Gödel’s first incompleteness theorem in this style (at CSL '23), and in collaboration with Dominik Kirst and Niklas Mück I have given a proof of Post’s hierarchy theorem (at CSL '24).
In this invited talk, I will give a broader overview of this line of research investigating a mechanised synthetic approach to logic and computability theory. In particular, I will discuss a Coq library of undecidability proofs, results in the theory of reducibility degrees, constructive reverse analysis of theorems, as well as generalised incompleteness results such as Löb’s theorem.
Cite as
Yannick Forster. Synthetic Mathematics for the Mechanisation of Computability Theory and Logic (Invited Talk). In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{forster:LIPIcs.CSL.2025.3,
author = {Forster, Yannick},
title = {{Synthetic Mathematics for the Mechanisation of Computability Theory and Logic}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {3:1--3:2},
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.3},
URN = {urn:nbn:de:0030-drops-227603},
doi = {10.4230/LIPIcs.CSL.2025.3},
annote = {Keywords: Synthetic mathematics, computability theory, logic}
}
Document
Invited Talk
Playing with Modalities (Invited Talk)
Abstract
In this work, we will explore modalities through dialogical game lenses. Games provide a powerful tool for bridging the gap between intended and formal semantics, often offering a more conceptually natural approach to logic than traditional model-theoretic semantics.
We begin by exploring substructural calculi from a game semantic perspective, driven by intuitions about resource-consciousness and, more specifically, cost-sensitive reasoning. The game comes into full swing as we introduce cost labels to assumptions and a corresponding budget. Different proofs of the same end-sequent are interpreted as strategies for a player to defend a claim, which vary in cost. This leads to a labelled calculus, which can be viewed as a fragment of subexponential linear logic. We conclude this first part with a discussion of cut-admissibility for the proposed system.
In the second part, we show that our games offer an interesting insight also into modal logics. More precisely, we will focus on the modal logic PNL, characterised by Kripke frames with two types of disjoint and symmetric reachability relations. This framework is motivated by the study of group polarisation, where the opinions or beliefs of individuals within a group become more extreme or polarised after interaction. Our approach to reasoning about group polarisation is based on PNL and highlights a different aspect of formal reasoning about the corresponding models - using games and proof systems. We conclude by outlining potential directions for future research.
Cite as
Elaine Pimentel, Carlos Olarte, Timo Lang, Robert Freiman, and Christian G. Fermüller. Playing with Modalities (Invited Talk). In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 4:1-4:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{pimentel_et_al:LIPIcs.CSL.2025.4,
author = {Pimentel, Elaine and Olarte, Carlos and Lang, Timo and Freiman, Robert and Ferm\"{u}ller, Christian G.},
title = {{Playing with Modalities}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {4:1--4:20},
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.4},
URN = {urn:nbn:de:0030-drops-227614},
doi = {10.4230/LIPIcs.CSL.2025.4},
annote = {Keywords: Linear logic, modal logic, proof theory, game semantics}
}
Document
Invited Talk
Modal Automata: Analysing Modal Fixpoint Logics, One Step at a Time (Invited Talk)
Abstract
We present and investigate a general framework for studying modal fixpoint logics and some related versions of monadic second-order logic, by means of certain finite automata that operate on Kripke structures. Characteristic of these modal automata is that the co-domain of their transition function is a set of formulas of a so-called one-step logic. The motivation for taking this perspective is that if a logic is characterised by a class of modal automata, many of its properties are already determined at the level of the much simpler one-step logic.
Cite as
Yde Venema. Modal Automata: Analysing Modal Fixpoint Logics, One Step at a Time (Invited Talk). In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 5:1-5:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{venema:LIPIcs.CSL.2025.5,
author = {Venema, Yde},
title = {{Modal Automata: Analysing Modal Fixpoint Logics, One Step at a Time}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {5:1--5:5},
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.5},
URN = {urn:nbn:de:0030-drops-227627},
doi = {10.4230/LIPIcs.CSL.2025.5},
annote = {Keywords: modal logic, parity automata, fixpoint logic, one-step logic}
}
Document
Equi-Rank Homomorphism Preservation Theorem on Finite Structures
Abstract
The Homomorphism Preservation Theorem (HPT) of classical model theory states that a first-order sentence is preserved under homomorphisms if, and only if, it is equivalent to an existential-positive sentence. This theorem remains valid when restricted to finite structures, as demonstrated by the author in [Rossman, 2008; Rossman, 2017] via distinct model-theoretic and circuit-complexity based proofs. In this paper, we present a third (and significantly simpler) proof of the finitary HPT based on a generalized Cai-Fürer-Immerman construction. This method establishes a tight correspondence between syntactic parameters of a homomorphism-preserved sentence (quantifier rank, variable width, alternation height) and structural parameters of its minimal models (tree-width, tree-depth, decomposition height). Consequently, we prove a conjectured "equi-rank" version of the finitary HPT. In contrast, previous versions of the finitary HPT possess additional properties, but incur blow-ups in the quantifier rank of the equivalent existential-positive sentence.
Cite as
Benjamin Rossman. Equi-Rank Homomorphism Preservation Theorem on Finite Structures. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{rossman:LIPIcs.CSL.2025.6,
author = {Rossman, Benjamin},
title = {{Equi-Rank Homomorphism Preservation Theorem on Finite Structures}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {6:1--6: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.6},
URN = {urn:nbn:de:0030-drops-227634},
doi = {10.4230/LIPIcs.CSL.2025.6},
annote = {Keywords: finite model theory, preservation theorems, quantifier rank}
}
Document
Extension Preservation on Dense Graph Classes
Abstract
Preservation theorems provide a direct correspondence between the syntactic structure of first-order sentences and the closure properties of their respective classes of models. A line of work has explored preservation theorems relativised to combinatorially tame classes of sparse structures [Atserias et al., JACM 2006; Atserias et al., SiCOMP 2008; Dawar, JCSS 2010; Dawar and Eleftheriadis, MFCS 2024]. In this article we initiate the study of preservation theorems for dense classes of graphs. In contrast to the sparse setting, we show that extension preservation fails on most natural dense classes of low complexity. Nonetheless, we isolate a technical condition which is sufficient for extension preservation to hold, providing a dense analogue to a result of [Atserias et al., SiCOMP 2008].
Cite as
Ioannis Eleftheriadis. Extension Preservation on Dense Graph Classes. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 7:1-7:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{eleftheriadis:LIPIcs.CSL.2025.7,
author = {Eleftheriadis, Ioannis},
title = {{Extension Preservation on Dense Graph Classes}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {7:1--7: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.7},
URN = {urn:nbn:de:0030-drops-227640},
doi = {10.4230/LIPIcs.CSL.2025.7},
annote = {Keywords: Extension preservation, finite model theory, dense graphs, cliquewidth}
}
Document
The Parameterized Complexity of Learning Monadic Second-Order Logic
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
On Homogeneous Models of Fluted Languages
Abstract
We study the fluted fragment of first-order logic which is often viewed as a multi-variable non-guarded extension to various systems of description logics lacking role-inverses. In this paper we show that satisfiable fluted sentences (even under reasonable extensions) admit special kinds of "nice" models which we call globally/locally homogeneous. Homogeneous models allow us to simplify methods for analysing fluted logics with counting quantifiers and establish a novel result for the decidability of the (finite) satisfiability problem for the fluted fragment with periodic counting. More specifically, we will show that the (finite) satisfiability problem for the language is Tower-complete. If only two variable are used, computational complexity drops to NExpTime-completeness. We supplement our findings by showing that generalisations of fluted logics, such as the adjacent fragment, have finite and general satisfiability problems which are, respectively, Σ⁰₁- and Π⁰₁-complete. Additionally, satisfiability becomes Σ¹₁-complete if periodic counting quantifiers are permitted.
Cite as
Daumantas Kojelis. On Homogeneous Models of Fluted Languages. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{kojelis:LIPIcs.CSL.2025.9,
author = {Kojelis, Daumantas},
title = {{On Homogeneous Models of Fluted Languages}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {9:1--9:20},
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.9},
URN = {urn:nbn:de:0030-drops-227669},
doi = {10.4230/LIPIcs.CSL.2025.9},
annote = {Keywords: Fluted Fragment, Fluted Logic, Fluted Fragment with Periodic Counting, Adjacent Fragment, Adjacent Fragment with Counting, Adjacent Fragment with Periodic Counting, Counting Quantifiers, Periodic Counting Quantifiers, Decidable Fragments of First-Order Logic}
}
Document
The Complexity of Second-Order HyperLTL
Abstract
We determine the complexity of second-order HyperLTL satisfiability, finite-state satisfiability, and model-checking: All three are equivalent to truth in third-order arithmetic.
We also consider two fragments of second-order HyperLTL that have been introduced with the aim to facilitate effective model-checking by restricting the sets one can quantify over. The first one restricts second-order quantification to smallest/largest sets that satisfy a guard while the second one restricts second-order quantification further to least fixed points of (first-order) HyperLTL definable functions. All three problems for the first fragment are still equivalent to truth in third-order arithmetic while satisfiability for the second fragment is Σ₁¹-complete, i.e., only as hard as for (first-order) HyperLTL and therefore much less complex. Finally, finite-state satisfiability and model-checking are in Σ₂² and are Σ₁¹-hard, and thus also less complex than for full second-order HyperLTL.
Cite as
Hadar Frenkel and Martin Zimmermann. The Complexity of Second-Order HyperLTL. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 10:1-10:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{frenkel_et_al:LIPIcs.CSL.2025.10,
author = {Frenkel, Hadar and Zimmermann, Martin},
title = {{The Complexity of Second-Order HyperLTL}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {10:1--10:23},
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.10},
URN = {urn:nbn:de:0030-drops-227679},
doi = {10.4230/LIPIcs.CSL.2025.10},
annote = {Keywords: HyperLTL, Satisfiability, Model-checking}
}
Document
On the Expansion of Monadic Second-Order Logic with Cantor-Bendixson Rank and Order Type Predicates
Abstract
In this work, we consider two extensions of monadic second-order logic, and study in what cases the classical decidability results are preserved.
The first extension, MSO[CBrank_β], is MSO (over the signature of the binary tree) augmented with the extra ability to express that the subtree over a set X has Cantor-Bendixson rank β, for some fixed countable ordinal β. We show that this extension is decidable over the binary tree if and only if β is finite, which means that it is decidable if and only if it is equivalent in expressiveness to MSO.
The second extension, MSO[otp_α], is MSO (over the signature of order) augmented with the extra ability to express that the suborder induced by a set X has order type α for some fixed countable ordinal α. We show that this extension is decidable over countable ordinals if and only if α < ω^ω, which means that it is decidable if and only if it is equivalent in expressiveness to MSO.
The first result can be established as a consequence of the second. The second result relies on the undecidability results of the logic BMSO (itself relying on the undecidability of MSO+U) in the case of ω^β for β a limit ordinal, and on entirely new techniques when β is a successor ordinal. We also have some partial extensions of the second result to some uncountable cases.
Cite as
Thomas Colcombet and Alexander Rabinovich. On the Expansion of Monadic Second-Order Logic with Cantor-Bendixson Rank and Order Type Predicates. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 11:1-11:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{colcombet_et_al:LIPIcs.CSL.2025.11,
author = {Colcombet, Thomas and Rabinovich, Alexander},
title = {{On the Expansion of Monadic Second-Order Logic with Cantor-Bendixson Rank and Order Type Predicates}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {11:1--11:26},
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.11},
URN = {urn:nbn:de:0030-drops-227685},
doi = {10.4230/LIPIcs.CSL.2025.11},
annote = {Keywords: Logic, Algorithmic model theory, Monadic second-order logic, Ordinals, Binary tree}
}
Document
First-Order Logic with Equicardinality in Random Graphs
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
Computational Complexity of the Weisfeiler-Leman Dimension
Abstract
The Weisfeiler-Leman dimension of a graph G is the least number k such that the k-dimensional Weisfeiler-Leman algorithm distinguishes G from every other non-isomorphic graph, or equivalently, the least k such that G is definable in (k+1)-variable first-order logic with counting. The dimension is a standard measure of the descriptive or structural complexity of a graph and recently finds various applications in particular in the context of machine learning. This paper studies the complexity of computing the Weisfeiler-Leman dimension. We observe that deciding whether the Weisfeiler-Leman dimension of G is at most k is NP-hard, even if G is restricted to have 4-bounded color classes. For each fixed k ≥ 2, we give a polynomial-time algorithm that decides whether the Weisfeiler-Leman dimension of a given graph with 5-bounded color classes is at most k. Moreover, we show that for these bounds on the color classes, this is optimal because the problem is PTIME-hard under logspace-uniform AC_0-reductions. Furthermore, for each larger bound c on the color classes and each fixed k ≥ 2, we provide a polynomial-time decision algorithm for the abelian case, that is, for structures of which each color class has an abelian automorphism group.
While the graph classes we consider may seem quite restrictive, graphs with 4-bounded abelian colors include CFI-graphs and multipedes, which form the basis of almost all known hard instances and lower bounds related to the Weisfeiler-Leman algorithm.
Cite as
Moritz Lichter, Simon Raßmann, and Pascal Schweitzer. Computational Complexity of the Weisfeiler-Leman Dimension. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{lichter_et_al:LIPIcs.CSL.2025.13,
author = {Lichter, Moritz and Ra{\ss}mann, Simon and Schweitzer, Pascal},
title = {{Computational Complexity of the Weisfeiler-Leman Dimension}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {13:1--13:22},
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.13},
URN = {urn:nbn:de:0030-drops-227707},
doi = {10.4230/LIPIcs.CSL.2025.13},
annote = {Keywords: Weisfeiler-Leman algorithm, dimension, complexity, coherent configurations}
}
Document
Finite Variable Counting Logics with Restricted Requantification
Abstract
Counting logics with a bounded number of variables form one of the central concepts in descriptive complexity theory. Although they restrict the number of variables that a formula can contain, the variables can be nested within scopes of quantified occurrences of themselves. In other words, the variables can be requantified. We study the fragments obtained from counting logics by restricting requantification for some but not necessarily all the variables.
Similar to the logics without limitation on requantification, we develop tools to investigate the restricted variants. Specifically, we introduce a bijective pebble game in which certain pebbles can only be placed once and for all, and a corresponding two-parametric family of Weisfeiler-Leman algorithms. We show close correspondences between the three concepts.
By using a suitable cops-and-robber game and adaptations of the Cai-Fürer-Immerman construction, we completely clarify the relative expressive power of the new logics.
We show that the restriction of requantification has beneficial algorithmic implications in terms of graph identification. Indeed, we argue that with regard to space complexity, non-requantifiable variables only incur an additive polynomial factor when testing for equivalence. In contrast, for all we know, requantifiable variables incur a multiplicative linear factor.
Finally, we observe that graphs of bounded tree-depth and 3-connected planar graphs can be identified using no, respectively, only a very limited number of requantifiable variables.
Cite as
Simon Raßmann, Georg Schindling, and Pascal Schweitzer. Finite Variable Counting Logics with Restricted Requantification. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{ramann_et_al:LIPIcs.CSL.2025.14,
author = {Ra{\ss}mann, Simon and Schindling, Georg and Schweitzer, Pascal},
title = {{Finite Variable Counting Logics with Restricted Requantification}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {14:1--14:23},
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.14},
URN = {urn:nbn:de:0030-drops-227716},
doi = {10.4230/LIPIcs.CSL.2025.14},
annote = {Keywords: Requantification, Finite variable counting logics, Weisfeiler-Leman algorithm}
}
Document
On the VC Dimension of First-Order Logic with Counting and Weight Aggregation
Abstract
We prove optimal upper bounds on the Vapnik-Chervonenkis density of formulas in the extensions of first-order logic with counting (FOC_1) and with weight aggregation (FOWA_1) on nowhere dense classes of (vertex- and edge-)weighted finite graphs. This lifts a result of Pilipczuk, Siebertz, and Toruńczyk [Michał Pilipczuk et al., 2018] from first-order logic on ordinary finite graphs to substantially more expressive logics on weighted finite graphs. Moreover, this proves that every FOC_1 formula and every FOWA_1 formula has bounded Vapnik-Chervonenkis dimension on nowhere dense classes of weighted finite graphs; thereby, it lifts a result of Adler and Adler [Hans Adler and Isolde Adler, 2014] from first-order logic to FOC_1 and FOWA_1.
Generalising another result of Pilipczuk, Siebertz, and Toruńczyk [Michał Pilipczuk et al., 2018], we also provide an explicit upper bound on the ladder index of FOC_1 and FOWA_1 formulas on nowhere dense classes. This shows that nowhere dense classes of weighted finite graphs are FOC_1-stable and FOWA_1-stable.
Cite as
Steffen van Bergerem and Nicole Schweikardt. On the VC Dimension of First-Order Logic with Counting and Weight Aggregation. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{vanbergerem_et_al:LIPIcs.CSL.2025.15,
author = {van Bergerem, Steffen and Schweikardt, Nicole},
title = {{On the VC Dimension of First-Order Logic with Counting and Weight Aggregation}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {15:1--15: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.15},
URN = {urn:nbn:de:0030-drops-227722},
doi = {10.4230/LIPIcs.CSL.2025.15},
annote = {Keywords: VC dimension, VC density, stability, nowhere dense graphs, first-order logic with weight aggregation, first-order logic with counting}
}
Document
Undefinability of Approximation of 2-To-2 Games
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
Description Complexity of Unary Structures in First-Order Logic with Links to Entropy
Abstract
The description complexity of a model is the length of the shortest formula that defines the model. We study the description complexity of unary structures in first-order logic FO, also drawing links to semantic complexity in the form of entropy. The class of unary structures provides, e.g., a simple way to represent tabular Boolean data sets as relational structures. We define structures with FO-formulas that are strictly linear in the size of the model as opposed to using the naive quadratic ones, and we use arguments based on formula size games to obtain related lower bounds for description complexity. For a typical structure the upper and lower bounds in fact match up to a sublinear term, leading to a precise asymptotic result on the expected description complexity of a randomly selected structure. We then give bounds on the relationship between Shannon entropy and description complexity. We extend this relationship also to Boltzmann entropy by establishing an asymptotic match between the two entropies. Despite the simplicity of unary structures, our arguments require the use of formula size games, Stirling’s approximation and Chernoff bounds.
Cite as
Reijo Jaakkola, Antti Kuusisto, and Miikka Vilander. Description Complexity of Unary Structures in First-Order Logic with Links to Entropy. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{jaakkola_et_al:LIPIcs.CSL.2025.17,
author = {Jaakkola, Reijo and Kuusisto, Antti and Vilander, Miikka},
title = {{Description Complexity of Unary Structures in First-Order Logic with Links to Entropy}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {17:1--17:20},
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.17},
URN = {urn:nbn:de:0030-drops-227749},
doi = {10.4230/LIPIcs.CSL.2025.17},
annote = {Keywords: formula size, finite model theory, formula size games, entropy, randomness}
}
Document
Reachability for Multi-Priced Timed Automata with Positive and Negative Rates
Abstract
Multi-priced timed automata (MPTA) are timed automata with observer variables whose derivatives can change from one location to another. Observers are read-once variables: they do not affect the control flow of the automaton and their value is output only at the end of a run. Thus MPTA lie between timed and hybrid automata in expressiveness. Previous work considered observers with non-negative slope in every location. In this paper we treat observers that have both positive and negative rates. Our main result is an algorithm to decide a gap version of the reachability problem for this variant of MPTA. We translate the gap reachability problem into a gap satisfiability problem for mixed integer-real systems of nonlinear constraints. Our main technical contribution - a result of independent interest - is a procedure to solve such contraints via a combination of branch-and-bound and relaxation-and-rounding.
Cite as
Andrew Scoones, Mahsa Shirmohammadi, and James Worrell. Reachability for Multi-Priced Timed Automata with Positive and Negative Rates. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 18:1-18:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{scoones_et_al:LIPIcs.CSL.2025.18,
author = {Scoones, Andrew and Shirmohammadi, Mahsa and Worrell, James},
title = {{Reachability for Multi-Priced Timed Automata with Positive and Negative Rates}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {18:1--18:13},
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.18},
URN = {urn:nbn:de:0030-drops-227758},
doi = {10.4230/LIPIcs.CSL.2025.18},
annote = {Keywords: Bilinear constraints, Existential theory of real closed fields, Diophantine approximation, Pareto curve}
}
Document
Two-Way One-Counter Nets Revisited
Abstract
One Counter Nets (OCNs) are finite-state automata equipped with a counter that cannot become negative, but cannot be explicitly tested for zero. Their close connection to various other models (e.g., PDAs, Vector Addition Systems, and Counter Automata) make them an attractive modeling tool.
The two-way variant of OCNs (2-OCNs) was introduced in the 1980’s and shown to be more expressive than OCNs, so much so that the emptiness problem is undecidable already in the deterministic model (2-DOCNs).
In a first part, we study the emptiness problem of natural restrictions of 2-OCNs, under the light of modern results about Vector Addition System with States (VASS). We show that emptiness is decidable for 2-OCNs over bounded languages (i.e., languages contained in a₁^* a₂^* ⋯ a_k^*), and decidable and Ackermann-complete for sweeping 2-OCNs, where the head direction only changes at the end-markers. Both decidability results revolve around reducing the problem to VASS reachability, but they rely on strikingly different approaches. In a second part, we study the expressive power of 2-OCNs, showing an array of connections between bounded languages, sweeping 2-OCNs, and semilinear languages. Most noteworthy among these connections, is that the bounded languages recognized by sweeping 2-OCNs are precisely those that are semilinear. Finally, we establish an intricate pumping lemma for 2-DOCNs and use it to show that there are OCN languages that are not 2-DOCN recognizable, improving on the known result that there are such 2-OCN languages.
Cite as
Shaull Almagor, Michaël Cadilhac, and Asaf Yeshurun. Two-Way One-Counter Nets Revisited. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{almagor_et_al:LIPIcs.CSL.2025.19,
author = {Almagor, Shaull and Cadilhac, Micha\"{e}l and Yeshurun, Asaf},
title = {{Two-Way One-Counter Nets Revisited}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {19:1--19:20},
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.19},
URN = {urn:nbn:de:0030-drops-227765},
doi = {10.4230/LIPIcs.CSL.2025.19},
annote = {Keywords: Counter Net, Two way, Automata}
}
Document
Boundedness of Cost Register Automata over the Integer Min-Plus Semiring
Abstract
Cost register automata (CRAs) are deterministic automata with registers taking values from a fixed semiring. A CRA computes a function from words to values from this semiring. CRAs are tightly related to well-studied weighted automata. Given a CRA, the boundedness problem asks if there exists a natural number N such that for every word, the value of the CRA on this word does not exceed N. This problem is known to be undecidable for the class of linear CRAs over the integer min-plus semiring (ℤ∪{+∞}, min, +), but very little is known about its subclasses. In this paper, we study boundedness of copyless linear CRAs with resets over the integer min-plus semiring. We show that it is decidable for such CRAs with at most two registers. More specifically, we show that it is, respectively, NL-complete and in coNP if the numbers in the input are presented in unary and binary. We also provide complexity results for two classes with an arbitrary number of registers. Namely, we show that for CRAs that use the minimum operation only in the output function, boundedness is PSPACE-complete if transferring values to other registers is allowed, and is coNP-complete otherwise. Finally, for each f_i in the hierarchy of fast-growing functions, we provide a stateless CRA with i registers whose output exceeds N only on runs longer than f_i(N). Our construction yields a non-elementary lower bound already for four registers.
Cite as
Andrei Draghici, Radosław Piórkowski, and Andrew Ryzhikov. Boundedness of Cost Register Automata over the Integer Min-Plus Semiring. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 20:1-20:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{draghici_et_al:LIPIcs.CSL.2025.20,
author = {Draghici, Andrei and Pi\'{o}rkowski, Rados{\l}aw and Ryzhikov, Andrew},
title = {{Boundedness of Cost Register Automata over the Integer Min-Plus Semiring}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {20:1--20:23},
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.20},
URN = {urn:nbn:de:0030-drops-227775},
doi = {10.4230/LIPIcs.CSL.2025.20},
annote = {Keywords: cost register automata, boundedness, decidability}
}
Document
The Algebras for Automatic Relations
Abstract
We introduce "synchronous algebras", an algebraic structure tailored to recognize automatic relations (a.k.a. synchronous relations, or regular relations). They are the equivalent of monoids for regular languages, however they conceptually differ in two points: first, they are typed and second, they are equipped with a dependency relation expressing constraints between elements of different types.
The interest of the proposed definition is that it allows to lift, in an effective way, pseudovarieties of regular languages to that of synchronous relations, and we show how algebraic characterizations of pseudovarieties of regular languages can be lifted to the pseudovarieties of synchronous relations that they induce. Since this construction is effective, this implies that the membership problem is decidable for (infinitely) many natural classes of automatic relations. A typical example of such a pseudovariety is the class of "group relations", defined as the relations recognized by finite-state synchronous permutation automata.
In order to prove this result, we adapt two pillars of algebraic language theory to synchronous algebras: (a) any relation admits a syntactic synchronous algebra recognizing it, and moreover, the relation is synchronous if, and only if, its syntactic algebra is finite and (b) classes of synchronous relations with desirable closure properties (i.e. pseudovarieties) correspond to pseudovarieties of synchronous algebras.
Cite as
Rémi Morvan. The Algebras for Automatic Relations. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{morvan:LIPIcs.CSL.2025.21,
author = {Morvan, R\'{e}mi},
title = {{The Algebras for Automatic Relations}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {21:1--21: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.21},
URN = {urn:nbn:de:0030-drops-227780},
doi = {10.4230/LIPIcs.CSL.2025.21},
annote = {Keywords: synchronous automata, automatic relations, regular relations, transductions, synchronous algebras, Eilenberg correspondence, pseudovarieties, algebraic characterizations}
}
Document
On the Minimisation of Deterministic and History-Deterministic Generalised (Co)Büchi Automata
Abstract
We present a polynomial-time algorithm minimising the number of states of history-deterministic generalised coBüchi automata, building on the work of Abu Radi and Kupferman on coBüchi automata. On the other hand, we establish that the minimisation problem for both deterministic and history-deterministic generalised Büchi automata is NP-complete, as well as the problem of minimising at the same time the number of states and colours of history-deterministic generalised coBüchi automata.
Cite as
Antonio Casares, Olivier Idir, Denis Kuperberg, Corto Mascle, and Aditya Prakash. On the Minimisation of Deterministic and History-Deterministic Generalised (Co)Büchi Automata. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{casares_et_al:LIPIcs.CSL.2025.22,
author = {Casares, Antonio and Idir, Olivier and Kuperberg, Denis and Mascle, Corto and Prakash, Aditya},
title = {{On the Minimisation of Deterministic and History-Deterministic Generalised (Co)B\"{u}chi Automata}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {22:1--22: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.22},
URN = {urn:nbn:de:0030-drops-227798},
doi = {10.4230/LIPIcs.CSL.2025.22},
annote = {Keywords: Automata minimisation, omega-regular languages, good-for-games automata}
}
Document
Permissive Equilibria in Multiplayer Reachability Games
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}
}
Document
Propositional Logics of Overwhelming Truth
Abstract
Cryptographers consider that asymptotic security holds when, for any possible attacker running in polynomial time, the probability that the attack succeeds is negligible, i.e. that it tends fast enough to zero with the size of secrets. In order to reason formally about cryptographic truth, one may thus consider logics where a formula is satisfied when it is true with overwhelming probability, i.e. a probability that tends fast enough to one with the size of secrets. In such logics it is not always the case that either ϕ or ⌝ϕ is satisfied by a given model. However, security analyses will inevitably involve specific formulas, which we call determined, satisfying this property - typically because they are not probabilistic. The Squirrel proof assistant, which implements a logic of overwhelming truth, features ad-hoc proof rules for this purpose.
In this paper, we study several propositional logics whose semantics rely on overwhelming truth. We first consider a modal logic of overwhelming truth, and show that it coincides with S5. In addition to providing an axiomatization, this brings a well-behaved proof system for our logic in the form of Poggiolesi’s hypersequent calculus. Further, we show that this system can be adapted to elegantly incorporate reasoning on determined atoms. We then consider a logic that is closer to Squirrel’s language, where the overwhelming truth modality cannot be nested. In that case, we show that a simple proof system, based on regular sequents, is sound and complete. This result justifies the core of Squirrel’s proof system.
Cite as
Thibaut Antoine and David Baelde. Propositional Logics of Overwhelming Truth. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{antoine_et_al:LIPIcs.CSL.2025.24,
author = {Antoine, Thibaut and Baelde, David},
title = {{Propositional Logics of Overwhelming Truth}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {24:1--24: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.24},
URN = {urn:nbn:de:0030-drops-227818},
doi = {10.4230/LIPIcs.CSL.2025.24},
annote = {Keywords: Cryptography, Modal Logic, Sequent Calculus}
}
Document
Exponential Lower Bounds on Definable Fixed Points
Abstract
It is known that the μ-calculus is no more expressive than basic modal logic over the class of finite partial orders, as well as over the class of finite, strict partial orders. Nevertheless, we show that the μ-calculus is exponentially more succinct, even when a reflexive modality is added as primitive. As corollaries, we obtain a lower bound for the fixed-point theorem for Gödel-Löb logic and a variant for Grzegorczyk logic, as well as lower bounds on interpolants for the interpolation theorem of Gödel-Löb logic.
Cite as
Konstantinos Papafilippou and David Fernández-Duque. Exponential Lower Bounds on Definable Fixed Points. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{papafilippou_et_al:LIPIcs.CSL.2025.25,
author = {Papafilippou, Konstantinos and Fern\'{a}ndez-Duque, David},
title = {{Exponential Lower Bounds on Definable Fixed Points}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {25:1--25: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.25},
URN = {urn:nbn:de:0030-drops-227827},
doi = {10.4230/LIPIcs.CSL.2025.25},
annote = {Keywords: Modal logic, Provability Logic, Fixed-Point Theorem, mu-calculus, Interpolation, Succinctness}
}
Document
The Complexity of Deciding Characteristic Formulae in Van Glabbeek’s Branching-Time Spectrum
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
A Complete Diagrammatic Calculus for Automata Simulation
Abstract
We give a sound and complete (in)equational theory for simulation of finite state automata. Our approach uses a string diagrammatic calculus to represent automata and a functorial semantics to capture simulation in a compositional way. Interestingly, in contrast to other approaches based on regular expressions, fixpoints are a derived notion in our calculus and the resulting axiomatisation is finitary.
Cite as
Thibaut Antoine, Robin Piedeleu, Alexandra Silva, and Fabio Zanasi. A Complete Diagrammatic Calculus for Automata Simulation. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 27:1-27:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{antoine_et_al:LIPIcs.CSL.2025.27,
author = {Antoine, Thibaut and Piedeleu, Robin and Silva, Alexandra and Zanasi, Fabio},
title = {{A Complete Diagrammatic Calculus for Automata Simulation}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {27:1--27:22},
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.27},
URN = {urn:nbn:de:0030-drops-227848},
doi = {10.4230/LIPIcs.CSL.2025.27},
annote = {Keywords: finite-state automata, simulation, string diagrams, axiomatisation}
}
Document
Strong Induction Is an Up-To Technique
Abstract
Up-to techniques are enhancements of the coinduction proof principle which, in lattice theoretic terms, is the dual of induction. What is the dual of coinduction up-to? By means of duality, we illustrate a theory of induction up-to and we observe that an elementary proof technique, commonly known as strong induction, is an instance of induction up-to. We also show that, when generalising our theory from lattices to categories, one obtains an enhancement of the induction definition principle known in the literature as comonadic recursion.
Cite as
Filippo Bonchi, Elena Di Lavore, and Anna Ricci. Strong Induction Is an Up-To Technique. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 28:1-28:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{bonchi_et_al:LIPIcs.CSL.2025.28,
author = {Bonchi, Filippo and Di Lavore, Elena and Ricci, Anna},
title = {{Strong Induction Is an Up-To Technique}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {28:1--28: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.28},
URN = {urn:nbn:de:0030-drops-227856},
doi = {10.4230/LIPIcs.CSL.2025.28},
annote = {Keywords: Induction, Coinduction, Up-to Techniques, Induction up-to, Lattices, Algebras}
}
Document
Correspondences Between Codensity and Coupling-Based Liftings, a Practical Approach
Abstract
The Kantorovich distance is a widely used metric between probability distributions. The Kantorovich-Rubinstein duality states that it can be defined in two equivalent ways: as a supremum, based on non-expansive functions into [0,1], and as an infimum, based on probabilistic couplings.
Orthogonally, there are categorical generalisations of both presentations proposed in the literature, in the form of codensity liftings and what we refer to as coupling-based liftings. Both lift endofunctors on the category Set of sets and functions to that of pseudometric spaces, and both are parameterised by modalities from coalgebraic modal logic.
A generalisation of the Kantorovich-Rubinstein duality has been more nebulous - it is known not to work in some cases. In this paper we propose a compositional approach for obtaining such generalised dualities for a class of functors, which is closed under coproducts and products. Our approach is based on an explicit construction of modalities and also applies to and extends known cases such as that of the powerset functor.
Cite as
Samuel Humeau, Daniela Petrisan, and Jurriaan Rot. Correspondences Between Codensity and Coupling-Based Liftings, a Practical Approach. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{humeau_et_al:LIPIcs.CSL.2025.29,
author = {Humeau, Samuel and Petrisan, Daniela and Rot, Jurriaan},
title = {{Correspondences Between Codensity and Coupling-Based Liftings, a Practical Approach}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {29:1--29: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.29},
URN = {urn:nbn:de:0030-drops-227861},
doi = {10.4230/LIPIcs.CSL.2025.29},
annote = {Keywords: Kantorovich distance, behavioural metrics, Kantorovich-Rubinstein duality, functor liftings}
}
Document
A Complete Inference System for Probabilistic Infinite Trace Equivalence
Abstract
We present the first sound and complete axiomatization of infinite trace semantics for generative probabilistic transition systems. Our approach is categorical, and we build on recent results on proper functors over convex sets. At the core of our proof is a characterization of infinite traces as the final coalgebra of a functor over convex algebras. Somewhat surprisingly, our axiomatization of infinite trace semantics coincides with that of finite trace semantics, even though the techniques used in the completeness proof are significantly different.
Cite as
Corina Cîrstea, Lawrence S. Moss, Victoria Noquez, Todd Schmid, Alexandra Silva, and Ana Sokolova. A Complete Inference System for Probabilistic Infinite Trace Equivalence. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 30:1-30:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{cirstea_et_al:LIPIcs.CSL.2025.30,
author = {C\^{i}rstea, Corina and Moss, Lawrence S. and Noquez, Victoria and Schmid, Todd and Silva, Alexandra and Sokolova, Ana},
title = {{A Complete Inference System for Probabilistic Infinite Trace Equivalence}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {30:1--30:23},
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.30},
URN = {urn:nbn:de:0030-drops-227870},
doi = {10.4230/LIPIcs.CSL.2025.30},
annote = {Keywords: Coalgebra, infinite trace, semantics, logic, convex sets}
}
Document
Simple Types for Probabilistic Termination
Abstract
We present a new typing discipline to guarantee the probability of termination in probabilistic lambda-calculi. The main contribution is a particular naturality and simplicity: our probabilistic types are as simple types, but generated from probabilities as base types, representing a least probability of termination. Simple types are recovered by restricting probabilities to one.
Our vehicle is the Probabilistic Event Lambda-Calculus by Dal Lago, Guerrieri, and Heijltjes, which presents a solution to the issue of confluence in probabilistic lambda-calculi. Our probabilistic type system provides an alternative solution to that using counting quantifiers by Antonelli, Dal Lago, and Pistone, for the same calculus.
The problem that both type systems address is to give a lower bound on the probability that terms head-normalize. Following the recent Functional Machine Calculus by Heijltjes, our development takes the (simplified) Krivine machine as primary, and proceeds via an extension of the calculus with sequential composition and identity on the machine. Our type system then gives a natural account of termination probability on the Krivine machine, reflected back onto head-normalization for the original calculus. In this way we are able to avoid the use of counting quantifiers, while improving on the termination bounds given by Antonelli, Dal Lago, and Pistone.
Cite as
Willem Heijltjes and Georgina Majury. Simple Types for Probabilistic Termination. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{heijltjes_et_al:LIPIcs.CSL.2025.31,
author = {Heijltjes, Willem and Majury, Georgina},
title = {{Simple Types for Probabilistic Termination}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {31:1--31: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.31},
URN = {urn:nbn:de:0030-drops-227885},
doi = {10.4230/LIPIcs.CSL.2025.31},
annote = {Keywords: lambda-calculus, probabilistic termination, simple types}
}
Document
A Mixed Linear and Graded Logic: Proofs, Terms, and Models
Abstract
Graded modal logics generalise standard modal logics via families of modalities indexed by an algebraic structure whose operations mediate between the different modalities. The graded "of-course" modality !_r captures how many times a proposition is used and has an analogous interpretation to the of-course modality from linear logic; the of-course modality from linear logic can be modelled by a linear exponential comonad and graded of-course can be modelled by a graded linear exponential comonad. Benton showed in his seminal paper on Linear/Non-Linear logic that the of-course modality can be split into two modalities connecting intuitionistic logic with linear logic, forming a symmetric monoidal adjunction. Later, Fujii et al. demonstrated that every graded comonad can be decomposed into an adjunction and a "strict action". We give a similar result to Benton, leveraging Fujii et al.’s decomposition, showing that graded modalities can be split into two modalities connecting a graded logic with a graded linear logic. We propose a sequent calculus, its proof theory and categorical model, and a natural deduction system which we show is isomorphic to the sequent calculus system. Interestingly, our system can also be understood as Linear/Non-Linear logic composed with an action that adds the grading, further illuminating the shared principles between linear logic and a class of graded modal logics.
Cite as
Victoria Vollmer, Danielle Marshall, Harley Eades III, and Dominic Orchard. A Mixed Linear and Graded Logic: Proofs, Terms, and Models. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 32:1-32:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{vollmer_et_al:LIPIcs.CSL.2025.32,
author = {Vollmer, Victoria and Marshall, Danielle and Eades III, Harley and Orchard, Dominic},
title = {{A Mixed Linear and Graded Logic: Proofs, Terms, and Models}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {32:1--32: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.32},
URN = {urn:nbn:de:0030-drops-227892},
doi = {10.4230/LIPIcs.CSL.2025.32},
annote = {Keywords: linear logic, graded modal logic, adjoint decomposition}
}
Document
Quantitative Graded Semantics and Spectra of Behavioural Metrics
Abstract
Behavioural metrics provide a quantitative refinement of classical two-valued behavioural equivalences on systems with quantitative data, such as metric or probabilistic transition systems. In analogy to the linear-time/ branching-time spectrum of two-valued behavioural equivalences on transition systems, behavioural metrics vary in granularity, and are often characterized by fragments of suitable modal logics. In the latter respect, the quantitative case is, however, more involved than the two-valued one; in fact, we show that probabilistic metric trace distance cannot be characterized by any compositionally defined modal logic with unary modalities. We go on to provide a unifying treatment of spectra of behavioural metrics in the emerging framework of graded monads, working in coalgebraic generality, that is, parametrically in the system type. In the ensuing development of quantitative graded semantics, we introduce algebraic presentations of graded monads on the category of metric spaces. Moreover, we provide a general criterion for a given real-valued modal logic to characterize a given behavioural distance. As a case study, we apply this criterion to obtain a new characteristic modal logic for trace distance in fuzzy metric transition systems.
Cite as
Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Quantitative Graded Semantics and Spectra of Behavioural Metrics. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{forster_et_al:LIPIcs.CSL.2025.33,
author = {Forster, Jonas and Schr\"{o}der, Lutz and Wild, Paul and Beohar, Harsh and Gurke, Sebastian and K\"{o}nig, Barbara and Messing, Karla},
title = {{Quantitative Graded Semantics and Spectra of Behavioural Metrics}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {33:1--33: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.33},
URN = {urn:nbn:de:0030-drops-227907},
doi = {10.4230/LIPIcs.CSL.2025.33},
annote = {Keywords: transition systems, modal logics, coalgebras, behavioural metrics}
}
Document
The Lambda Calculus Is Quantifiable
Abstract
In this paper we introduce several quantitative methods for the lambda-calculus based on partial metrics, a well-studied variant of standard metric spaces that have been used to metrize non-Hausdorff topologies, like those arising from Scott domains. First, we study quantitative variants, based on program distances, of sensible equational theories for the λ-calculus, like those arising from Böhm trees and from the contextual preorder. Then, we introduce applicative distances capturing higher-order Scott topologies, including reflexive objects like the D_∞ model. Finally, we provide a quantitative insight on the well-known connection between the Böhm tree of a λ-term and its Taylor expansion, by showing that the latter can be presented as an isometric transformation.
Cite as
Valentin Maestracci and Paolo Pistone. The Lambda Calculus Is Quantifiable. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 34:1-34:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{maestracci_et_al:LIPIcs.CSL.2025.34,
author = {Maestracci, Valentin and Pistone, Paolo},
title = {{The Lambda Calculus Is Quantifiable}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {34:1--34:23},
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.34},
URN = {urn:nbn:de:0030-drops-227911},
doi = {10.4230/LIPIcs.CSL.2025.34},
annote = {Keywords: Lambda-calculus, Scott semantics, Partial metric spaces, B\"{o}hm trees, Taylor expansion}
}
Document
A Kleene Algebra with Tests for Union Bound Reasoning About Probabilistic Programs
Abstract
Kleene Algebra with Tests (KAT) provides a framework for algebraic equational reasoning about imperative programs. The recent variant Guarded KAT (GKAT) allows to reason on non-probabilistic properties of probabilistic programs. Here we introduce an extension of this framework called approximate GKAT (aGKAT), which equips GKAT with a partially ordered monoid (real numbers) enabling to express satisfaction of (deterministic) properties except with a probability up to a certain bound. This allows to represent in equational reasoning "à la KAT" proofs of probabilistic programs based on the union bound, a technique from basic probability theory. We show how a propositional variant of approximate Hoare Logic (aHL), a program logic for union bound, can be soundly encoded in our system aGKAT. We then illustrate the use of aGKAT with an example of accuracy analysis from the field of differential privacy.
Cite as
Leandro Gomes, Patrick Baillot, and Marco Gaboardi. A Kleene Algebra with Tests for Union Bound Reasoning About Probabilistic Programs. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 35:1-35:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{gomes_et_al:LIPIcs.CSL.2025.35,
author = {Gomes, Leandro and Baillot, Patrick and Gaboardi, Marco},
title = {{A Kleene Algebra with Tests for Union Bound Reasoning About Probabilistic Programs}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {35:1--35: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.35},
URN = {urn:nbn:de:0030-drops-227929},
doi = {10.4230/LIPIcs.CSL.2025.35},
annote = {Keywords: Kleene algebras with tests, Hoare logic, equational reasoning, probabilistic programs, union bound, formal verification}
}
Document
Kleene Algebra with Commutativity Conditions Is Undecidable
Abstract
We prove that the equational theory of Kleene algebra with commutativity conditions on primitives (or atomic terms) is undecidable, thereby settling a longstanding open question in the theory of Kleene algebra. While this question has also been recently solved independently by Kuznetsov, our results hold even for weaker theories that do not support the induction axioms of Kleene algebra.
Cite as
Arthur Azevedo de Amorim, Cheng Zhang, and Marco Gaboardi. Kleene Algebra with Commutativity Conditions Is Undecidable. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 36:1-36:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{azevedodeamorim_et_al:LIPIcs.CSL.2025.36,
author = {Azevedo de Amorim, Arthur and Zhang, Cheng and Gaboardi, Marco},
title = {{Kleene Algebra with Commutativity Conditions Is Undecidable}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {36:1--36:25},
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.36},
URN = {urn:nbn:de:0030-drops-227933},
doi = {10.4230/LIPIcs.CSL.2025.36},
annote = {Keywords: Kleene Algebra, Hypotheses, Complexity}
}
Document
Finite Relational Semantics for Language Kleene Algebra with Complement
Abstract
We study the equational theory of Kleene algebra (KA) w.r.t. languages (here, meaning the equational theory of regular expressions where each letter maps to any language) by extending the algebraic signature with the language complement. This extension significantly enhances the expressive power of KA. In this paper, we present a finite relational semantics completely characterizing the equational theory w.r.t. languages, which extends the relational characterizations known for KA and for KA with top. Based on this relational semantics, we show that the equational theory w.r.t. languages is Π⁰₁-complete for KA with complement (with or without Kleene-star) and is PSPACE-complete if the complement only applies to variables or constants.
Cite as
Yoshiki Nakamura. Finite Relational Semantics for Language Kleene Algebra with Complement. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 37:1-37:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{nakamura:LIPIcs.CSL.2025.37,
author = {Nakamura, Yoshiki},
title = {{Finite Relational Semantics for Language Kleene Algebra with Complement}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {37:1--37:23},
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.37},
URN = {urn:nbn:de:0030-drops-227944},
doi = {10.4230/LIPIcs.CSL.2025.37},
annote = {Keywords: Kleene algebra, Language model, Relational model, Complexity}
}
Document
A Complete Graphical Language for Linear Optical Circuits with Finite-Photon-Number Sources and Detectors
Abstract
Graphical languages are powerful and useful to represent, rewrite and simplify different kinds of processes. In particular, they have been widely used for quantum processes, improving the state of the art for compilation, simulation and verification. In this work, we focus on one of the main carrier of quantum information and computation: linear optical circuits. We introduce the LO_fi-calculus, the first graphical language to reason on the infinite-dimensional photonic space with circuits only composed of the four core elements of linear optics: the phase shifter, the beam splitter, and auxiliary sources and detectors with bounded photon number. First, we study the subfragment of circuits composed of phase shifters and beam splitters, for which we provide the first minimal equational theory. Next, we introduce a rewriting procedure on those LO_fi-circuits that converge to normal forms. We prove those forms to be unique, establishing both a novel and unique representation of linear optical processes. Finally, we complement the language with an equational theory that we prove to be complete: two LO_fi-circuits represent the same quantum process if and only if one can be transformed into the other with the rules of the LO_fi-calculus.
Cite as
Nicolas Heurtel. A Complete Graphical Language for Linear Optical Circuits with Finite-Photon-Number Sources and Detectors. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 38:1-38:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{heurtel:LIPIcs.CSL.2025.38,
author = {Heurtel, Nicolas},
title = {{A Complete Graphical Language for Linear Optical Circuits with Finite-Photon-Number Sources and Detectors}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {38:1--38:23},
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.38},
URN = {urn:nbn:de:0030-drops-227957},
doi = {10.4230/LIPIcs.CSL.2025.38},
annote = {Keywords: Quantum Computing, Graphical Language, Linear Optical Circuits, Linear Optical Quantum Computing, Completeness, Fock Space}
}
Document
A Strictly Linear Subatomic Proof System
Abstract
We present a subatomic deep-inference proof system for a conservative extension of propositional classical logic with decision trees that is strictly linear. In a strictly linear subatomic system, a single linear rule shape subsumes not only the structural rules, such as contraction and weakening, but also the unit equality rules. An interpretation map from subatomic logic to propositional classical logic recovers the usual semantics and proof theoretic properties. By using explicit substitutions that indicate the substitution of one derivation into another, we are able to show that the unit-equality inference steps can be eliminated from a subatomic system for propositional classical logic with only a polynomial complexity cost in the size of the derivation, from which it follows that the system p-simulates Frege systems, and we show cut elimination for the resulting strictly linear system.
Cite as
Victoria Barrett, Alessio Guglielmi, and Benjamin Ralph. A Strictly Linear Subatomic Proof System. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 39:1-39:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{barrett_et_al:LIPIcs.CSL.2025.39,
author = {Barrett, Victoria and Guglielmi, Alessio and Ralph, Benjamin},
title = {{A Strictly Linear Subatomic Proof System}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {39:1--39:22},
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.39},
URN = {urn:nbn:de:0030-drops-227967},
doi = {10.4230/LIPIcs.CSL.2025.39},
annote = {Keywords: Deep inference, Open deduction, Subatomic logic, Decision trees, Explicit substitutions, Cut elimination, Proof theory}
}
Document
Completeness of First-Order Bi-Intuitionistic Logic
Abstract
We provide a succinct and verified completeness proof for first-order bi-intuitionistic logic, relative to constant domain Kripke semantics. By doing so, we make up for the almost-50-year-old substantial mistakes in Rauszer’s foundational work, detected but unresolved by Shillito two years ago. Moreover, an even earlier but historically neglected proof by Klemke has been found to contain at least local errors by Olkhovikov and Badia, that remained unfixed due to the technical complexity of Klemke’s argument. To resolve this unclear situation once and for all, we give a succinct completeness proof, based on and dualising a standard proof for constant domain intuitionistic logic, and verify our constructions using the Coq proof assistant to guarantee correctness.
Cite as
Dominik Kirst and Ian Shillito. Completeness of First-Order Bi-Intuitionistic Logic. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 40:1-40:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{kirst_et_al:LIPIcs.CSL.2025.40,
author = {Kirst, Dominik and Shillito, Ian},
title = {{Completeness of First-Order Bi-Intuitionistic Logic}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {40:1--40: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.40},
URN = {urn:nbn:de:0030-drops-227979},
doi = {10.4230/LIPIcs.CSL.2025.40},
annote = {Keywords: bi-intuitionistic logic, first-order logic, completeness, Coq proof assistant}
}
Document
Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
Abstract
It is well-known that extending the Hilbert axiomatic system for first-order intuitionistic logic with an exclusion operator, that is dual to implication, collapses the domains of models into a constant domain. This makes it an interesting problem to find a sound and complete proof system for first-order bi-intuitionistic logic with non-constant domains that is also conservative over first-order intuitionistic logic. We solve this problem by presenting the first sound and complete proof system for first-order bi-intuitionistic logic with increasing domains. We formalize our proof system as a polytree sequent calculus (a notational variant of nested sequents), and prove that it enjoys cut-elimination and is conservative over first-order intuitionistic logic. A key feature of our calculus is an explicit eigenvariable context, which allows us to control precisely the scope of free variables in a polytree structure. Semantically this context can be seen as encoding a notion of Scott’s existence predicate for intuitionistic logic. This turns out to be crucial to avoid the collapse of domains and to prove the completeness of our proof system. The explicit consideration of the variable context in a formula sheds light on a previously overlooked dependency between the residuation principle and the existence predicate in the first-order setting, which may help to explain the difficulty in designing a sound and complete proof system for first-order bi-intuitionistic logic.
Cite as
Tim S. Lyon, Ian Shillito, and Alwen Tiu. Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 41:1-41:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{lyon_et_al:LIPIcs.CSL.2025.41,
author = {Lyon, Tim S. and Shillito, Ian and Tiu, Alwen},
title = {{Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {41:1--41:23},
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.41},
URN = {urn:nbn:de:0030-drops-227987},
doi = {10.4230/LIPIcs.CSL.2025.41},
annote = {Keywords: Bi-intuitionistic, Cut-elimination, Conservativity, Domain, First-order, Polytree, Proof theory, Reachability, Sequent}
}
Document
Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations
Abstract
We demonstrate the inter-translatability of proofs between the most prominent sequent-based formalisms for Gödel-Löb provability logic. In particular, we consider Sambin and Valentini’s sequent system GL_{seq}, Shamkanov’s non-wellfounded and cyclic sequent systems GL_∞ and GL_{circ}, Poggiolesi’s tree-hypersequent system CSGL, and Negri’s labeled sequent system G3GL. Shamkanov provided proof-theoretic correspondences between GL_{seq}, GL_∞, and GL_{circ}, and Goré and Ramanayake showed how to transform proofs between CSGL and G3GL, however, the exact nature of proof transformations between the former three systems and the latter two systems has remained an open problem. We solve this open problem by showing how to restructure tree-hypersequent proofs into an end-active form and introduce a novel linearization technique that transforms such proofs into linear nested sequent proofs. As a result, we obtain a new proof-theoretic tool for extracting linear nested sequent systems from tree-hypersequent systems, which yields the first cut-free linear nested sequent calculus LNGL for Gödel-Löb provability logic. We show how to transform proofs in LNGL into a certain normal form, where proofs repeat in stages of modal and local rule applications, and which are translatable into GL_{seq} and G3GL proofs. These new syntactic transformations, together with those mentioned above, establish full proof-theoretic correspondences between GL_{seq}, GL_∞, GL_{circ}, CSGL, G3GL, and LNGL while also giving (to the best of the author’s knowledge) the first constructive proof mappings between structural (viz. labeled, tree-hypersequent, and linear nested sequent) systems and a cyclic sequent system.
Cite as
Tim S. Lyon. Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 42:1-42:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{lyon:LIPIcs.CSL.2025.42,
author = {Lyon, Tim S.},
title = {{Unifying Sequent Systems for G\"{o}del-L\"{o}b Provability Logic via Syntactic Transformations}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {42:1--42:23},
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.42},
URN = {urn:nbn:de:0030-drops-227992},
doi = {10.4230/LIPIcs.CSL.2025.42},
annote = {Keywords: Cyclic proof, G\"{o}del-L\"{o}b logic, Labeled sequent, Linear nested sequent, Modal logic, Non-wellfounded proof, Proof theory, Proof transformation, Tree-hypersequent}
}
Document
Linear Realisability over Nets: Multiplicatives
Abstract
We provide a new realisability model based on orthogonality for the multiplicative fragment of linear logic, both in presence of generalised axioms (MLL^✠) and in the standard case (MLL). The novelty is the definition of cut elimination for generalised axioms. We prove that our model is adequate and complete both for MLL^✠ and MLL.
Cite as
Adrien Ragot, Thomas Seiller, and Lorenzo Tortora de Falco. Linear Realisability over Nets: Multiplicatives. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 43:1-43:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{ragot_et_al:LIPIcs.CSL.2025.43,
author = {Ragot, Adrien and Seiller, Thomas and Tortora de Falco, Lorenzo},
title = {{Linear Realisability over Nets: Multiplicatives}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {43:1--43: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.43},
URN = {urn:nbn:de:0030-drops-228002},
doi = {10.4230/LIPIcs.CSL.2025.43},
annote = {Keywords: Linear Logic, Proof Nets, Realisability, Orthogonality, Hypergraphs, Rewriting, Correctness}
}
Document
Classical Linear Logic in Perfect Banach Lattices
Abstract
In recent years, researchers have proposed various models of linear logic with strong connections to measure theory, with probabilistic coherence spaces (PCoh) being one of the most prominent. One of the main limitations of the PCoh model is that it cannot interpret continuous measures. To overcome this obstacle, Ehrhard has extended PCoh to a category of positive cones and linear Scott-continuous functions and shown that it is a model of intuitionistic linear logic. In this work we show that the category PBanLat₁ of perfect Banach lattices and positive linear functions of norm at most 1 can serve the same purpose, with some added benefits. We show that PBanLat₁ is a model of classical linear logic (without exponential) and that PCoh embeds fully and faithfully in PBanLat₁ while preserving the monoidal and *-autonomous structures. Finally, we show how PBanLat₁ can be used to give semantics to a higher-order probabilistic programming language.
Cite as
Pedro H. Azevedo de Amorim, Leon Witzman, and Dexter Kozen. Classical Linear Logic in Perfect Banach Lattices. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 44:1-44:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{azevedodeamorim_et_al:LIPIcs.CSL.2025.44,
author = {Azevedo de Amorim, Pedro H. and Witzman, Leon and Kozen, Dexter},
title = {{Classical Linear Logic in Perfect Banach Lattices}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {44:1--44: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.44},
URN = {urn:nbn:de:0030-drops-228013},
doi = {10.4230/LIPIcs.CSL.2025.44},
annote = {Keywords: Probabilistic Semantics, Linear Logic, Categorical Semantics}
}
Document
Insights from Univalent Foundations: A Case Study Using Double Categories
Abstract
Category theory unifies mathematical concepts, aiding comparisons across structures by incorporating not just objects, but also morphisms capturing interactions between objects. Of particular importance in some applications are double categories, which are categories with two classes of morphisms, axiomatizing two different kinds of interactions between objects. These have found applications in many areas of mathematics and theoretical computer science, for instance, the study of lenses, open systems, and rewriting.
However, double categories come with a wide variety of equivalences, which makes it challenging to transport structure along equivalences. To deal with this challenge, we propose the univalence maxim: each notion of equivalence of categorical structures has a corresponding notion of univalent categorical structure which induces that notion of equivalence. We also prove corresponding univalence principles, which allow us to transport structure and properties along equivalences. In this way, the usually informal practice of reasoning modulo equivalence becomes grounded in an entirely formal logical principle.
We apply this perspective to various double categorical structures, such as (pseudo) double categories and double bicategories. Concretely, we characterize and formalize their definitions in Coq UniMath up to chosen equivalences, which we achieve by establishing their univalence principles.
Cite as
Nima Rasekh, Niels van der Weide, Benedikt Ahrens, and Paige Randall North. Insights from Univalent Foundations: A Case Study Using Double Categories. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 45:1-45:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{rasekh_et_al:LIPIcs.CSL.2025.45,
author = {Rasekh, Nima and van der Weide, Niels and Ahrens, Benedikt and North, Paige Randall},
title = {{Insights from Univalent Foundations: A Case Study Using Double Categories}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {45:1--45: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.45},
URN = {urn:nbn:de:0030-drops-228024},
doi = {10.4230/LIPIcs.CSL.2025.45},
annote = {Keywords: formalization of mathematics, category theory, double categories, univalent foundations}
}
Document
Coslice Colimits in Homotopy Type Theory
Abstract
We contribute to the theory of (homotopy) colimits inside homotopy type theory. The heart of our work characterizes the connection between colimits in coslices of a universe, called coslice colimits, and colimits in the universe (i.e., ordinary colimits). To derive this characterization, we find an explicit construction of colimits in coslices that is tailored to reveal the connection. We use the construction to derive properties of colimits. Notably, we prove that the forgetful functor from a coslice creates colimits over trees. We also use the construction to examine how colimits interact with orthogonal factorization systems and with cohomology theories. As a consequence of their interaction with orthogonal factorization systems, all pointed colimits (special kinds of coslice colimits) preserve n-connectedness, which implies that higher groups are closed under colimits on directed graphs. We have formalized our main construction of the coslice colimit functor in Agda.
Cite as
Perry Hart and Kuen-Bang Hou (Favonia). Coslice Colimits in Homotopy Type Theory. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 46:1-46:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{hart_et_al:LIPIcs.CSL.2025.46,
author = {Hart, Perry and Hou (Favonia), Kuen-Bang},
title = {{Coslice Colimits in Homotopy Type Theory}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {46:1--46:20},
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.46},
URN = {urn:nbn:de:0030-drops-228039},
doi = {10.4230/LIPIcs.CSL.2025.46},
annote = {Keywords: colimits, homotopy type theory, category theory, higher inductive types, synthetic homotopy theory}
}
Document
A Rewriting Theory for Quantum λ-Calculus
Abstract
Quantum lambda calculus has been studied mainly as an idealized programming language - the evaluation essentially corresponds to a deterministic abstract machine. Very little work has been done to develop a rewriting theory for quantum lambda calculus. Recent advances in the theory of probabilistic rewriting give us a way to tackle this task with tools unavailable a decade ago. Our primary focus are standardization and normalization results.
Cite as
Claudia Faggian, Gaetan Lopez, and Benoît Valiron. A Rewriting Theory for Quantum λ-Calculus. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 47:1-47:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{faggian_et_al:LIPIcs.CSL.2025.47,
author = {Faggian, Claudia and Lopez, Gaetan and Valiron, Beno\^{i}t},
title = {{A Rewriting Theory for Quantum \lambda-Calculus}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {47:1--47:22},
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.47},
URN = {urn:nbn:de:0030-drops-228046},
doi = {10.4230/LIPIcs.CSL.2025.47},
annote = {Keywords: quantum lambda-calculus, probabilistic rewriting, operational semantics, asymptotic normalization, principles of quantum programming languages}
}
Document
Quantum and Classical Markovian Graphical Causal Models and Their Identification
Abstract
Markov categories allow formalization of probabilistic and causal reasoning in a general setting that applies uniformly to many different kinds of classical probabilistic processes. It has so far been challenging, however, to generalize these techniques to reasoning about quantum processes, as the quantum no-cloning theorem forbids "copy" maps of the sort that have been used to axiomatize conditional independence, and the related notions of complete common causes and Markovianity, in classical Bayesian networks. Here, we introduce a new categorical notion of Markovian causal model, according to which a distinguished subcategory of "common cause" maps plays a similar role to that of "copy" maps in the categorical formulation of Bayesian networks. Moreover, defining causal models as second-order processes yields a clean and flexible formulation of interventions. Our formalism is both rich enough to handle "complete common cause" assumptions and general enough to encompass not only standard classical causal identification scenarios, but also quantum causal scenarios and new kinds of classical causal identification based on imperfect observations. Furthermore, we show that one can reason uniformly across all of these cases using string-diagrammatic techniques.
Cite as
Jonathan Barrett, Isaac Friend, and Aleks Kissinger. Quantum and Classical Markovian Graphical Causal Models and Their Identification. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 48:1-48:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{barrett_et_al:LIPIcs.CSL.2025.48,
author = {Barrett, Jonathan and Friend, Isaac and Kissinger, Aleks},
title = {{Quantum and Classical Markovian Graphical Causal Models and Their Identification}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {48:1--48:23},
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.48},
URN = {urn:nbn:de:0030-drops-228054},
doi = {10.4230/LIPIcs.CSL.2025.48},
annote = {Keywords: causal inference, Bayesian networks, quantum combs, process theories}
}
Document
Minimality in Finite-Dimensional ZW-Calculi
Abstract
The ZW-calculus is a graphical language capable of representing 2-dimensional quantum systems (qubit) through its diagrams, and manipulating them through its equational theory. We extend the formalism to accommodate finite dimensional Hilbert spaces beyond qubit systems.
First we define a qudit version of the language, where all systems have the same arbitrary finite dimension d, and show that the provided equational theory is both complete - i.e. semantical equivalence is entirely captured by the equations - and minimal - i.e. none of the equations are consequences of the others. We then extend the graphical language further to allow for mixed-dimensional systems. We again show the completeness and minimality of the provided equational theory.
Cite as
Marc de Visme and Renaud Vilmart. Minimality in Finite-Dimensional ZW-Calculi. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 49:1-49:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@InProceedings{devisme_et_al:LIPIcs.CSL.2025.49,
author = {de Visme, Marc and Vilmart, Renaud},
title = {{Minimality in Finite-Dimensional ZW-Calculi}},
booktitle = {33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
pages = {49:1--49:22},
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.49},
URN = {urn:nbn:de:0030-drops-228067},
doi = {10.4230/LIPIcs.CSL.2025.49},
annote = {Keywords: Quantum Computing, Categorical Quantum Mechanics, ZW-calculus, Qudits, Finite Dimensional Hilbert Spaces, Completeness, Minimality}
}