Volume
LIPIcs, Volume 288
32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL)
Event
CSL 2024, February 19-23, 2024, Naples, ItalyEditors
Publication Details
- published at: 2024-02-07
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-310-2
- DBLP: db/conf/csl/csl2024
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 288, CSL 2024, Complete Volume
Abstract
LIPIcs, Volume 288, CSL 2024, Complete Volume
Cite as
32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 1-892, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Proceedings{murano_et_al:LIPIcs.CSL.2024,
title = {{LIPIcs, Volume 288, CSL 2024, Complete Volume}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {1--892},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024},
URN = {urn:nbn:de:0030-drops-196423},
doi = {10.4230/LIPIcs.CSL.2024},
annote = {Keywords: LIPIcs, Volume 288, CSL 2024, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{murano_et_al:LIPIcs.CSL.2024.0,
author = {Murano, Aniello and Silva, Alexandra},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {0:i--0:xiv},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.0},
URN = {urn:nbn:de:0030-drops-196436},
doi = {10.4230/LIPIcs.CSL.2024.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Ackermann Award
The Ackermann Award 2023
Abstract
Report on the 2023 Ackermann Award.
Cite as
Maribel Fernández, Jean Goubault-Larrecq, and Delia Kesner. The Ackermann Award 2023. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{fernandez_et_al:LIPIcs.CSL.2024.1,
author = {Fern\'{a}ndez, Maribel and Goubault-Larrecq, Jean and Kesner, Delia},
title = {{The Ackermann Award 2023}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {1:1--1:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.1},
URN = {urn:nbn:de:0030-drops-196446},
doi = {10.4230/LIPIcs.CSL.2024.1},
annote = {Keywords: lambda-calculus, computational complexity, geometry of interaction, abstract machines, intersection types}
}
Document
Invited Talk
Craig Interpolation for Decidable Fragments of First-Order Logic (Invited Talk)
Abstract
The Craig Interpolation Property (CIP) is a property of logics. It states that, for all formulas φ and ψ, if φ ⊧ ψ, then there exists an "interpolant" ϑ such that φ ⊧ ϑ and ϑ ⊧ ψ, and such that all non-logical symbols occurring in ϑ occur both in φ and in ψ. Craig [Craig, 1957] proved in 1957 that first-order logic (FO) has this property. Since then, many refinements of Craig’s result have been obtained (e.g., [Otto, 2000; Benedikt et al., 2016]). These have found applications in various areas of computer science and AI, including formal verification, modular hard/software specification and automated deduction [McMillan, 2018; Calvanese et al., 2020; Hoder et al., 2012], and more recently prominently in databases [Toman and Weddell, 2011; Benedikt et al., 2016] and knowledge representation [Lutz and Wolter, 2011; ten Cate et al., 2013; Koopmann and Schmidt, 2015]. In this invited talk, we will survey recent work pertaining to Craig interpolation for various important decidable fragment of first-order logic, including guarded fragments, finite-variable fragments, and ordered fragments. Most of these fragments lack the CIP (the guarded-negation fragment GNFO being a notable exception [Bárány et al., 2013]). We will discuss strategies that have been proposed in recent literature to deal with this lack of CIP, as well as recent results that shed light on where, within the landscape of decidable fragment of first-order logic, one may find logics that enjoy CIP [Jung and Wolter, 2021; ten Cate and Comer, 2023].
Cite as
Balder ten Cate. Craig Interpolation for Decidable Fragments of First-Order Logic (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{tencate:LIPIcs.CSL.2024.2,
author = {ten Cate, Balder},
title = {{Craig Interpolation for Decidable Fragments of First-Order Logic}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {2:1--2:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.2},
URN = {urn:nbn:de:0030-drops-196488},
doi = {10.4230/LIPIcs.CSL.2024.2},
annote = {Keywords: First-Order Logic, Decidable Fragments, Craig Interpolation}
}
Document
Invited Talk
Artificial Intelligence and Artificial Ignorance (Invited Talk)
Abstract
This invited talk first delves into the division between the two primary branches of AI research: symbolic AI, which predominantly focuses on knowledge representation and logical reasoning, and sub-symbolic AI, primarily centered on machine learning employing neural networks. We explore both the notable accomplishments and the challenges encountered in each of these approaches. We provide instances where traditional deep learning encounters limitations, and we elucidate significant obstacles in achieving automated symbolic reasoning. We then discuss the recent groundbreaking advancements in generative AI, driven by language models such as ChatGPT. We showcase instances where these models excel and, conversely, where they exhibit shortcomings and produce erroneous information. We identify and illustrate five key reasons for potential failures in language models, which include: [(i)]
1) information loss due to data compression,
2) training bias,
3) the incorporation of incorrect external data,
4) the misordering of results, and
5) the failure to detect and resolve logical inconsistencies contained in a sequence of LLM-generated prompt-answers. Lastly, we touch upon the Chat2Data project, which endeavors to leverage language models for the automated verification and enhancement of relational databases, all while mitigating the pitfalls (i)-(v) mentioned earlier.
Cite as
Georg Gottlob. Artificial Intelligence and Artificial Ignorance (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{gottlob:LIPIcs.CSL.2024.3,
author = {Gottlob, Georg},
title = {{Artificial Intelligence and Artificial Ignorance}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {3:1--3:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.3},
URN = {urn:nbn:de:0030-drops-196459},
doi = {10.4230/LIPIcs.CSL.2024.3},
annote = {Keywords: AI applications, symbolic AI, sub-symbolic AI, AI usefulness, achievements of symbolic AI, achievements of machine learning, machine learning errors and mistakes, large language models, LLMs, LLM usefulness, LLM mistakes, inaccuracies}
}
Document
Invited Talk
Approximating Fixpoints of Approximated Functions (Invited Talk)
Abstract
There is a large body of work on fixpoint theorems, guaranteeing the existence of fixpoints for certain functions and providing methods for computing them. This includes for instance Banachs’s fixpoint theorem, the well-known result by Knaster-Tarski that is frequently employed in computer science and Kleene iteration.
It is less clear how to compute fixpoints if the function whose (least) fixpoint we are interested in is not known exactly, but can only be obtained by a sequence of subsequently better approximations. This scenario occurs for instance in the context of reinforcement learning, where the probabilities of a Markov decision process (MDP) - for which one wants to learn a strategy - are unknown and can only be sampled. There are several solutions to this problem where the fixpoint computation (for determining the value vector and the optimal strategy) and the exploration of the model are interleaved. However, these methods work only well for discounted MDPs, that is in the contractive setting, but not for general MDPs, that is for non-expansive functions.
After describing and motivating the problem, we will in particular concentrate on the non-expansive case. There are many interesting systems who value vectors can be obtained by determining the fixpoints of non-expansive functions. Other than contractive functions, they do not guarantee uniqueness of the fixpoint, making it more difficult to approximate the least fixpoint by methods other than Kleene iteration. And also Kleene iteration fails if the function under consideration is only approximated.
We hence describe a dampened Mann iteration scheme for (higher-dimensional) functions on the reals that converges to the least fixpoint from everywhere. This scheme can also be adapted to functions that are approximated, under certain conditions.
We will in particular study the case of MDPs and consider a related problem that arises when performing model-checking for quantitative mu-calculi, which involves the computation of nested fixpoints.
This is joint work with Paolo Baldan, Sebastian Gurke, Tommaso Padoan and Florian Wittbold.
Cite as
Barbara König. Approximating Fixpoints of Approximated Functions (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, p. 4:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{konig:LIPIcs.CSL.2024.4,
author = {K\"{o}nig, Barbara},
title = {{Approximating Fixpoints of Approximated Functions}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {4:1--4:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.4},
URN = {urn:nbn:de:0030-drops-196469},
doi = {10.4230/LIPIcs.CSL.2024.4},
annote = {Keywords: fixpoints, approximation, Markov decision processes}
}
Document
Invited Talk
Strategy Synthesis for Partially Observable Stochastic Games with Neural Perception Mechanisms (Invited Talk)
Abstract
Strategic reasoning is essential to ensure stable multi-agent coordination in complex environments, as it enables synthesis of optimal (or near-optimal) agent strategies and equilibria that guarantee expected outcomes, even in adversarial scenarios. Partially-observable stochastic games (POSGs) are a natural model for real-world settings involving multiple agents, uncertainty and partial information, but lack practical algorithms for computing or approximating optimal values and strategies. Recently, progress has been made for one-sided POSGs, a subclass of two-agent, zero-sum POSGs where only one agent has partial information while the other agent is assumed to have full knowledge of the state, with heuristic search value iteration (HSVI) proposed for computing approximately optimal values and strategies in one-sided POSGs [Horák et al., 2023]. This model is well suited to safety-critical applications, when making worst-case assumptions about one agent; examples include the attacker in a security application, modelled, e.g., as a patrolling or pursuit-evasion game.
However, many realistic autonomous coordination scenarios involve agents perceiving continuous environments using data-driven observation functions, typically implemented as neural networks (NNs). Examples include autonomous vehicles using NNs to perform object recognition or to estimate pedestrian intention, or NN-enabled vision in an airborne pursuit-evasion scenario. Such perception mechanisms bring new challenges, notably continuous environments, which are inherently tied to NN-enabled perception because of standard training regimes. This means that naive discretisation is difficult, since decision boundaries obtained for data-driven perception are typically irregular and can be misaligned with gridding schemes for discretisation, affecting the precision of the computed strategies.
This invited paper will discuss progress with developing a model class and algorithms for one-sided POSGs with neural perception mechanisms [R. Yan et al., 2022; Yan et al., 2023] that work directly with their continuous state space. Building on continuous-state POMDPs with NN perception mechanisms [Yan et al., 2023], where the key idea is that ReLU neural network classifiers induce a finite decomposition of the continuous environment into polyhedra for each classification label, a piecewise constant representation for the value, reward and perception functions is developed that forms the basis for a variant of HSVI, a point-based solution method that computes a lower and upper bound on the value function from a given belief to compute an (approximately) optimal strategy. We extend these ideas from the single-agent (POMDP) setting [Yan et al., 2023] to zero-sum POSGs. In the game setting, this involves solving a normal form game at each stage and iteration, and goes significantly beyond HSVI for finite POSGs [Horák et al., 2023].
Cite as
Marta Kwiatkowska. Strategy Synthesis for Partially Observable Stochastic Games with Neural Perception Mechanisms (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{kwiatkowska:LIPIcs.CSL.2024.5,
author = {Kwiatkowska, Marta},
title = {{Strategy Synthesis for Partially Observable Stochastic Games with Neural Perception Mechanisms}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {5:1--5:2},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.5},
URN = {urn:nbn:de:0030-drops-196471},
doi = {10.4230/LIPIcs.CSL.2024.5},
annote = {Keywords: Stochastic games, neural networks, formal verification, strategy synthesis}
}
Document
Invited Talk
Logical Algorithmics: From Theory to Practice (Invited Talk)
Abstract
The standard approach to algorithm development is to focus on a specific problem and develop for it a specific algorithm. Codd’s introduction of the relational model in 1970 included two fundamental ideas: (1) Relations provide a universal data representation formalism, and (2) Relational databases can be queried using first-order logic. Realizing these ideas required the development of a meta-algorithm, which takes a declarative query and executes it with respect to a database. In this talk, I will describe this approach, which I call Logical Algorithmics, in detail, and explore its profound ramification.
Cite as
Moshe Y. Vardi. Logical Algorithmics: From Theory to Practice (Invited Talk). In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, p. 6:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{vardi:LIPIcs.CSL.2024.6,
author = {Vardi, Moshe Y.},
title = {{Logical Algorithmics: From Theory to Practice}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {6:1--6:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.6},
URN = {urn:nbn:de:0030-drops-196494},
doi = {10.4230/LIPIcs.CSL.2024.6},
annote = {Keywords: Logic, Algorithms}
}
Document
Semantic Bounds and Multi Types, Revisited
Abstract
Intersection types are a standard tool in operational and semantical studies of the λ-calculus. De Carvalho showed how multi types, a quantitative variant of intersection types providing a handy presentation of the relational denotational model, allows one to extract precise bounds on the number of β-steps and the size of normal forms.
In the last few years, de Carvalho’s work has been extended and adapted to a number of λ-calculi, evaluation strategies, and abstract machines. These works, however, only adapt the first part of his work, that extracts bounds from multi type derivations, while never consider the second part, which deals with extracting bounds from the multi types themselves. The reason is that this second part is more technical, and requires to reason up to type substitutions. It is however also the most interesting, because it shows that the bounding power is inherent to the relational model (which is induced by the types, without the derivations), independently of its presentation as a type system.
Here we dissect and clarify the second part of de Carvalho’s work, establishing a link with principal multi types, and isolating a key property independent of type substitutions.
Cite as
Beniamino Accattoli. Semantic Bounds and Multi Types, Revisited. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 7:1-7:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{accattoli:LIPIcs.CSL.2024.7,
author = {Accattoli, Beniamino},
title = {{Semantic Bounds and Multi Types, Revisited}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {7:1--7:24},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.7},
URN = {urn:nbn:de:0030-drops-196504},
doi = {10.4230/LIPIcs.CSL.2024.7},
annote = {Keywords: Lambda calculus, intersection types, denotational semantics, linear logic}
}
Document
Infinitary Cut-Elimination via Finite Approximations
Abstract
We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a global level by adapting a standard progressing criterion. We present an infinitary version of cut-elimination based on finite approximations, and we prove that, in presence of the progressing criterion, it returns well-defined non-wellfounded proofs at its limit. Furthermore, we show that cut-elimination preserves the progressing criterion and various regularity conditions internalizing degrees of proof-theoretical uniformity. Finally, we provide a denotational semantics for our systems based on the relational model.
Cite as
Matteo Acclavio, Gianluca Curzi, and Giulio Guerrieri. Infinitary Cut-Elimination via Finite Approximations. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{acclavio_et_al:LIPIcs.CSL.2024.8,
author = {Acclavio, Matteo and Curzi, Gianluca and Guerrieri, Giulio},
title = {{Infinitary Cut-Elimination via Finite Approximations}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {8:1--8:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.8},
URN = {urn:nbn:de:0030-drops-196510},
doi = {10.4230/LIPIcs.CSL.2024.8},
annote = {Keywords: cut-elimination, non-wellfounded proofs, parsimonious logic, linear logic, proof theory, approximation, sequent calculus, non-uniform proofs}
}
Document
Descriptive Complexity for Neural Networks via Boolean Networks
Abstract
We investigate the descriptive complexity of a class of neural networks with unrestricted topologies and piecewise polynomial activation functions. We consider the general scenario where the running time is unlimited and floating-point numbers are used for simulating reals. We characterize these neural networks with a rule-based logic for Boolean networks. In particular, we show that the sizes of the neural networks and the corresponding Boolean rule formulae are polynomially related. In fact, in the direction from Boolean rules to neural networks, the blow-up is only linear. We also analyze the delays in running times due to the translations. In the translation from neural networks to Boolean rules, the time delay is polylogarithmic in the neural network size and linear in time. In the converse translation, the time delay is linear in both factors. We also obtain translations between the rule-based logic for Boolean networks, the diamond-free fragment of modal substitution calculus and a class of recursive Boolean circuits where the number of input and output gates match.
Cite as
Veeti Ahvonen, Damian Heiman, and Antti Kuusisto. Descriptive Complexity for Neural Networks via Boolean Networks. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 9:1-9:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{ahvonen_et_al:LIPIcs.CSL.2024.9,
author = {Ahvonen, Veeti and Heiman, Damian and Kuusisto, Antti},
title = {{Descriptive Complexity for Neural Networks via Boolean Networks}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {9:1--9:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.9},
URN = {urn:nbn:de:0030-drops-196528},
doi = {10.4230/LIPIcs.CSL.2024.9},
annote = {Keywords: Descriptive complexity, neural networks, Boolean networks, floating-point arithmetic, logic}
}
Document
Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories
Abstract
We consider a minimal extension of the language of arithmetic, such that the bounded formulas provably total in a suitably-defined theory à la Buss (expressed in this new language) precisely capture polytime random functions. Then, we provide two new characterizations of the semantic class BPP obtained by internalizing the error-bound check within a logical system: the first relies on measure-sensitive quantifiers, while the second is based on standard first-order quantification. This leads us to introduce a family of effectively enumerable subclasses of BPP, called BPP_T and consisting of languages captured by those probabilistic Turing machines whose underlying error can be proved bounded in T. As a paradigmatic example of this approach, we establish that polynomial identity testing is in BPP_T, where T = IΔ₀+Exp is a well-studied theory based on bounded induction.
Cite as
Melissa Antonelli, Ugo Dal Lago, Davide Davoli, Isabel Oitavem, and Paolo Pistone. Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{antonelli_et_al:LIPIcs.CSL.2024.10,
author = {Antonelli, Melissa and Dal Lago, Ugo and Davoli, Davide and Oitavem, Isabel and Pistone, Paolo},
title = {{Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {10:1--10:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.10},
URN = {urn:nbn:de:0030-drops-196538},
doi = {10.4230/LIPIcs.CSL.2024.10},
annote = {Keywords: Bounded Arithmetic, Randomized Computation, Implicit Computational Complexity}
}
Document
Active Learning of Deterministic Transducers with Outputs in Arbitrary Monoids
Abstract
We study monoidal transducers, transition systems arising as deterministic automata whose transitions also produce outputs in an arbitrary monoid, for instance allowing outputs to commute or to cancel out. We use the categorical framework for minimization and learning of Colcombet, Petrişan and Stabile to recover the notion of minimal transducer recognizing a language, and give necessary and sufficient conditions on the output monoid for this minimal transducer to exist and be unique (up to isomorphism). The categorical framework then provides an abstract algorithm for learning it using membership and equivalence queries, and we discuss practical aspects of this algorithm’s implementation.
Cite as
Quentin Aristote. Active Learning of Deterministic Transducers with Outputs in Arbitrary Monoids. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{aristote:LIPIcs.CSL.2024.11,
author = {Aristote, Quentin},
title = {{Active Learning of Deterministic Transducers with Outputs in Arbitrary Monoids}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {11:1--11:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.11},
URN = {urn:nbn:de:0030-drops-196545},
doi = {10.4230/LIPIcs.CSL.2024.11},
annote = {Keywords: transducers, monoids, active learning, category theory}
}
Document
Extending the WMSO+U Logic with Quantification over Tuples
Abstract
We study a new extension of the weak MSO logic, talking about boundedness. Instead of a previously considered quantifier 𝖴, expressing the fact that there exist arbitrarily large finite sets satisfying a given property, we consider a generalized quantifier 𝖴, expressing the fact that there exist tuples of arbitrarily large finite sets satisfying a given property. First, we prove that the new logic WMSO+𝖴_{tup} is strictly more expressive than WMSO+𝖴. In particular, WMSO+𝖴_{tup} is able to express the so-called simultaneous unboundedness property, for which we prove that it is not expressible in WMSO+𝖴. Second, we prove that it is decidable whether the tree generated by a given higher-order recursion scheme satisfies a given sentence of WMSO+𝖴_{tup}.
Cite as
Anita Badyl and Paweł Parys. Extending the WMSO+U Logic with Quantification over Tuples. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{badyl_et_al:LIPIcs.CSL.2024.12,
author = {Badyl, Anita and Parys, Pawe{\l}},
title = {{Extending the WMSO+U Logic with Quantification over Tuples}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {12:1--12:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.12},
URN = {urn:nbn:de:0030-drops-196557},
doi = {10.4230/LIPIcs.CSL.2024.12},
annote = {Keywords: Boundedness, logic, decidability, expressivity, recursion schemes}
}
Document
A Natural Intuitionistic Modal Logic: Axiomatization and Bi-Nested Calculus
Abstract
We introduce FIK, a natural intuitionistic modal logic specified by Kripke models satisfying the condition of forward confluence. We give a complete Hilbert-style axiomatization of this logic and propose a bi-nested calculus for it. The calculus provides a decision procedure as well as a countermodel extraction: from any failed derivation of a given formula, we obtain by the calculus a finite countermodel of it directly.
Cite as
Philippe Balbiani, Han Gao, Çiğdem Gencer, and Nicola Olivetti. A Natural Intuitionistic Modal Logic: Axiomatization and Bi-Nested Calculus. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 13:1-13:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{balbiani_et_al:LIPIcs.CSL.2024.13,
author = {Balbiani, Philippe and Gao, Han and Gencer, \c{C}i\u{g}dem and Olivetti, Nicola},
title = {{A Natural Intuitionistic Modal Logic: Axiomatization and Bi-Nested Calculus}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {13:1--13:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.13},
URN = {urn:nbn:de:0030-drops-196565},
doi = {10.4230/LIPIcs.CSL.2024.13},
annote = {Keywords: Intuitionistic Modal Logic, Axiomatization, Completeness, Sequent Calculus}
}
Document
Tropical Mathematics and the Lambda-Calculus I: Metric and Differential Analysis of Effectful Programs
Abstract
We study the interpretation of the lambda-calculus in a framework based on tropical mathematics, and we show that it provides a unifying framework for two well-developed quantitative approaches to program semantics: on the one hand program metrics, based on the analysis of program sensitivity via Lipschitz conditions, on the other hand resource analysis, based on linear logic and higher-order program differentiation. To do that, we focus on the semantics arising from the relational model weighted over the tropical semiring, and we discuss its application to the study of "best case" program behavior for languages with probabilistic and non-deterministic effects. Finally, we show that a general foundation for this approach is provided by an abstract correspondence between tropical algebra and Lawvere’s theory of generalized metric spaces.
Cite as
Davide Barbarossa and Paolo Pistone. Tropical Mathematics and the Lambda-Calculus I: Metric and Differential Analysis of Effectful Programs. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{barbarossa_et_al:LIPIcs.CSL.2024.14,
author = {Barbarossa, Davide and Pistone, Paolo},
title = {{Tropical Mathematics and the Lambda-Calculus I: Metric and Differential Analysis of Effectful Programs}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {14:1--14:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.14},
URN = {urn:nbn:de:0030-drops-196577},
doi = {10.4230/LIPIcs.CSL.2024.14},
annote = {Keywords: Relational semantics, Differential lambda-calculus, Tropical semiring, Program metrics, Lawvere quantale}
}
Document
Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals
Abstract
Causal multiteam semantics is a framework where probabilistic dependencies arising from data and causation between variables can be together formalized and studied logically. We discover complete characterizations of expressivity for several logics that can express probabilistic statements, conditioning and interventionist counterfactuals. The results characterize the languages in terms of families of linear equations and closure conditions that define the corresponding classes of causal multiteams. The characterizations yield a strict hierarchy of expressive power. Finally, we present some undefinability results based on the characterizations.
Cite as
Fausto Barbero and Jonni Virtema. Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{barbero_et_al:LIPIcs.CSL.2024.15,
author = {Barbero, Fausto and Virtema, Jonni},
title = {{Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {15:1--15:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.15},
URN = {urn:nbn:de:0030-drops-196583},
doi = {10.4230/LIPIcs.CSL.2024.15},
annote = {Keywords: Interventionist counterfactuals, Multiteam semantics, Causation, Probability logic, Linear inequalities, Expressive power}
}
Document
A General Constructive Form of Higman’s Lemma
Abstract
In logic and computer science one often needs to constructivize a theorem ∀ f ∃ g.P(f,g), stating that for every infinite sequence f there is an infinite sequence g such that P(f,g). Here P is a computable predicate but g is not necessarily computable from f. In this paper we propose the following constructive version of ∀ f ∃ g.P(f,g): for every f there is a "long enough" finite prefix g₀ of g such that P(f,g₀), where "long enough" is expressed by membership to a bar which is a free parameter of the constructive version.
Our approach with bars generalises the approaches to Higman’s lemma undertaken by Coquand-Fridlender, Murthy-Russell and Schwichtenberg-Seisenberger-Wiesnet. As a first test for our bar technique, we sketch a constructive theory of well-quasi orders. This includes yet another constructive version of Higman’s lemma: that every infinite sequence of words has an infinite ascending subsequence. As compared with the previous constructive versions of Higman’s lemma, our constructive proofs are closer to the original classical proofs.
Cite as
Stefano Berardi, Gabriele Buriola, and Peter Schuster. A General Constructive Form of Higman’s Lemma. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{berardi_et_al:LIPIcs.CSL.2024.16,
author = {Berardi, Stefano and Buriola, Gabriele and Schuster, Peter},
title = {{A General Constructive Form of Higman’s Lemma}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {16:1--16:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.16},
URN = {urn:nbn:de:0030-drops-196599},
doi = {10.4230/LIPIcs.CSL.2024.16},
annote = {Keywords: intuitionistic logic, constructive mathematics, formal proof, inductive predicate, bar induction, well quasi-order, Higman’s lemma}
}
Document
Quantifiying the Robustness of Dynamical Systems. Relating Time and Space to Length and Precision
Abstract
Reasoning about dynamical systems evolving over the reals is well-known to lead to undecidability. In particular, it is known that there cannot be reachability decision procedures for first-order theories over the reals extended with even very basic functions, or for logical theories that reason about real-valued functions, or decision procedures for state reachability. This mostly comes from the fact that reachability for dynamical systems over the reals is fundamentally undecidable, as Turing machines can be embedded into (even very simple) dynamical systems.
However, various results in the literature have shown that decision procedures exist when restricting to robust systems, with a suitably-chosen notion of robustness. In particular, it has been established in the field of verification that if the state reachability is not sensitive to infinitesimal perturbations, then decision procedures for state reachability exist. In the context of logical theories over the reals, it has been established that decision procedures exist if we focus on properties not sensitive to arbitrarily small perturbations. For example by considering properties that are either true or δ-far from being true, for some δ > 0.
In this article, we first propose a unified theory explaining in a uniform framework these statements, that were established in different contexts.
More fundamentally, while all these statements are only about computability issues, we also consider complexity theory aspects. We prove that robustness to some precision is inherently related to the complexity of the decision procedure. When a system is robust, it makes sense to quantify at which level of perturbation it is. We prove that assuming robustness to a polynomial perturbation on precision leads to a characterisation of PSPACE. We prove that assuming robustness to polynomial perturbation on time or length leads to similar statements for PTIME.
In other words, precision on computations is inherently related to space complexity, while length or time of trajectories, is intrinsically related to time complexity. These statements can also be interpreted in relation to several recent results about the computational power of analogue models of computation.
Cite as
Manon Blanc and Olivier Bournez. Quantifiying the Robustness of Dynamical Systems. Relating Time and Space to Length and Precision. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 17:1-17:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{blanc_et_al:LIPIcs.CSL.2024.17,
author = {Blanc, Manon and Bournez, Olivier},
title = {{Quantifiying the Robustness of Dynamical Systems. Relating Time and Space to Length and Precision}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {17:1--17:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.17},
URN = {urn:nbn:de:0030-drops-196609},
doi = {10.4230/LIPIcs.CSL.2024.17},
annote = {Keywords: Computability, Complexity theory, Computable analysis, Verification, Decision, Robustness, Dynamical Systems, Models of computation, Analogue Computations}
}
Document
From Local to Global Optimality in Concurrent Parity Games
Abstract
We study two-player games on finite graphs. Turn-based games have many nice properties, but concurrent games are harder to tame: e.g. turn-based stochastic parity games have positional optimal strategies, whereas even basic concurrent reachability games may fail to have optimal strategies. We study concurrent stochastic parity games, and identify a local structural condition that, when satisfied at each state, guarantees existence of positional optimal strategies for both players.
Cite as
Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux. From Local to Global Optimality in Concurrent Parity Games. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 18:1-18:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{bordais_et_al:LIPIcs.CSL.2024.18,
author = {Bordais, Benjamin and Bouyer, Patricia and Le Roux, St\'{e}phane},
title = {{From Local to Global Optimality in Concurrent Parity Games}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {18:1--18:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.18},
URN = {urn:nbn:de:0030-drops-196612},
doi = {10.4230/LIPIcs.CSL.2024.18},
annote = {Keywords: Game forms, stochastic games, parity games, Blackwell/Martin values}
}
Document
Ehrenfeucht-Fraïssé Games in Semiring Semantics
Abstract
Ehrenfeucht-Fraïssé games provide a fundamental method for proving elementary equivalence (and equivalence up to a certain quantifier rank) of relational structures. We investigate the soundness and completeness of this method in the more general context of semiring semantics. Motivated originally by provenance analysis of database queries, semiring semantics evaluates logical statements not just by true or false, but by values in some commutative semiring; this can provide much more detailed information, for instance concerning the combinations of atomic facts that imply the truth of a statement, or practical information about evaluation costs, confidence scores, access levels or the number of successful evaluation strategies. There is a wide variety of different semirings that are relevant for provenance analysis, and the applicability of classical logical methods in semiring semantics may strongly depend on the algebraic properties of the underlying semiring.
While Ehrenfeucht-Fraïssé games are sound and complete for logical equivalences in classical semantics, and thus on the Boolean semiring, this is in general not the case for other semirings. We provide a detailed analysis of the soundness and completeness of model comparison games on specific semirings, not just for classical Ehrenfeucht-Fraïssé games but also for other variants based on bijections or counting.
Finally we propose a new kind of games, called homomorphism games, based on the fact that there exist locally very different semiring interpretations that can be proved to be elementarily equivalent via separating sets of homomorphisms. We prove that these homomorphism games provide a sound and complete method for logical equivalences on finite lattice semirings.
Cite as
Sophie Brinke, Erich Grädel, and Lovro Mrkonjić. Ehrenfeucht-Fraïssé Games in Semiring Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{brinke_et_al:LIPIcs.CSL.2024.19,
author = {Brinke, Sophie and Gr\"{a}del, Erich and Mrkonji\'{c}, Lovro},
title = {{Ehrenfeucht-Fra\"{i}ss\'{e} Games in Semiring Semantics}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {19:1--19:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.19},
URN = {urn:nbn:de:0030-drops-196623},
doi = {10.4230/LIPIcs.CSL.2024.19},
annote = {Keywords: Semiring semantics, elementary equivalence, Ehrenfeucht-Fra\"{i}ss\'{e} games}
}
Document
Quantum Circuit Completeness: Extensions and Simplifications
Abstract
Although quantum circuits have been ubiquitous for decades in quantum computing, the first complete equational theory for quantum circuits has only recently been introduced. Completeness guarantees that any true equation on quantum circuits can be derived from the equational theory.
We improve this completeness result in two ways: (i) We simplify the equational theory by proving that several rules can be derived from the remaining ones. In particular, two out of the three most intricate rules are removed, the third one being slightly simplified. (ii) The complete equational theory can be extended to quantum circuits with ancillae or qubit discarding, to represent respectively quantum computations using an additional workspace, and hybrid quantum computations. We show that the remaining intricate rule can be greatly simplified in these more expressive settings, leading to equational theories where all equations act on a bounded number of qubits.
The development of simple and complete equational theories for expressive quantum circuit models opens new avenues for reasoning about quantum circuits. It provides strong formal foundations for various compiling tasks such as circuit optimisation, hardware constraint satisfaction and verification.
Cite as
Alexandre Clément, Noé Delorme, Simon Perdrix, and Renaud Vilmart. Quantum Circuit Completeness: Extensions and Simplifications. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 20:1-20:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{clement_et_al:LIPIcs.CSL.2024.20,
author = {Cl\'{e}ment, Alexandre and Delorme, No\'{e} and Perdrix, Simon and Vilmart, Renaud},
title = {{Quantum Circuit Completeness: Extensions and Simplifications}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {20:1--20:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.20},
URN = {urn:nbn:de:0030-drops-196639},
doi = {10.4230/LIPIcs.CSL.2024.20},
annote = {Keywords: Quantum Circuits, Completeness, Graphical Language}
}
Document
Reverse Tangent Categories
Abstract
Previous work has shown that reverse differential categories give an abstract setting for gradient-based learning of functions between Euclidean spaces. However, reverse differential categories are not suited to handle gradient-based learning for functions between more general spaces such as smooth manifolds. In this paper, we propose a setting to handle this, which we call reverse tangent categories: tangent categories with an involution operation for their differential bundles.
Cite as
Geoffrey Cruttwell and Jean-Simon Pacaud Lemay. Reverse Tangent Categories. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{cruttwell_et_al:LIPIcs.CSL.2024.21,
author = {Cruttwell, Geoffrey and Lemay, Jean-Simon Pacaud},
title = {{Reverse Tangent Categories}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {21:1--21:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.21},
URN = {urn:nbn:de:0030-drops-196644},
doi = {10.4230/LIPIcs.CSL.2024.21},
annote = {Keywords: Tangent Categories, Reverse Tangent Categories, Reverse Differential Categories, Categorical Machine Learning}
}
Document
Intuitionistic Gödel-Löb Logic, à la Simpson: Labelled Systems and Birelational Semantics
Abstract
We derive an intuitionistic version of Gödel-Löb modal logic (GL) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, ℓIGL, by restricting a non-wellfounded labelled system for GL to have only one formula on the right. The latter is obtained using techniques from cyclic proof theory, sidestepping the barrier that GL’s usual frame condition (converse well-foundedness) is not first-order definable. While existing intuitionistic versions of GL are typically defined over only the box (and not the diamond), our presentation includes both modalities.
Our main result is that ℓIGL coincides with a corresponding semantic condition in birelational semantics: the composition of the modal relation and the intuitionistic relation is conversely well-founded. We call the resulting logic IGL. While the soundness direction is proved using standard ideas, the completeness direction is more complex and necessitates a detour through several intermediate characterisations of IGL.
Cite as
Anupam Das, Iris van der Giessen, and Sonia Marin. Intuitionistic Gödel-Löb Logic, à la Simpson: Labelled Systems and Birelational Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{das_et_al:LIPIcs.CSL.2024.22,
author = {Das, Anupam and van der Giessen, Iris and Marin, Sonia},
title = {{Intuitionistic G\"{o}del-L\"{o}b Logic, \`{a} la Simpson: Labelled Systems and Birelational Semantics}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {22:1--22:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.22},
URN = {urn:nbn:de:0030-drops-196654},
doi = {10.4230/LIPIcs.CSL.2024.22},
annote = {Keywords: provability logic, proof theory, intuitionistic modal logic, cyclic proofs, non-wellfounded proofs, proof search, cut-elimination, labelled sequents}
}
Document
Quantifiers Closed Under Partial Polymorphisms
Abstract
We study Lindström quantifiers that satisfy certain closure properties which are motivated by the study of polymorphisms in the context of constraint satisfaction problems (CSP). When the algebra of polymorphisms of a finite structure 𝔅 satisfies certain equations, this gives rise to a natural closure condition on the class of structures that map homomorphically to 𝔅. The collection of quantifiers that satisfy closure conditions arising from a fixed set of equations are rather more general than those arising as CSP. For any such conditions 𝒫, we define a pebble game that delimits the distinguishing power of the infinitary logic with all quantifiers that are 𝒫-closed. We use the pebble game to show that the problem of deciding whether a system of linear equations is solvable in ℤ / 2ℤ is not expressible in the infinitary logic with all quantifiers closed under a near-unanimity condition.
Cite as
Anuj Dawar and Lauri Hella. Quantifiers Closed Under Partial Polymorphisms. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{dawar_et_al:LIPIcs.CSL.2024.23,
author = {Dawar, Anuj and Hella, Lauri},
title = {{Quantifiers Closed Under Partial Polymorphisms}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {23:1--23:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.23},
URN = {urn:nbn:de:0030-drops-196662},
doi = {10.4230/LIPIcs.CSL.2024.23},
annote = {Keywords: generalized quantifiers, constraint satisfaction problems, pebble games, finite variable logics, descriptive complexity theory}
}
Document
The Worst-Case Complexity of Symmetric Strategy Improvement
Abstract
Symmetric strategy improvement is an algorithm introduced by Schewe et al. (ICALP 2015) that can be used to solve two-player games on directed graphs such as parity games and mean payoff games. In contrast to the usual well-known strategy improvement algorithm, it iterates over strategies of both players simultaneously. The symmetric version solves the known worst-case examples for strategy improvement quickly, however its worst-case complexity remained open.
We present a class of worst-case examples for symmetric strategy improvement on which this symmetric version also takes exponentially many steps. Remarkably, our examples exhibit this behaviour for any choice of improvement rule, which is in contrast to classical strategy improvement where hard instances are usually hand-crafted for a specific improvement rule. We present a generalized version of symmetric strategy iteration depending less rigidly on the interplay of the strategies of both players. However, it turns out it has the same shortcomings.
Cite as
Tom van Dijk, Georg Loho, and Matthew T. Maat. The Worst-Case Complexity of Symmetric Strategy Improvement. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{vandijk_et_al:LIPIcs.CSL.2024.24,
author = {van Dijk, Tom and Loho, Georg and Maat, Matthew T.},
title = {{The Worst-Case Complexity of Symmetric Strategy Improvement}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {24:1--24:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.24},
URN = {urn:nbn:de:0030-drops-196672},
doi = {10.4230/LIPIcs.CSL.2024.24},
annote = {Keywords: Parity game, Mean payoff game, Symmetric strategy improvement, Strategy improvement, Worst-case complexity}
}
Document
The Produoidal Algebra of Process Decomposition
Abstract
We characterize a universal normal produoidal category of monoidal contexts over an arbitrary monoidal category. In the same sense that a monoidal morphism represents a process, a monoidal context represents an incomplete process: a piece of a decomposition, possibly containing missing parts. In particular, symmetric monoidal contexts coincide with monoidal lenses and endow them with a novel universal property. We apply this algebraic structure to the analysis of multi-party protocols in arbitrary theories of processes.
Cite as
Matt Earnshaw, James Hefford, and Mario Román. The Produoidal Algebra of Process Decomposition. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{earnshaw_et_al:LIPIcs.CSL.2024.25,
author = {Earnshaw, Matt and Hefford, James and Rom\'{a}n, Mario},
title = {{The Produoidal Algebra of Process Decomposition}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {25:1--25:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.25},
URN = {urn:nbn:de:0030-drops-196688},
doi = {10.4230/LIPIcs.CSL.2024.25},
annote = {Keywords: monoidal categories, profunctors, lenses, duoidal categories}
}
Document
Extensions and Limits of the Specker-Blatter Theorem
Abstract
The original Specker-Blatter Theorem (1983) was formulated for classes of structures 𝒞 of one or several binary relations definable in Monadic Second Order Logic MSOL. It states that the number of such structures on the set [n] is modularly C-finite (MC-finite). In previous work we extended this to structures definable in CMSOL, MSOL extended with modular counting quantifiers. The first author also showed that the Specker-Blatter Theorem does not hold for one quaternary relation (2003).
If the vocabulary allows a constant symbol c, there are n possible interpretations on [n] for c. We say that a constant c is hard-wired if c is always interpreted by the same element j ∈ [n]. In this paper we show:
(i) The Specker-Blatter Theorem also holds for CMSOL when hard-wired constants are allowed. The proof method of Specker and Blatter does not work in this case.
(ii) The Specker-Blatter Theorem does not hold already for 𝒞 with one ternary relation definable in First Order Logic FOL. This was left open since 1983.
Using hard-wired constants allows us to show MC-finiteness of counting functions of various restricted partition functions which were not known to be MC-finite till now. Among them we have the restricted Bell numbers B_{r,A}, restricted Stirling numbers of the second kind S_{r,A} or restricted Lah-numbers L_{r,A}. Here r is an non-negative integer and A is an ultimately periodic set of non-negative integers.
Cite as
Eldar Fischer and Johann A. Makowsky. Extensions and Limits of the Specker-Blatter Theorem. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{fischer_et_al:LIPIcs.CSL.2024.26,
author = {Fischer, Eldar and Makowsky, Johann A.},
title = {{Extensions and Limits of the Specker-Blatter Theorem}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {26:1--26:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.26},
URN = {urn:nbn:de:0030-drops-196694},
doi = {10.4230/LIPIcs.CSL.2024.26},
annote = {Keywords: Specker-Blatter Theorem, Monadic Second Order Logic, MC-finiteness}
}
Document
Going Deep and Going Wide: Counting Logic and Homomorphism Indistinguishability over Graphs of Bounded Treedepth and Treewidth
Abstract
We study the expressive power of first-order logic with counting quantifiers, especially the k-variable and quantifier-rank-q fragment 𝖢^k_q, using homomorphism indistinguishability. Recently, Dawar, Jakl, and Reggio (2021) proved that two graphs satisfy the same 𝖢^k_q-sentences if and only if they are homomorphism indistinguishable over the class 𝒯^k_q of graphs admitting a k-pebble forest cover of depth q. Their proof builds on the categorical framework of game comonads developed by Abramsky, Dawar, and Wang (2017). We reprove their result using elementary techniques inspired by Dvořák (2010). Using these techniques we also give a characterisation of guarded counting logic. Our main focus, however, is to provide a graph theoretic analysis of the graph class 𝒯^k_q. This allows us to separate 𝒯^k_q from the intersection of the graph class TW_{k-1}, that is graphs of treewidth less or equal k-1, and TD_q, that is graphs of treedepth at most q if q is sufficiently larger than k. We are able to lift this separation to the semantic separation of the respective homomorphism indistinguishability relations. A part of this separation is to prove that the class TD_q is homomorphism distinguishing closed, which was already conjectured by Roberson (2022).
Cite as
Eva Fluck, Tim Seppelt, and Gian Luca Spitzer. Going Deep and Going Wide: Counting Logic and Homomorphism Indistinguishability over Graphs of Bounded Treedepth and Treewidth. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{fluck_et_al:LIPIcs.CSL.2024.27,
author = {Fluck, Eva and Seppelt, Tim and Spitzer, Gian Luca},
title = {{Going Deep and Going Wide: Counting Logic and Homomorphism Indistinguishability over Graphs of Bounded Treedepth and Treewidth}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {27:1--27:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.27},
URN = {urn:nbn:de:0030-drops-196704},
doi = {10.4230/LIPIcs.CSL.2024.27},
annote = {Keywords: Treewidth, treedepth, homomorphism indistinguishability, counting first-order logic}
}
Document
Realizability Models for Large Cardinals
Abstract
Realizabilty is a branch of logic that aims at extracting the computational content of mathematical proofs by establishing a correspondence between proofs and programs. Invented by S.C. Kleene in the 1945 to develop a connection between intuitionism and Turing computable functions, realizability has evolved to include not only classical logic but even set theory, thanks to the work of J-L. Krivine. Krivine’s work made possible to build realizability models for Zermelo-Frænkel set theory, ZF, assuming its consistency. Nevertheless, a large part of set theoretic research involves investigating further axioms that are known as large cardinals axioms; in this paper we focus on four large cardinals axioms: the axioms of (strongly) inaccessible cardinal, Mahlo cardinals, measurable cardinals and Reinhardt cardinals. We show how to build realizability models for each of these four axioms assuming their consistency relative to ZFC or ZF.
Cite as
Laura Fontanella, Guillaume Geoffroy, and Richard Matthews. Realizability Models for Large Cardinals. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{fontanella_et_al:LIPIcs.CSL.2024.28,
author = {Fontanella, Laura and Geoffroy, Guillaume and Matthews, Richard},
title = {{Realizability Models for Large Cardinals}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {28:1--28:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.28},
URN = {urn:nbn:de:0030-drops-196715},
doi = {10.4230/LIPIcs.CSL.2024.28},
annote = {Keywords: Logic, Classical Realizability, Set Theory, Large Cardinals}
}
Document
The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions
Abstract
The Kleene-Post theorem and Post’s theorem are two central and historically important results in the development of oracle computability theory, clarifying the structure of Turing reducibility degrees. They state, respectively, that there are incomparable Turing degrees and that the arithmetical hierarchy is connected to the relativised form of the halting problem defined via Turing jumps.
We study these two results in the calculus of inductive constructions (CIC), the constructive type theory underlying the Coq proof assistant. CIC constitutes an ideal foundation for the formalisation of computability theory for two reasons: First, like in other constructive foundations, computable functions can be treated via axioms as a purely synthetic notion rather than being defined in terms of a concrete analytic model of computation such as Turing machines. Furthermore and uniquely, CIC allows consistently assuming classical logic via the law of excluded middle or weaker variants on top of axioms for synthetic computability, enabling both fully classical developments and taking the perspective of constructive reverse mathematics on computability theory.
In the present paper, we give a fully constructive construction of two Turing-incomparable degrees à la Kleene-Post and observe that the classical content of Post’s theorem seems to be related to the arithmetical hierarchy of the law of excluded middle due to Akama et. al. Technically, we base our investigation on a previously studied notion of synthetic oracle computability and contribute the first consistency proof of a suitable enumeration axiom. All results discussed in the paper are mechanised and contributed to the Coq library of synthetic computability.
Cite as
Yannick Forster, Dominik Kirst, and Niklas Mück. The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{forster_et_al:LIPIcs.CSL.2024.29,
author = {Forster, Yannick and Kirst, Dominik and M\"{u}ck, Niklas},
title = {{The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {29:1--29:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.29},
URN = {urn:nbn:de:0030-drops-196728},
doi = {10.4230/LIPIcs.CSL.2024.29},
annote = {Keywords: Constructive mathematics, Computability theory, Logical foundations, Constructive type theory, Interactive theorem proving, Coq proof assistant}
}
Document
A Many-Sorted Epistemic Logic for Chromatic Hypergraphs
Abstract
We propose a many-sorted modal logic for reasoning about knowledge in multi-agent systems. Our logic introduces a clear distinction between participating agents and the environment. This allows to express local properties of agents and global properties of worlds in a uniform way, as well as to talk about the presence or absence of agents in a world. The logic subsumes the standard epistemic logic and is a conservative extension of it. The semantics is given in chromatic hypergraphs, a generalization of chromatic simplicial complexes, which were recently used to model knowledge in distributed systems. We show that the logic is sound and complete with respect to the intended semantics. We also show a further connection of chromatic hypergraphs with neighborhood frames.
Cite as
Éric Goubault, Roman Kniazev, and Jérémy Ledent. A Many-Sorted Epistemic Logic for Chromatic Hypergraphs. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 30:1-30:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{goubault_et_al:LIPIcs.CSL.2024.30,
author = {Goubault, \'{E}ric and Kniazev, Roman and Ledent, J\'{e}r\'{e}my},
title = {{A Many-Sorted Epistemic Logic for Chromatic Hypergraphs}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {30:1--30:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.30},
URN = {urn:nbn:de:0030-drops-196730},
doi = {10.4230/LIPIcs.CSL.2024.30},
annote = {Keywords: Modal logics, epistemic logics, multi-agent systems, hypergraphs}
}
Document
Remarks on Parikh-Recognizable Omega-languages
Abstract
Several variants of Parikh automata on infinite words were recently introduced by Guha et al. [FSTTCS, 2022]. We show that one of these variants coincides with blind counter machine as introduced by Fernau and Stiebe [Fundamenta Informaticae, 2008]. Fernau and Stiebe showed that every ω-language recognized by a blind counter machine is of the form ⋃_iU_iV_i^ω for Parikh recognizable languages U_i, V_i, but blind counter machines fall short of characterizing this class of ω-languages. They posed as an open problem to find a suitable automata-based characterization. We introduce several additional variants of Parikh automata on infinite words that yield automata characterizations of classes of ω-language of the form ⋃_iU_iV_i^ω for all combinations of languages U_i, V_i being regular or Parikh-recognizable. When both U_i and V_i are regular, this coincides with Büchi’s classical theorem. We study the effect of ε-transitions in all variants of Parikh automata and show that almost all of them admit ε-elimination. Finally we study the classical decision problems with applications to model checking.
Cite as
Mario Grobler, Leif Sabellek, and Sebastian Siebertz. Remarks on Parikh-Recognizable Omega-languages. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{grobler_et_al:LIPIcs.CSL.2024.31,
author = {Grobler, Mario and Sabellek, Leif and Siebertz, Sebastian},
title = {{Remarks on Parikh-Recognizable Omega-languages}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {31:1--31:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.31},
URN = {urn:nbn:de:0030-drops-196743},
doi = {10.4230/LIPIcs.CSL.2024.31},
annote = {Keywords: Parikh automata, blind counter machines, infinite words, B\"{u}chi’s theorem}
}
Document
Characterising and Verifying the Core in Concurrent Multi-Player Mean-Payoff Games
Abstract
Concurrent multi-player mean-payoff games are important models for systems of agents with individual, non-dichotomous preferences. Whilst these games have been extensively studied in terms of their equilibria in non-cooperative settings, this paper explores an alternative solution concept: the core from cooperative game theory. This concept is particularly relevant for cooperative AI systems, as it enables the modelling of cooperation among agents, even when their goals are not fully aligned. Our contribution is twofold. First, we provide a characterisation of the core using discrete geometry techniques and establish a necessary and sufficient condition for its non-emptiness. We then use the characterisation to prove the existence of polynomial witnesses in the core. Second, we use the existence of such witnesses to solve key decision problems in rational verification and provide tight complexity bounds for the problem of checking whether some/every equilibrium in a game satisfies a given LTL or GR(1) specification. Our approach is general and can be adapted to handle other specifications expressed in various fragments of LTL without incurring additional computational costs.
Cite as
Julian Gutierrez, Anthony W. Lin, Muhammad Najib, Thomas Steeples, and Michael Wooldridge. Characterising and Verifying the Core in Concurrent Multi-Player Mean-Payoff Games. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 32:1-32:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{gutierrez_et_al:LIPIcs.CSL.2024.32,
author = {Gutierrez, Julian and Lin, Anthony W. and Najib, Muhammad and Steeples, Thomas and Wooldridge, Michael},
title = {{Characterising and Verifying the Core in Concurrent Multi-Player Mean-Payoff Games}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {32:1--32:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.32},
URN = {urn:nbn:de:0030-drops-196752},
doi = {10.4230/LIPIcs.CSL.2024.32},
annote = {Keywords: Concurrent games, multi-agent systems, temporal logic, game theory}
}
Document
Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures
Abstract
We propose ωMSO⋈BAPA , an expressive logic for describing countable structures, which subsumes and transcends both Counting Monadic Second-Order Logic (CMSO) and Boolean Algebra with Presburger Arithmetic (BAPA). We show that satisfiability of ωMSO⋈BAPA is decidable over the class of labeled infinite binary trees, whereas it becomes undecidable even for a rather mild relaxations. The decidability result is established by an elaborate multi-step transformation into a particular normal form, followed by the deployment of Parikh-Muller Tree Automata, a novel kind of automaton for infinite labeled binary trees, integrating and generalizing both Muller and Parikh automata while still exhibiting a decidable (in fact PSpace-complete) emptiness problem. By means of MSO-interpretations, we lift the decidability result to all tree-interpretable classes of structures, including the classes of finite/countable structures of bounded treewidth/cliquewidth/partitionwidth. We generalize the result further by showing that decidability is even preserved when coupling width-restricted ωMSO⋈BAPA with width-unrestricted two-variable logic with advanced counting. A final showcase demonstrates how our results can be leveraged to harvest decidability results for expressive μ-calculi extended by global Presburger constraints.
Cite as
Luisa Herrmann, Vincent Peth, and Sebastian Rudolph. Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 33:1-33:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{herrmann_et_al:LIPIcs.CSL.2024.33,
author = {Herrmann, Luisa and Peth, Vincent and Rudolph, Sebastian},
title = {{Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {33:1--33:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.33},
URN = {urn:nbn:de:0030-drops-196768},
doi = {10.4230/LIPIcs.CSL.2024.33},
annote = {Keywords: MSO, BAPA, Parikh-Muller tree automata, decidability, MSO-interpretations}
}
Document
Energy Games over Totally Ordered Groups
Abstract
Kopczyński (ICALP 2006) conjectured that prefix-independent half-positional winning conditions are closed under finite unions. We refute this conjecture over finite arenas. For that, we introduce a new class of prefix-independent bi-positional winning conditions called energy conditions over totally ordered groups. We give an example of two such conditions whose union is not half-positional. We also conjecture that every prefix-independent bi-positional winning condition coincides with some energy condition over a totally ordered group on periodic sequences.
Cite as
Alexander Kozachinskiy. Energy Games over Totally Ordered Groups. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 34:1-34:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{kozachinskiy:LIPIcs.CSL.2024.34,
author = {Kozachinskiy, Alexander},
title = {{Energy Games over Totally Ordered Groups}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {34:1--34:12},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.34},
URN = {urn:nbn:de:0030-drops-196778},
doi = {10.4230/LIPIcs.CSL.2024.34},
annote = {Keywords: Games on graphs, half-positionality, ordered groups}
}
Document
QLTL Model-Checking
Abstract
Quantified LTL (QLTL) extends the temporal logic LTL with quantifications over atomic propositions. Several semantics exist to handle these quantifications, depending on the definition of executions over which formulas are interpreted: either infinite sequences of subsets of atomic propositions (aka the "tree semantics") or infinite sequences of control states combined with a labelling function that associates atomic propositions to the control states (aka the "structure semantics"). The main difference being that in the latter different occurrences of a control state should be labelled similarly. The tree semantics has been intensively studied from the complexity and expressivity point of view (especially in the work of Sistla [Sistla, 1983; Sistla et al., 1987]) for which the satisfiability and model-checking problems are known to be TOWER-complete. For the structure semantics, French has shown that the satisfiability problem is undecidable [French, 2003]. We study here the model-checking problem for QLTL under this semantics and prove that it is EXPSPACE-complete. We also show that the complexity drops down to PSPACE-complete for two specific cases of structures, namely path and flat ones.
Cite as
François Laroussinie, Loriane Leclercq, and Arnaud Sangnier. QLTL Model-Checking. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 35:1-35:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{laroussinie_et_al:LIPIcs.CSL.2024.35,
author = {Laroussinie, Fran\c{c}ois and Leclercq, Loriane and Sangnier, Arnaud},
title = {{QLTL Model-Checking}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {35:1--35:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.35},
URN = {urn:nbn:de:0030-drops-196783},
doi = {10.4230/LIPIcs.CSL.2024.35},
annote = {Keywords: Quantified Linear-time temporal logic, Model-cheking, Verification, Automata theory}
}
Document
Limitations of Game Comonads for Invertible-Map Equivalence via Homomorphism Indistinguishability
Abstract
Abramsky, Dawar, and Wang (2017) introduced the pebbling comonad for k-variable counting logic and thereby initiated a line of work that imports category theoretic machinery to finite model theory. Such game comonads have been developed for various logics, yielding characterisations of logical equivalences in terms of isomorphisms in the associated co-Kleisli category. We show a first limitation of this approach by studying linear-algebraic logic, which is strictly more expressive than first-order counting logic and whose k-variable logical equivalence relations are known as invertible-map equivalences (IM). We show that there exists no finite-rank comonad on the category of graphs whose co-Kleisli isomorphisms characterise IM-equivalence, answering a question of Ó Conghaile and Dawar (CSL 2021). We obtain this result by ruling out a characterisation of IM-equivalence in terms of homomorphism indistinguishability and employing the Lovász-type theorem for game comonads established by Reggio (2022). Two graphs are homomorphism indistinguishable over a graph class if they admit the same number of homomorphisms from every graph in the class. The IM-equivalences cannot be characterised in this way, neither when counting homomorphisms in the natural numbers, nor in any finite prime field.
Cite as
Moritz Lichter, Benedikt Pago, and Tim Seppelt. Limitations of Game Comonads for Invertible-Map Equivalence via Homomorphism Indistinguishability. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 36:1-36:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{lichter_et_al:LIPIcs.CSL.2024.36,
author = {Lichter, Moritz and Pago, Benedikt and Seppelt, Tim},
title = {{Limitations of Game Comonads for Invertible-Map Equivalence via Homomorphism Indistinguishability}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {36:1--36:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.36},
URN = {urn:nbn:de:0030-drops-196799},
doi = {10.4230/LIPIcs.CSL.2024.36},
annote = {Keywords: finite model theory, graph isomorphism, linear-algebraic logic, homomorphism indistinguishability, game comonads, invertible-map equivalence}
}
Document
Confluence of Conditional Rewriting Modulo
Abstract
We investigate confluence of rewriting with Equational Generalized Term Rewriting Systems R, consisting of Horn clauses, some of them defining conditional equations s = t ⇐ c and rewriting rules 𝓁 → r ⇐ c. In both cases, c is a sequence of atoms, possibly defined by using additional Horn clauses. Such systems include Equational Term Rewriting Systems and (join, oriented, and semi-equational) Conditional Term Rewriting Systems. A set of equations E defines an equivalence =_E and quotient set T(F,X)/=_E of terms, where reductions s →_{R/E}t using rules in R occur. For such systems, we obtain a finite set of conditional pairs π, which can be viewed as logical sentences, to prove and disprove confluence of →_{R/E} by (dis)proving joinability of such conditional pairs π.
Cite as
Salvador Lucas. Confluence of Conditional Rewriting Modulo. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 37:1-37:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{lucas:LIPIcs.CSL.2024.37,
author = {Lucas, Salvador},
title = {{Confluence of Conditional Rewriting Modulo}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {37:1--37:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.37},
URN = {urn:nbn:de:0030-drops-196809},
doi = {10.4230/LIPIcs.CSL.2024.37},
annote = {Keywords: Conditional rewriting, Confluence, Program analysis}
}
Document
A First Order Theory of Diagram Chasing
Abstract
This paper discusses the formalization of proofs "by diagram chasing", a standard technique for proving properties in abelian categories. We discuss how the essence of diagram chases can be captured by a simple many-sorted first-order theory, and we study the models and decidability of this theory. The longer-term motivation of this work is the design of a computer-aided instrument for writing reliable proofs in homological algebra, based on interactive theorem provers.
Cite as
Assia Mahboubi and Matthieu Piquerez. A First Order Theory of Diagram Chasing. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 38:1-38:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{mahboubi_et_al:LIPIcs.CSL.2024.38,
author = {Mahboubi, Assia and Piquerez, Matthieu},
title = {{A First Order Theory of Diagram Chasing}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {38:1--38:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.38},
URN = {urn:nbn:de:0030-drops-196817},
doi = {10.4230/LIPIcs.CSL.2024.38},
annote = {Keywords: Diagram chasing, formal proofs, abelian categories, decidability}
}
Document
What Monads Can and Cannot Do with a Bit of Extra Time
Abstract
The delay monad provides a way to introduce general recursion in type theory. To write programs that use a wide range of computational effects directly in type theory, we need to combine the delay monad with the monads of these effects. Here we present a first systematic study of such combinations.
We study both the coinductive delay monad and its guarded recursive cousin, giving concrete examples of combining these with well-known computational effects. We also provide general theorems stating which algebraic effects distribute over the delay monad, and which do not. Lastly, we salvage some of the impossible cases by considering distributive laws up to weak bisimilarity.
Cite as
Rasmus Ejlers Møgelberg and Maaike Annebet Zwart. What Monads Can and Cannot Do with a Bit of Extra Time. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 39:1-39:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{mgelberg_et_al:LIPIcs.CSL.2024.39,
author = {M{\o}gelberg, Rasmus Ejlers and Zwart, Maaike Annebet},
title = {{What Monads Can and Cannot Do with a Bit of Extra Time}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {39:1--39:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.39},
URN = {urn:nbn:de:0030-drops-196823},
doi = {10.4230/LIPIcs.CSL.2024.39},
annote = {Keywords: Delay Monad, Monad Compositions, Distributive Laws, Guarded Recursion, Type Theory}
}
Document
Syntactically and Semantically Regular Languages of λ-Terms Coincide Through Logical Relations
Abstract
A fundamental theme in automata theory is regular languages of words and trees, and their many equivalent definitions. Salvati has proposed a generalization to regular languages of simply typed λ-terms, defined using denotational semantics in finite sets.
We provide here some evidence for its robustness. First, we give an equivalent syntactic characterization that naturally extends the seminal work of Hillebrand and Kanellakis connecting regular languages of words and syntactic λ-definability. Second, we show that any finitary extensional model of the simply typed λ-calculus, when used in Salvati’s definition, recognizes exactly the same class of languages of λ-terms as the category of finite sets does.
The proofs of these two results rely on logical relations and can be seen as instances of a more general construction of a categorical nature, inspired by previous categorical accounts of logical relations using the gluing construction.
Cite as
Vincent Moreau and Lê Thành Dũng (Tito) Nguyễn. Syntactically and Semantically Regular Languages of λ-Terms Coincide Through Logical Relations. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 40:1-40:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{moreau_et_al:LIPIcs.CSL.2024.40,
author = {Moreau, Vincent and Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng (Tito)},
title = {{Syntactically and Semantically Regular Languages of \lambda-Terms Coincide Through Logical Relations}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {40:1--40:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.40},
URN = {urn:nbn:de:0030-drops-196831},
doi = {10.4230/LIPIcs.CSL.2024.40},
annote = {Keywords: regular languages, simple types, denotational semantics, logical relations}
}
Document
Promise and Infinite-Domain Constraint Satisfaction
Abstract
Two particularly active branches of research in constraint satisfaction are the study of promise constraint satisfaction problems (PCSPs) with finite templates and the study of infinite-domain constraint satisfaction problems with ω-categorical templates. In this paper, we explore some connections between these two hitherto unrelated fields and describe a general approach to studying the complexity of PCSPs by constructing suitable infinite CSP templates. As a result, we obtain new characterizations of the power of various classes of algorithms for PCSPs, such as first-order logic, arc consistency reductions, and obtain new proofs of the characterizations of the power of the classical linear and affine relaxations for PCSPs.
Cite as
Antoine Mottet. Promise and Infinite-Domain Constraint Satisfaction. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 41:1-41:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{mottet:LIPIcs.CSL.2024.41,
author = {Mottet, Antoine},
title = {{Promise and Infinite-Domain Constraint Satisfaction}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {41:1--41:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.41},
URN = {urn:nbn:de:0030-drops-196842},
doi = {10.4230/LIPIcs.CSL.2024.41},
annote = {Keywords: promise constraint satisfaction problems, polymorphisms, homogeneous structures, first-order logic}
}
Document
Local Operators in Topos Theory and Separation of Semi-Classical Axioms in Intuitionistic Arithmetic
Abstract
There has been work on the strength of semi-classical axioms over Heyting arithmetic such as Σ_n-DNE (double negation elimination) and Π_n-LEM (law of excluded middle). Among other things, Akama et al. show that Σ_n-DNE does not imply Π_n-LEM for any n ≥ 1 by using Kleene realizability relativized to Turing degrees. These realizability notions are expressed by subtoposes of the effective topos ℰff and thus by corresponding local operators (a.k.a. Lawvere-Tierney topologies).
Our purpose is to provide a topos-theoretic explanation for separation of semi-classical axioms. It consists of determining the least dense local operator of a given axiom φ in a topos ℰ, which completely characterizes the dense subtoposes of ℰ satisfying φ. This idea is motivated by Caramello’s study of intermediate propositional logics and van Oosten’s study of Lifschitz realizability.
We first investigate sufficient conditions for an arithmetical formula to have a least dense operator. In particular, we show that each semi-classical axiom has a least dense operator in every elementary topos with natural number object. This is a generalization of van Oosten’s result for Π₁∨Π₁-DNE in ℰff. We next determine least dense operators of semi-classical axioms in ℰff in terms of (generalized) Turing degrees. Not only does it immediately imply some separation results of Akama et al. but also explain that realizability notions they used are optimal in the sense of minimality. We finally point out a negative consequence that Π_n-LEM, Σ_n-LEM and Σ_{n+1}-DNE are never separable by any subtopos of ℰff for any n ≥ 0.
Cite as
Satoshi Nakata. Local Operators in Topos Theory and Separation of Semi-Classical Axioms in Intuitionistic Arithmetic. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 42:1-42:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{nakata:LIPIcs.CSL.2024.42,
author = {Nakata, Satoshi},
title = {{Local Operators in Topos Theory and Separation of Semi-Classical Axioms in Intuitionistic Arithmetic}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {42:1--42:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.42},
URN = {urn:nbn:de:0030-drops-196859},
doi = {10.4230/LIPIcs.CSL.2024.42},
annote = {Keywords: local operator, elementary topos, effective topos, realizability, intuitionistic arithmetic}
}
Document
Coherence by Normalization for Linear Multicategorical Structures
Abstract
We establish a formal correspondence between resource calculi and appropriate linear multicategories. We consider the cases of (symmetric) representable, symmetric closed and autonomous multicategories. For all these structures, we prove that morphisms of the corresponding free constructions can be presented by means of typed resource terms, up to a reduction relation and a structural equivalence. Thanks to the linearity of the calculi, we can prove strong normalization of the reduction by combinatorial methods, defining appropriate decreasing measures. From this, we achieve a general coherence result: morphisms that live in the free multicategorical structures are the same whenever the normal forms of the associated terms are equal. As further application, we obtain syntactic proofs of Mac Lane’s coherence theorems for (symmetric) monoidal categories.
Cite as
Federico Olimpieri. Coherence by Normalization for Linear Multicategorical Structures. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 43:1-43:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{olimpieri:LIPIcs.CSL.2024.43,
author = {Olimpieri, Federico},
title = {{Coherence by Normalization for Linear Multicategorical Structures}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {43:1--43:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.43},
URN = {urn:nbn:de:0030-drops-196865},
doi = {10.4230/LIPIcs.CSL.2024.43},
annote = {Keywords: Coherence, Linear Multicategories, Resource Calculi, Normalization}
}
Document
Conservativity of Type Theory over Higher-Order Arithmetic
Abstract
We investigate how much type theory can prove about the natural numbers. A classical result in this area shows that dependent type theory without any universes is conservative over Heyting Arithmetic (HA). We build on this result by showing that type theories with one level of impredicative universes are conservative over Higher-order Heyting Arithmetic (HAH). This result clearly depends on the specific type theory in question, however, we show that the interpretation of logic also plays a major role. For proof-irrelevant interpretations, we will see that strong versions of type theory prove exactly the same higher-order arithmetical formulas as HAH. Conversely, for proof-relevant interpretations, they prove different second-order arithmetical formulas than HAH, while still proving exactly the same first-order arithmetical formulas. Along the way, we investigate the various interpretations of logic in type theory, and to what extent dependent type theories can be seen as extensions of higher-order logic. We apply our results by proving a De Jongh’s theorem for type theory.
Cite as
Daniël Otten and Benno van den Berg. Conservativity of Type Theory over Higher-Order Arithmetic. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 44:1-44:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{otten_et_al:LIPIcs.CSL.2024.44,
author = {Otten, Dani\"{e}l and van den Berg, Benno},
title = {{Conservativity of Type Theory over Higher-Order Arithmetic}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {44:1--44:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.44},
URN = {urn:nbn:de:0030-drops-196873},
doi = {10.4230/LIPIcs.CSL.2024.44},
annote = {Keywords: Conservativity, Arithmetic, Realizability, Calculus of Inductive Constructions}
}
Document
A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic
Abstract
We study an operator on classes of languages. For each class 𝒞, it produces a new class FO²(𝕀_𝒞) associated with a variant of two-variable first-order logic equipped with a signature 𝕀_𝒞 built from 𝒞. For 𝒞 = {∅, A*}, we obtain the usual FO²(<)} logic, equipped with linear order. For 𝒞 = {∅,{ε},A+,A*}, we get the variant FO²(<,+1), which also includes the successor predicate. If 𝒞 consists of all Boolean combinations of languages A*aA*, where a is a letter, we get the variant FO²(< ,Bet), which includes "between" relations. We prove a generic algebraic characterization of the classes FO^2(𝕀_𝒞). It elegantly generalizes those known for all the cases mentioned above. Moreover, it implies that if 𝒞 has decidable separation (plus some standard properties), then FO²2(𝕀_𝒞) has a decidable membership problem.
We actually work with an equivalent definition of FO²(𝕀_𝒞) in terms of unary temporal logic. For each class 𝒞, we consider a variant TL(𝒞) of unary temporal logic whose future/past modalities depend on 𝒞 and such that TL(𝒞) = FO²(𝕀_𝒞). Finally, we also characterize FL(𝒞) and PL(𝒞), the pure-future and pure-past restrictions of TL(𝒞). Like for TL(𝒞), these characterizations imply that if 𝒞 is a class with decidable separation, then FL(𝒞) and PL(𝒞) have decidable membership.
Cite as
Thomas Place and Marc Zeitoun. A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 45:1-45:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{place_et_al:LIPIcs.CSL.2024.45,
author = {Place, Thomas and Zeitoun, Marc},
title = {{A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {45:1--45:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.45},
URN = {urn:nbn:de:0030-drops-196888},
doi = {10.4230/LIPIcs.CSL.2024.45},
annote = {Keywords: Classes of regular languages, Generalized unary temporal logic, Generalized two-variable first-order logic, Generic decidable characterizations, Membership, Separation}
}
Document
Concurrent Stochastic Lossy Channel Games
Abstract
Concurrent stochastic games are an important formalism for the rational verification of probabilistic multi-agent systems, which involves verifying whether a temporal logic property is satisfied in some or all game-theoretic equilibria of such systems. In this work, we study the rational verification of probabilistic multi-agent systems where agents can cooperate by communicating over unbounded lossy channels. To model such systems, we present concurrent stochastic lossy channel games (CSLCG) and employ an equilibrium concept from cooperative game theory known as the core, which is the most fundamental and widely studied cooperative equilibrium concept. Our main contribution is twofold. First, we show that the rational verification problem is undecidable for systems whose agents have almost-sure LTL objectives. Second, we provide a decidable fragment of such a class of objectives that subsumes almost-sure reachability and safety. Our techniques involve reductions to solving infinite-state zero-sum games with conjunctions of qualitative objectives. To the best of our knowledge, our result represents the first decidability result on the rational verification of stochastic multi-agent systems on infinite arenas.
Cite as
Daniel Stan, Muhammad Najib, Anthony Widjaja Lin, and Parosh Aziz Abdulla. Concurrent Stochastic Lossy Channel Games. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 46:1-46:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{stan_et_al:LIPIcs.CSL.2024.46,
author = {Stan, Daniel and Najib, Muhammad and Lin, Anthony Widjaja and Abdulla, Parosh Aziz},
title = {{Concurrent Stochastic Lossy Channel Games}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {46:1--46:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.46},
URN = {urn:nbn:de:0030-drops-196894},
doi = {10.4230/LIPIcs.CSL.2024.46},
annote = {Keywords: concurrent, games, stochastic, lossy channels, wqo, finite attractor property, cooperative, core, Nash equilibrium}
}
Document
Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics
Abstract
We develop a denotational semantics for general reference types in an impredicative version of guarded homotopy type theory, an adaptation of synthetic guarded domain theory to Voevodsky’s univalent foundations. We observe for the first time the profound impact of univalence on the denotational semantics of mutable state. Univalence automatically ensures that all computations are invariant under symmetries of the heap - a bountiful source of program equivalences. In particular, even the most simplistic univalent model enjoys many new equations that do not hold when the same constructions are carried out in the universes of traditional set-level (extensional) type theory.
Cite as
Jonathan Sterling, Daniel Gratzer, and Lars Birkedal. Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 47:1-47:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{sterling_et_al:LIPIcs.CSL.2024.47,
author = {Sterling, Jonathan and Gratzer, Daniel and Birkedal, Lars},
title = {{Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {47:1--47:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.47},
URN = {urn:nbn:de:0030-drops-196901},
doi = {10.4230/LIPIcs.CSL.2024.47},
annote = {Keywords: univalent foundations, homotopy type theory, impredicative encodings, synthetic guarded domain theory, guarded recursion, higher-order store, reference types}
}
Document
Guarded Hybrid Team Logics
Abstract
Team logics are extensions of first-order logic where formulae are not evaluated over assignments, but over sets ("teams") of assignments. In its most basic form, this does not increase the expressiveness of the logic because we can only form statements about the common properties of all assignments ("flatness"). Therefore, additional "team atoms" are introduced to allow for assertions about interdependencies between the assignments like dependence or inclusion. We propose to consider binders known from hybrid logic to increase the expressiveness, where the bound teams may then be referenced as regular relations. We call this hybrid team logic (HTL). Additionally, we define the positive and negative fragments of HTL (HTL^+ and HTL^-) by requiring that relations that arise from binding only occur positively or negatively, respectively.
We find that HTL and its positive and negative fragments are equivalent to prominent team logics: HTL^+ is eqivalent to inclusion logic, HTL^- is equivalent to exclusion/dependence logic and HTL itself is equivalent to independence or inclusion/exclusion logic. This classifies HTL as equivalent to existential second order logic and HTL^+ as equivalent to the positive fragment of greatest fixpoint logic.
Binders also enhance the expressiveness of guarded team logics because they enable access to information that normally is obscured by the built-in limitations of these logics. We will take a closer look at guarded hybrid team logics and establish a finite model property for the guarded fragment of HTL using model checking games. More precisely, we encode winning strategies of model checking games as relations, a process that is a natural fit for binders. Further, we notice that the hierarchy of guarded team logics is more complex than the hierarchy of non-guarded team logics, and we establish a hierarchy of prominent union-closed guarded team logics.
Cite as
Marius Tritschler. Guarded Hybrid Team Logics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 48:1-48:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@InProceedings{tritschler:LIPIcs.CSL.2024.48,
author = {Tritschler, Marius},
title = {{Guarded Hybrid Team Logics}},
booktitle = {32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
pages = {48:1--48:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-310-2},
ISSN = {1868-8969},
year = {2024},
volume = {288},
editor = {Murano, Aniello and Silva, Alexandra},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.48},
URN = {urn:nbn:de:0030-drops-196919},
doi = {10.4230/LIPIcs.CSL.2024.48},
annote = {Keywords: Team semantics, guarded logics, expressiveness, model checking games}
}