eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
1
892
10.4230/LIPIcs.CSL.2024
article
LIPIcs, Volume 288, CSL 2024, Complete Volume
Murano, Aniello
1
https://orcid.org/0000-0003-4876-3448
Silva, Alexandra
2
https://orcid.org/0000-0001-5014-9784
University of Naples Federico II, Italy
Cornell University, Ithaca, NY, USA
LIPIcs, Volume 288, CSL 2024, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024/LIPIcs.CSL.2024.pdf
LIPIcs, Volume 288, CSL 2024, Complete Volume
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
0:i
0:xiv
10.4230/LIPIcs.CSL.2024.0
article
Front Matter, Table of Contents, Preface, Conference Organization
Murano, Aniello
1
https://orcid.org/0000-0003-4876-3448
Silva, Alexandra
2
https://orcid.org/0000-0001-5014-9784
University of Naples Federico II, Italy
Cornell University, Ithaca, NY, USA
Front Matter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.0/LIPIcs.CSL.2024.0.pdf
Front Matter
Table of Contents
Preface
Conference Organization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
1:1
1:4
10.4230/LIPIcs.CSL.2024.1
article
The Ackermann Award 2023
Fernández, Maribel
1
https://orcid.org/0000-0001-8325-5815
Goubault-Larrecq, Jean
2
Kesner, Delia
3
Department of Informatics, King’s College London, UK
LSV, Ecole Normale Supérieure Paris-Saclay, France
IRIF (CNRS UMR 8243) - Université Paris Cité, France
Report on the 2023 Ackermann Award.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.1/LIPIcs.CSL.2024.1.pdf
lambda-calculus
computational complexity
geometry of interaction
abstract machines
intersection types
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
2:1
2:2
10.4230/LIPIcs.CSL.2024.2
article
Craig Interpolation for Decidable Fragments of First-Order Logic (Invited Talk)
ten Cate, Balder
1
https://orcid.org/0000-0002-2538-5846
ILLC, University of Amsterdam, The Netherlands
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].
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.2/LIPIcs.CSL.2024.2.pdf
First-Order Logic
Decidable Fragments
Craig Interpolation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
3:1
3:1
10.4230/LIPIcs.CSL.2024.3
article
Artificial Intelligence and Artificial Ignorance (Invited Talk)
Gottlob, Georg
1
2
https://orcid.org/0000-0002-2353-5230
University of Calabria, Italy
University of Oxford, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.3/LIPIcs.CSL.2024.3.pdf
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
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
4:1
4:1
10.4230/LIPIcs.CSL.2024.4
article
Approximating Fixpoints of Approximated Functions (Invited Talk)
König, Barbara
1
https://orcid.org/0000-0002-4193-2889
University of Duisburg-Essen, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.4/LIPIcs.CSL.2024.4.pdf
fixpoints
approximation
Markov decision processes
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
5:1
5:2
10.4230/LIPIcs.CSL.2024.5
article
Strategy Synthesis for Partially Observable Stochastic Games with Neural Perception Mechanisms (Invited Talk)
Kwiatkowska, Marta
1
https://orcid.org/0000-0001-9022-7599
Department of Computer Science, University of Oxford, UK
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].
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.5/LIPIcs.CSL.2024.5.pdf
Stochastic games
neural networks
formal verification
strategy synthesis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
6:1
6:1
10.4230/LIPIcs.CSL.2024.6
article
Logical Algorithmics: From Theory to Practice (Invited Talk)
Vardi, Moshe Y.
1
https://orcid.org/0000-0002-0661-5773
Rice University, Houston, TX, USA
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.6/LIPIcs.CSL.2024.6.pdf
Logic
Algorithms
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
7:1
7:24
10.4230/LIPIcs.CSL.2024.7
article
Semantic Bounds and Multi Types, Revisited
Accattoli, Beniamino
1
https://orcid.org/0000-0003-4944-9944
Inria & LIX, École Poytechnique, Palaiseau, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.7/LIPIcs.CSL.2024.7.pdf
Lambda calculus
intersection types
denotational semantics
linear logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
8:1
8:19
10.4230/LIPIcs.CSL.2024.8
article
Infinitary Cut-Elimination via Finite Approximations
Acclavio, Matteo
1
2
https://orcid.org/0000-0002-0425-2825
Curzi, Gianluca
3
4
https://orcid.org/0000-0001-8746-1704
Guerrieri, Giulio
2
https://orcid.org/0000-0002-0469-4279
University of Southern Denmark, Odense, Denmark
University of Sussex, Department of Informatics, Brighton, UK
University of Birmingham, UK
University of Gothenburg, Sweden
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.8/LIPIcs.CSL.2024.8.pdf
cut-elimination
non-wellfounded proofs
parsimonious logic
linear logic
proof theory
approximation
sequent calculus
non-uniform proofs
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
9:1
9:22
10.4230/LIPIcs.CSL.2024.9
article
Descriptive Complexity for Neural Networks via Boolean Networks
Ahvonen, Veeti
1
https://orcid.org/0009-0007-4819-0199
Heiman, Damian
1
https://orcid.org/0009-0000-6038-7006
Kuusisto, Antti
1
https://orcid.org/0000-0003-1356-8749
Tampere University, Finland
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.9/LIPIcs.CSL.2024.9.pdf
Descriptive complexity
neural networks
Boolean networks
floating-point arithmetic
logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
10:1
10:19
10.4230/LIPIcs.CSL.2024.10
article
Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories
Antonelli, Melissa
1
https://orcid.org/0009-0006-9072-4847
Dal Lago, Ugo
2
3
https://orcid.org/0000-0001-9200-070X
Davoli, Davide
3
Oitavem, Isabel
4
5
https://orcid.org/0000-0002-3573-9281
Pistone, Paolo
2
https://orcid.org/0000-0003-4250-9051
Helsinki Institute for Information Technology, Finland
Bologna University, Italy
Inria, Université Côte d'Azur, Sophia Antipolis, France
Center for Mathematics and Applications (NOVA Math), NOVA FCT, Caparica, Portugal
Department of Mathematics, NOVA FCT, Caparica, Portugal
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.10/LIPIcs.CSL.2024.10.pdf
Bounded Arithmetic
Randomized Computation
Implicit Computational Complexity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
11:1
11:20
10.4230/LIPIcs.CSL.2024.11
article
Active Learning of Deterministic Transducers with Outputs in Arbitrary Monoids
Aristote, Quentin
1
2
https://orcid.org/0009-0001-4061-7553
École Normale Supérieure de Paris, PSL University, France
Université Paris Cité, CNRS, Inria, IRIF, F-75013, Paris, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.11/LIPIcs.CSL.2024.11.pdf
transducers
monoids
active learning
category theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
12:1
12:20
10.4230/LIPIcs.CSL.2024.12
article
Extending the WMSO+U Logic with Quantification over Tuples
Badyl, Anita
1
Parys, Paweł
1
https://orcid.org/0000-0001-7247-1408
Institute of Informatics, University of Warsaw, Poland
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}.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.12/LIPIcs.CSL.2024.12.pdf
Boundedness
logic
decidability
expressivity
recursion schemes
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
13:1
13:21
10.4230/LIPIcs.CSL.2024.13
article
A Natural Intuitionistic Modal Logic: Axiomatization and Bi-Nested Calculus
Balbiani, Philippe
1
https://orcid.org/0000-0002-3569-9160
Gao, Han
2
https://orcid.org/0009-0004-1095-3347
Gencer, Çiğdem
1
https://orcid.org/0000-0002-2003-9012
Olivetti, Nicola
2
https://orcid.org/0000-0001-6254-3754
CNRS-INPT-UT3, IRIT, Toulouse, France
Aix-Marseille University, CNRS, LIS, Marseille, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.13/LIPIcs.CSL.2024.13.pdf
Intuitionistic Modal Logic
Axiomatization
Completeness
Sequent Calculus
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
14:1
14:23
10.4230/LIPIcs.CSL.2024.14
article
Tropical Mathematics and the Lambda-Calculus I: Metric and Differential Analysis of Effectful Programs
Barbarossa, Davide
1
https://orcid.org/0000-0003-4608-8282
Pistone, Paolo
1
https://orcid.org/0000-0003-4250-9051
Università di Bologna, Italy
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.14/LIPIcs.CSL.2024.14.pdf
Relational semantics
Differential lambda-calculus
Tropical semiring
Program metrics
Lawvere quantale
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
15:1
15:19
10.4230/LIPIcs.CSL.2024.15
article
Expressivity Landscape for Logics with Probabilistic Interventionist Counterfactuals
Barbero, Fausto
1
https://orcid.org/0000-0002-0959-6977
Virtema, Jonni
2
https://orcid.org/0000-0002-1582-3718
University of Helsinki, Finland
University of Sheffield, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.15/LIPIcs.CSL.2024.15.pdf
Interventionist counterfactuals
Multiteam semantics
Causation
Probability logic
Linear inequalities
Expressive power
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
16:1
16:17
10.4230/LIPIcs.CSL.2024.16
article
A General Constructive Form of Higman’s Lemma
Berardi, Stefano
1
https://orcid.org/0000-0001-5427-0020
Buriola, Gabriele
2
Schuster, Peter
2
Dipartimento di Informatica, Università di Torino, Italy
Dipartimento di Informatica, Università di Verona, Italy
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.16/LIPIcs.CSL.2024.16.pdf
intuitionistic logic
constructive mathematics
formal proof
inductive predicate
bar induction
well quasi-order
Higman’s lemma
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
17:1
17:20
10.4230/LIPIcs.CSL.2024.17
article
Quantifiying the Robustness of Dynamical Systems. Relating Time and Space to Length and Precision
Blanc, Manon
1
2
https://orcid.org/0000-0002-6961-089X
Bournez, Olivier
1
https://orcid.org/0000-0002-9218-1130
Institut Polytechnique de Paris, Ecole Polytechnique, LIX, Palaiseau, France
Université Paris-Saclay, LISN, Orsay, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.17/LIPIcs.CSL.2024.17.pdf
Computability
Complexity theory
Computable analysis
Verification
Decision
Robustness
Dynamical Systems
Models of computation
Analogue Computations
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
18:1
18:21
10.4230/LIPIcs.CSL.2024.18
article
From Local to Global Optimality in Concurrent Parity Games
Bordais, Benjamin
1
2
3
Bouyer, Patricia
1
Le Roux, Stéphane
1
Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, 91190 Gif-sur-Yvette, France
TU Dortmund University, Germany
Center for Trustworthy Data Science and Security, University Alliance Ruhr, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.18/LIPIcs.CSL.2024.18.pdf
Game forms
stochastic games
parity games
Blackwell/Martin values
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
19:1
19:22
10.4230/LIPIcs.CSL.2024.19
article
Ehrenfeucht-Fraïssé Games in Semiring Semantics
Brinke, Sophie
1
https://orcid.org/0009-0005-2865-0069
Grädel, Erich
1
https://orcid.org/0000-0002-8950-9991
Mrkonjić, Lovro
1
https://orcid.org/0000-0001-8812-7185
RWTH Aachen University, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.19/LIPIcs.CSL.2024.19.pdf
Semiring semantics
elementary equivalence
Ehrenfeucht-Fraïssé games
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
20:1
20:23
10.4230/LIPIcs.CSL.2024.20
article
Quantum Circuit Completeness: Extensions and Simplifications
Clément, Alexandre
1
https://orcid.org/0000-0002-7958-5712
Delorme, Noé
2
https://orcid.org/0000-0002-4544-9691
Perdrix, Simon
2
https://orcid.org/0000-0002-1808-2409
Vilmart, Renaud
1
https://orcid.org/0000-0002-8828-4671
Université Paris-Saclay, ENS Paris-Saclay, CNRS, Inria, LMF, 91190, Gif-sur-Yvette, France
Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.20/LIPIcs.CSL.2024.20.pdf
Quantum Circuits
Completeness
Graphical Language
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
21:1
21:21
10.4230/LIPIcs.CSL.2024.21
article
Reverse Tangent Categories
Cruttwell, Geoffrey
1
https://orcid.org/0000-0001-8742-6263
Lemay, Jean-Simon Pacaud
2
https://orcid.org/0000-0003-4124-3722
Mount Allison University, Sackville, Canada
Macquarie University, Sydney, Australia
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.21/LIPIcs.CSL.2024.21.pdf
Tangent Categories
Reverse Tangent Categories
Reverse Differential Categories
Categorical Machine Learning
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
22:1
22:18
10.4230/LIPIcs.CSL.2024.22
article
Intuitionistic Gödel-Löb Logic, à la Simpson: Labelled Systems and Birelational Semantics
Das, Anupam
1
van der Giessen, Iris
1
Marin, Sonia
1
University of Birmingham, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.22/LIPIcs.CSL.2024.22.pdf
provability logic
proof theory
intuitionistic modal logic
cyclic proofs
non-wellfounded proofs
proof search
cut-elimination
labelled sequents
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
23:1
23:19
10.4230/LIPIcs.CSL.2024.23
article
Quantifiers Closed Under Partial Polymorphisms
Dawar, Anuj
1
https://orcid.org/0000-0003-4014-8248
Hella, Lauri
2
https://orcid.org/0000-0002-9117-8124
Department of Computer Science and Technology, University of Cambridge, UK
Faculty of Information Technology and Communication Sciences, Tampere University, Finland
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.23/LIPIcs.CSL.2024.23.pdf
generalized quantifiers
constraint satisfaction problems
pebble games
finite variable logics
descriptive complexity theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
24:1
24:19
10.4230/LIPIcs.CSL.2024.24
article
The Worst-Case Complexity of Symmetric Strategy Improvement
van Dijk, Tom
1
https://orcid.org/0000-0002-5366-1051
Loho, Georg
2
https://orcid.org/0000-0001-6500-385X
Maat, Matthew T.
2
https://orcid.org/0009-0004-7361-8538
Formal Methods and Tools, University of Twente, The Netherlands
Discrete Mathematics and Mathematical Programming, University of Twente, The Netherlands
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.24/LIPIcs.CSL.2024.24.pdf
Parity game
Mean payoff game
Symmetric strategy improvement
Strategy improvement
Worst-case complexity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
25:1
25:19
10.4230/LIPIcs.CSL.2024.25
article
The Produoidal Algebra of Process Decomposition
Earnshaw, Matt
1
https://orcid.org/0000-0001-8236-2811
Hefford, James
2
https://orcid.org/0000-0002-6664-8657
Román, Mario
1
https://orcid.org/0000-0003-3158-1226
Tallinn University of Technology, Estonia
University of Oxford, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.25/LIPIcs.CSL.2024.25.pdf
monoidal categories
profunctors
lenses
duoidal categories
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
26:1
26:20
10.4230/LIPIcs.CSL.2024.26
article
Extensions and Limits of the Specker-Blatter Theorem
Fischer, Eldar
1
Makowsky, Johann A.
1
Faculty of Computer Science, Technion - Israel Institute of Technology, Haifa, Israel
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.26/LIPIcs.CSL.2024.26.pdf
Specker-Blatter Theorem
Monadic Second Order Logic
MC-finiteness
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
27:1
27:17
10.4230/LIPIcs.CSL.2024.27
article
Going Deep and Going Wide: Counting Logic and Homomorphism Indistinguishability over Graphs of Bounded Treedepth and Treewidth
Fluck, Eva
1
https://orcid.org/0000-0002-9643-6081
Seppelt, Tim
1
https://orcid.org/0000-0002-6447-0568
Spitzer, Gian Luca
1
https://orcid.org/0009-0008-0270-506X
RWTH Aachen University, Germany
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).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.27/LIPIcs.CSL.2024.27.pdf
Treewidth
treedepth
homomorphism indistinguishability
counting first-order logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
28:1
28:18
10.4230/LIPIcs.CSL.2024.28
article
Realizability Models for Large Cardinals
Fontanella, Laura
1
https://orcid.org/0000-0003-1588-7524
Geoffroy, Guillaume
2
Matthews, Richard
1
Univ. Paris Est Créteil, LACL, F-94010, France
Université Paris Cité, laboratoire IRIF, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.28/LIPIcs.CSL.2024.28.pdf
Logic
Classical Realizability
Set Theory
Large Cardinals
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
29:1
29:20
10.4230/LIPIcs.CSL.2024.29
article
The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions
Forster, Yannick
1
https://orcid.org/0000-0002-8676-9819
Kirst, Dominik
2
3
https://orcid.org/0000-0003-4126-6975
Mück, Niklas
3
4
https://orcid.org/0009-0006-9622-0762
Inria, Nantes Université, LS2N, Nantes, France
Ben-Gurion University of the Negev, Beer-Sheva, Israel
Saarland University, Saarland Informatics Campus, Saarbrücken, Germany
MPI-SWS, Saarland Informatics Campus, Saarbrücken, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.29/LIPIcs.CSL.2024.29.pdf
Constructive mathematics
Computability theory
Logical foundations
Constructive type theory
Interactive theorem proving
Coq proof assistant
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
30:1
30:18
10.4230/LIPIcs.CSL.2024.30
article
A Many-Sorted Epistemic Logic for Chromatic Hypergraphs
Goubault, Éric
1
https://orcid.org/0000-0002-3198-1863
Kniazev, Roman
1
2
3
https://orcid.org/0009-0006-7495-9793
Ledent, Jérémy
3
https://orcid.org/0000-0001-7375-4725
LIX, CNRS, École Polytechnique, IP-Paris, Palaiseau Cedex, France
Université Paris-Saclay, ENS Paris-Saclay, CNRS, LMF, 91190, Gif-Sur-Yvette, France
Université Paris Cité, CNRS, IRIF, F-75013, Paris, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.30/LIPIcs.CSL.2024.30.pdf
Modal logics
epistemic logics
multi-agent systems
hypergraphs
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
31:1
31:21
10.4230/LIPIcs.CSL.2024.31
article
Remarks on Parikh-Recognizable Omega-languages
Grobler, Mario
1
https://orcid.org/0000-0001-8103-6440
Sabellek, Leif
1
https://orcid.org/0000-0001-8051-5749
Siebertz, Sebastian
1
https://orcid.org/0000-0002-6347-1198
University of Bremen, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.31/LIPIcs.CSL.2024.31.pdf
Parikh automata
blind counter machines
infinite words
Büchi’s theorem
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
32:1
32:25
10.4230/LIPIcs.CSL.2024.32
article
Characterising and Verifying the Core in Concurrent Multi-Player Mean-Payoff Games
Gutierrez, Julian
1
Lin, Anthony W.
2
3
https://orcid.org/0000-0003-4715-5096
Najib, Muhammad
4
https://orcid.org/0000-0002-6289-5124
Steeples, Thomas
5
Wooldridge, Michael
5
Monash University, Clayton, Australia
University of Kaiserslautern-Landau, Germany
Max-Planck Institute for Software Systems, Kaiserslautern, Germany
Heriot-Watt University, Edinburgh, UK
University of Oxford, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.32/LIPIcs.CSL.2024.32.pdf
Concurrent games
multi-agent systems
temporal logic
game theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
33:1
33:19
10.4230/LIPIcs.CSL.2024.33
article
Decidable (Ac)counting with Parikh and Muller: Adding Presburger Arithmetic to Monadic Second-Order Logic over Tree-Interpretable Structures
Herrmann, Luisa
1
2
https://orcid.org/0009-0004-9532-0994
Peth, Vincent
3
https://orcid.org/0009-0007-8450-0705
Rudolph, Sebastian
1
2
https://orcid.org/0000-0002-1609-2080
Computational Logic Group, TU Dresden, Germany
Center for Scalable Data Analytics and Artificial Intelligence Dresden/Leipzig, Germany
Département d’informatique de l’ÉNS, École normale supérieure, CNRS, PSL University, Paris, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.33/LIPIcs.CSL.2024.33.pdf
MSO
BAPA
Parikh-Muller tree automata
decidability
MSO-interpretations
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
34:1
34:12
10.4230/LIPIcs.CSL.2024.34
article
Energy Games over Totally Ordered Groups
Kozachinskiy, Alexander
1
https://orcid.org/0000-0002-9956-9023
IMFD Chile & CENIA Chile, Santiago, Chile
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.34/LIPIcs.CSL.2024.34.pdf
Games on graphs
half-positionality
ordered groups
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
35:1
35:18
10.4230/LIPIcs.CSL.2024.35
article
QLTL Model-Checking
Laroussinie, François
1
Leclercq, Loriane
2
https://orcid.org/0000-0002-6254-8691
Sangnier, Arnaud
3
IRIF, Université Paris Cité, France
Ecole Centrale de Nantes, CNRS, LS2N, Nantes, France
DIBRIS, Università di Genova, Italy
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.35/LIPIcs.CSL.2024.35.pdf
Quantified Linear-time temporal logic
Model-cheking
Verification
Automata theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
36:1
36:19
10.4230/LIPIcs.CSL.2024.36
article
Limitations of Game Comonads for Invertible-Map Equivalence via Homomorphism Indistinguishability
Lichter, Moritz
1
https://orcid.org/0000-0001-5437-8074
Pago, Benedikt
2
https://orcid.org/0000-0001-6377-1230
Seppelt, Tim
1
https://orcid.org/0000-0002-6447-0568
RWTH Aachen University, Germany
University of Cambridge, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.36/LIPIcs.CSL.2024.36.pdf
finite model theory
graph isomorphism
linear-algebraic logic
homomorphism indistinguishability
game comonads
invertible-map equivalence
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
37:1
37:21
10.4230/LIPIcs.CSL.2024.37
article
Confluence of Conditional Rewriting Modulo
Lucas, Salvador
1
https://orcid.org/0000-0001-9923-2108
DSIC & VRAIN, Universitat Politècnica de València, Spain
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 π.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.37/LIPIcs.CSL.2024.37.pdf
Conditional rewriting
Confluence
Program analysis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
38:1
38:19
10.4230/LIPIcs.CSL.2024.38
article
A First Order Theory of Diagram Chasing
Mahboubi, Assia
1
2
https://orcid.org/0000-0002-0312-5461
Piquerez, Matthieu
1
https://orcid.org/0009-0002-1126-4725
Nantes Université, École Centrale Nantes, CNRS, INRIA, LS2N, UMR 6004, France
Vrije Universiteit Amsterdam, The Netherlands
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.38/LIPIcs.CSL.2024.38.pdf
Diagram chasing
formal proofs
abelian categories
decidability
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
39:1
39:18
10.4230/LIPIcs.CSL.2024.39
article
What Monads Can and Cannot Do with a Bit of Extra Time
Møgelberg, Rasmus Ejlers
1
https://orcid.org/0000-0003-0386-4376
Zwart, Maaike Annebet
1
https://orcid.org/0000-0002-0257-1574
IT University of Copenhagen, Denmark
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.39/LIPIcs.CSL.2024.39.pdf
Delay Monad
Monad Compositions
Distributive Laws
Guarded Recursion
Type Theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
40:1
40:22
10.4230/LIPIcs.CSL.2024.40
article
Syntactically and Semantically Regular Languages of λ-Terms Coincide Through Logical Relations
Moreau, Vincent
1
https://orcid.org/0009-0005-0638-1363
Nguyễn, Lê Thành Dũng (Tito)
2
https://orcid.org/0000-0002-6900-5577
IRIF & Université Paris Cité & Inria Paris, France
Laboratoire de l'informatique du parallélisme (LIP), École normale supérieure de Lyon, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.40/LIPIcs.CSL.2024.40.pdf
regular languages
simple types
denotational semantics
logical relations
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
41:1
41:19
10.4230/LIPIcs.CSL.2024.41
article
Promise and Infinite-Domain Constraint Satisfaction
Mottet, Antoine
1
https://orcid.org/0000-0002-3517-1745
Hamburg University of Technology, Research Group for Theoretical Computer Science, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.41/LIPIcs.CSL.2024.41.pdf
promise constraint satisfaction problems
polymorphisms
homogeneous structures
first-order logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
42:1
42:21
10.4230/LIPIcs.CSL.2024.42
article
Local Operators in Topos Theory and Separation of Semi-Classical Axioms in Intuitionistic Arithmetic
Nakata, Satoshi
1
Research Institute for Mathematical Sciences, Kyoto University, Japan
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.42/LIPIcs.CSL.2024.42.pdf
local operator
elementary topos
effective topos
realizability
intuitionistic arithmetic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
43:1
43:17
10.4230/LIPIcs.CSL.2024.43
article
Coherence by Normalization for Linear Multicategorical Structures
Olimpieri, Federico
1
https://orcid.org/0000-0003-1485-5360
School of Mathematics, University of Leeds, UK
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.43/LIPIcs.CSL.2024.43.pdf
Coherence
Linear Multicategories
Resource Calculi
Normalization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
44:1
44:23
10.4230/LIPIcs.CSL.2024.44
article
Conservativity of Type Theory over Higher-Order Arithmetic
Otten, Daniël
1
https://orcid.org/0000-0003-2557-3959
van den Berg, Benno
1
https://orcid.org/0000-0002-0469-0788
ILLC, University of Amsterdam, The Netherlands
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.44/LIPIcs.CSL.2024.44.pdf
Conservativity
Arithmetic
Realizability
Calculus of Inductive Constructions
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
45:1
45:23
10.4230/LIPIcs.CSL.2024.45
article
A Generic Characterization of Generalized Unary Temporal Logic and Two-Variable First-Order Logic
Place, Thomas
1
https://orcid.org/0009-0000-2840-9586
Zeitoun, Marc
1
https://orcid.org/0000-0003-4101-8437
Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400, Talence, France
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.45/LIPIcs.CSL.2024.45.pdf
Classes of regular languages
Generalized unary temporal logic
Generalized two-variable first-order logic
Generic decidable characterizations
Membership
Separation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
46:1
46:19
10.4230/LIPIcs.CSL.2024.46
article
Concurrent Stochastic Lossy Channel Games
Stan, Daniel
1
https://orcid.org/0000-0002-4723-5742
Najib, Muhammad
2
https://orcid.org/0000-0002-6289-5124
Lin, Anthony Widjaja
3
4
https://orcid.org/0000-0003-4715-5096
Abdulla, Parosh Aziz
5
https://orcid.org/0000-0001-6832-6611
EPITA, Le Kremlin-Bicêtre, France
Heriot-Watt University, Edinburgh, UK
University of Kaiserslautern-Landau, Germany
Max-Planck Institute for Software Systems, Kaiserslautern, Germany
Uppsala University, Sweden
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.46/LIPIcs.CSL.2024.46.pdf
concurrent
games
stochastic
lossy channels
wqo
finite attractor property
cooperative
core
Nash equilibrium
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
47:1
47:21
10.4230/LIPIcs.CSL.2024.47
article
Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics
Sterling, Jonathan
1
https://orcid.org/0000-0002-0585-5564
Gratzer, Daniel
2
https://orcid.org/0000-0003-1944-0789
Birkedal, Lars
2
https://orcid.org/0000-0003-1320-0098
University of Cambridge, UK
Aarhus University, Denmark
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.47/LIPIcs.CSL.2024.47.pdf
univalent foundations
homotopy type theory
impredicative encodings
synthetic guarded domain theory
guarded recursion
higher-order store
reference types
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
288
48:1
48:22
10.4230/LIPIcs.CSL.2024.48
article
Guarded Hybrid Team Logics
Tritschler, Marius
1
https://orcid.org/0009-0000-8765-2404
Technische Universität Darmstadt, Germany
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.48/LIPIcs.CSL.2024.48.pdf
Team semantics
guarded logics
expressiveness
model checking games