eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
1
684
10.4230/LIPIcs.CSL.2022
article
LIPIcs, Volume 216, CSL 2022, Complete Volume
Manea, Florin
1
https://orcid.org/0000-0001-6094-3324
Simpson, Alex
2
University of Göttingen, Germany
University of Ljubljana, Slovenia
LIPIcs, Volume 216, CSL 2022, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022/LIPIcs.CSL.2022.pdf
LIPIcs, Volume 216, CSL 2022, Complete Volume
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
0:i
0:xx
10.4230/LIPIcs.CSL.2022.0
article
Front Matter, Table of Contents, Preface, Conference Organization
Manea, Florin
1
https://orcid.org/0000-0001-6094-3324
Simpson, Alex
2
University of Göttingen, Germany
University of Ljubljana, Slovenia
Front Matter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.0/LIPIcs.CSL.2022.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
2022-01-27
216
1:1
1:15
10.4230/LIPIcs.CSL.2022.1
article
Between Deterministic and Nondeterministic Quantitative Automata (Invited Talk)
Boker, Udi
1
https://orcid.org/0000-0003-4322-8892
Reichman University, Herzliya, Israel
There is a challenging trade-off between deterministic and nondeterministic automata, where the former suit various applications better, however at the cost of being exponentially larger or even less expressive. This gave birth to many notions in between determinism and nondeterminism, aiming at enjoying, sometimes, the best of both worlds. Some of the notions are yes/no ones, for example initial nondeterminism (restricting nondeterminism to allowing several initial states), and some provide a measure of nondeterminism, for example the ambiguity level.
We analyze the possible generalization of such notions from Boolean to quantitative automata, and suggest that it depends on the following key characteristics of the considered notion 𝖭 - whether it is syntactic or semantic, and if semantic, whether it is word-based or language-based.
A syntactic notion, such as initial nondeterminism, applies as is to a quantitative automaton A, namely 𝖭(A). A word-based semantic notion, such as unambiguity, applies as is to a Boolean automaton t-A that is derived from A by accompanying it with some threshold value t ∈ ℝ, namely 𝖭(t-A). A language-based notion, such as history determinism, also applies as is to t-A, while in addition, it naturally generalizes into two different notions with respect to A itself, by either: i) taking the supremum of 𝖭(t-A) over all thresholds t, denoted by Threshold-𝖭(A); or ii) generalizing the basis of the notion from a language to a function, denoted simply by 𝖭(A). While in general 𝖭(A) ⇒ Threshold-𝖭(A) ⇒ 𝖭(t-A), we have for some notions 𝖭(A) ≡ Threshold-𝖭(A), and for some not. (For measure notions, ⇒ stands for ≥ with respect to the nondeterminism level.)
We classify numerous notions known in the Boolean setting according to their characterization above, generalize them to the quantitative setting and look into relations between them. The generalized notions open new research directions with respect to quantitative automata, and provide insights on the original notions with respect to Boolean automata.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.1/LIPIcs.CSL.2022.1.pdf
Quantitative Automata
Measure of Nondeterminism
Determinism
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
2:1
2:14
10.4230/LIPIcs.CSL.2022.2
article
How to Develop an Intuition for Risk... and Other Invisible Phenomena (Invited Talk)
Fernandes, Natasha
1
McIver, Annabelle
2
Morgan, Carroll
3
School of Engineering and IT, UNSW Canberra, Australia
Department of Computing, Macquarie University, Sydney, Australia
School of Computer Science and Engineering, UNSW, Sydney, Australia
The study of quantitative risk in security systems is often based around complex and subtle mathematical ideas involving probabilities. The notations for these ideas can pose a communication barrier between collaborating researchers even when those researchers are working within a similar framework.
This paper describes the use of geometrical representation and reasoning as a way to share ideas using the minimum of notation so as to build intuition about what kinds of properties might or might not be true. We describe a faithful geometrical setting for the channel model of quantitative information flow (QIF) and demonstrate how it can facilitate "proofs without words" for problems in the QIF setting.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.2/LIPIcs.CSL.2022.2.pdf
Geometry
Quantitative Information Flow
Proof
Explainability
Privacy
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
3:1
3:17
10.4230/LIPIcs.CSL.2022.3
article
Simulation by Rounds of Letter-To-Letter Transducers
Abu Nassar, Antonio
1
Almagor, Shaull
1
https://orcid.org/0000-0001-9021-1175
Computer Science Department, Technion, Haifa, Israel
Letter-to-letter transducers are a standard formalism for modeling reactive systems. Often, two transducers that model similar systems differ locally from one another, by behaving similarly, up to permutations of the input and output letters within "rounds". In this work, we introduce and study notions of simulation by rounds and equivalence by rounds of transducers. In our setting, words are partitioned to consecutive subwords of a fixed length k, called rounds. Then, a transducer 𝒯₁ is k-round simulated by transducer 𝒯₂ if, intuitively, for every input word x, we can permute the letters within each round in x, such that the output of 𝒯₂ on the permuted word is itself a permutation of the output of 𝒯₁ on x. Finally, two transducers are k-round equivalent if they simulate each other.
We solve two main decision problems, namely whether 𝒯₂ k-round simulates 𝒯₁ (1) when k is given as input, and (2) for an existentially quantified k.
We demonstrate the usefulness of the definitions by applying them to process symmetry: a setting in which a permutation in the identities of processes in a multi-process system naturally gives rise to two transducers, whose k-round equivalence corresponds to stability against such permutations.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.3/LIPIcs.CSL.2022.3.pdf
Transducers
Permutations
Parikh
Simulation
Equivalence
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
4:1
4:21
10.4230/LIPIcs.CSL.2022.4
article
Useful Open Call-By-Need
Accattoli, Beniamino
1
https://orcid.org/0000-0003-4944-9944
Leberle, Maico
1
Inria & École Polytechnique, Palaiseau, France
This paper studies useful sharing, which is a sophisticated optimization for λ-calculi, in the context of call-by-need evaluation in presence of open terms. Useful sharing turns out to be harder in call-by-need than in call-by-name or call-by-value, because call-by-need evaluates inside environments, making it harder to specify when a substitution step is useful. We isolate the key involved concepts and prove the correctness and the completeness of useful sharing in this setting.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.4/LIPIcs.CSL.2022.4.pdf
lambda calculus
call-by-need
operational semantics
sharing
cost models
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
5:1
5:18
10.4230/LIPIcs.CSL.2022.5
article
Gardening with the Pythia A Model of Continuity in a Dependent Setting
Baillon, Martin
1
Mahboubi, Assia
1
Pédrot, Pierre-Marie
1
INRIA and LS2N, Nantes, France
We generalize to a rich dependent type theory a proof originally developed by Escardó that all System 𝚃 functionals are continuous. It relies on the definition of a syntactic model of Baclofen Type Theory, a type theory where dependent elimination must be strict, into the Calculus of Inductive Constructions. The model is given by three translations: the axiom translation, that adds an oracle to the context; the branching translation, based on the dialogue monad, turning every type into a tree; and finally, a layer of algebraic binary parametricity, binding together the two translations. In the resulting type theory, every function f : (ℕ → ℕ) → ℕ is externally continuous.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.5/LIPIcs.CSL.2022.5.pdf
Type theory
continuity
syntactic model
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
6:1
6:16
10.4230/LIPIcs.CSL.2022.6
article
Weighted Automata and Expressions over Pre-Rational Monoids
Baudru, Nicolas
1
https://orcid.org/0000-0002-1333-3432
Dando, Louis-Marie
1
https://orcid.org/0000-0002-0199-8883
Lhote, Nathan
1
https://orcid.org/0000-0003-3303-5368
Monmege, Benjamin
1
https://orcid.org/0000-0002-4717-9955
Reynier, Pierre-Alain
1
Talbot, Jean-Marc
1
Aix Marseille Univ, CNRS, LIS, Marseille, France
The Kleene theorem establishes a fundamental link between automata and expressions over the free monoid. Numerous generalisations of this result exist in the literature; on one hand, lifting this result to a weighted setting has been widely studied. On the other hand, beyond the free monoid, different monoids can be considered: for instance, two-way automata, and even tree-walking automata, can be described by expressions using the free inverse monoid. In the present work, we aim at combining both research directions and consider weighted extensions of automata and expressions over a class of monoids that we call pre-rational, generalising both the free inverse monoid and graded monoids. The presence of idempotent elements in these pre-rational monoids leads in the weighted setting to consider infinite sums. To handle such sums, we will have to restrict ourselves to rationally additive semirings. Our main result is thus a generalisation of the Kleene theorem for pre-rational monoids and rationally additive semirings. As a corollary, we obtain a class of expressions equivalent to weighted two-way automata, as well as one for tree-walking automata.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.6/LIPIcs.CSL.2022.6.pdf
Weighted Automata and Expressions
Inverse Monoids
Two-Way Automata
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
7:1
7:17
10.4230/LIPIcs.CSL.2022.7
article
Optimal Strategies in Concurrent Reachability Games
Bordais, Benjamin
1
Bouyer, Patricia
1
Le Roux, Stéphane
1
Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, 91190 Gif-sur-Yvette, France
We study two-player reachability games on finite graphs. At each state the interaction between the players is concurrent and there is a stochastic Nature. Players also play stochastically. The literature tells us that 1) Player 𝖡, who wants to avoid the target state, has a positional strategy that maximizes the probability to win (uniformly from every state) and 2) from every state, for every ε > 0, Player 𝖠 has a strategy that maximizes up to ε the probability to win. Our work is two-fold.
First, we present a double-fixed-point procedure that says from which state Player 𝖠 has a strategy that maximizes (exactly) the probability to win. This is computable if Nature’s probability distributions are rational. We call these states maximizable. Moreover, we show that for every ε > 0, Player 𝖠 has a positional strategy that maximizes the probability to win, exactly from maximizable states and up to ε from sub-maximizable states.
Second, we consider three-state games with one main state, one target, and one bin. We characterize the local interactions at the main state that guarantee the existence of an optimal Player 𝖠 strategy. In this case there is a positional one. It turns out that in many-state games, these local interactions also guarantee the existence of a uniform optimal Player 𝖠 strategy. In a way, these games are well-behaved by design of their elementary bricks, the local interactions. It is decidable whether a local interaction has this desirable property.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.7/LIPIcs.CSL.2022.7.pdf
Concurrent reachability games
Game forms
Optimal strategies
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
8:1
8:16
10.4230/LIPIcs.CSL.2022.8
article
Finite-Memory Strategies in Two-Player Infinite Games
Bouyer, Patricia
1
Le Roux, Stéphane
1
Thomasset, Nathan
1
Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, 91190, Gif-sur-Yvette, France
We study infinite two-player win/lose games (A,B,W) where A,B are finite and W ⊆ (A×B)^ω. At each round Player 1 and Player 2 concurrently choose one action in A and B, respectively. Player 1 wins iff the generated sequence is in W. Each history h ∈ (A×B)^* induces a game (A,B,W_h) with W_h : = {ρ ∈ (A×B)^ω ∣ h ρ ∈ W}. We show the following: if W is in Δ⁰₂ (for the usual topology), if the inclusion relation induces a well partial order on the W_h’s, and if Player 1 has a winning strategy, then she has a finite-memory winning strategy. Our proof relies on inductive descriptions of set complexity, such as the Hausdorff difference hierarchy of the open sets.
Examples in Σ⁰₂ and Π⁰₂ show some tightness of our result. Our result can be translated to games on finite graphs: e.g. finite-memory determinacy of multi-energy games is a direct corollary, whereas it does not follow from recent general results on finite memory strategies.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.8/LIPIcs.CSL.2022.8.pdf
Two-player win/lose games
Infinite trees
Finite-memory winning strategies
Well partial orders
Hausdorff difference hierarchy
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
9:1
9:10
10.4230/LIPIcs.CSL.2022.9
article
Constructing the Space of Valuations of a Quasi-Polish Space as a Space of Ideals
de Brecht, Matthew
1
Kyoto University, Japan
We construct the space of valuations on a quasi-Polish space in terms of the characterization of quasi-Polish spaces as spaces of ideals of a countable transitive relation. Our construction is closely related to domain theoretical work on the probabilistic powerdomain, and helps illustrate the connections between domain theory and quasi-Polish spaces. Our approach is consistent with previous work on computable measures, and can be formalized within weak formal systems, such as subsystems of second order arithmetic.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.9/LIPIcs.CSL.2022.9.pdf
Quasi-Polish spaces
space of valuations
domain theory
measure theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
10:1
10:17
10.4230/LIPIcs.CSL.2022.10
article
On the Complexity of SPEs in Parity Games
Brice, Léonard
1
2
Raskin, Jean-François
2
van den Bogaard, Marie
3
Université Gustave Eiffel, Marne-la-Vallée, France
Université Libre de Bruxelles, Belgium
LIGM, Univ. Gustave Eiffel, CNRS, F-77454 Marne-la-Vallée, France
We study the complexity of problems related to subgame-perfect equilibria (SPEs) in infinite duration non zero-sum multiplayer games played on finite graphs with parity objectives. We present new complexity results that close gaps in the literature. Our techniques are based on a recent characterization of SPEs in prefix-independent games that is grounded on the notions of requirements and negotiation, and according to which the plays supported by SPEs are exactly the plays consistent with the requirement that is the least fixed point of the negotiation function. The new results are as follows. First, checking that a given requirement is a fixed point of the negotiation function is an NP-complete problem. Second, we show that the SPE constrained existence problem is NP-complete, this problem was previously known to be ExpTime-easy and NP-hard. Third, the SPE constrained existence problem is fixed-parameter tractable when the number of players and of colors are parameters. Fourth, deciding whether some requirement is the least fixed point of the negotiation function is complete for the second level of the Boolean hierarchy. Finally, the SPE-verification problem - that is, the problem of deciding whether there exists a play supported by a SPE that satisfies some LTL formula - is PSpace-complete, this problem was known to be ExpTime-easy and PSpace-hard.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.10/LIPIcs.CSL.2022.10.pdf
Games on graphs
subgame-perfect equilibria
parity objectives
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
11:1
11:19
10.4230/LIPIcs.CSL.2022.11
article
Synthetic Integral Cohomology in Cubical Agda
Brunerie, Guillaume
1
Ljungström, Axel
2
Mörtberg, Anders
2
https://orcid.org/0000-0001-9558-6080
Independent researcher, Stockholm, Sweden
Department of Mathematics, Stockholm University, Sweden
This paper discusses the formalization of synthetic cohomology theory in a cubical extension of Agda which natively supports univalence and higher inductive types. This enables significant simplifications of many proofs from Homotopy Type Theory and Univalent Foundations as steps that used to require long calculations now hold simply by computation. To this end, we give a new definition of the group structure for cohomology with ℤ-coefficients, optimized for efficient computations. We also invent an optimized definition of the cup product which allows us to give the first complete formalization of the axioms needed to turn the integral cohomology groups into a graded commutative ring. Using this, we characterize the cohomology groups of the spheres, torus, Klein bottle and real/complex projective planes. As all proofs are constructive we can then use Cubical Agda to distinguish between spaces by computation.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.11/LIPIcs.CSL.2022.11.pdf
Synthetic Homotopy Theory
Cohomology Theory
Cubical Agda
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
12:1
12:17
10.4230/LIPIcs.CSL.2022.12
article
On the Minimisation of Transition-Based Rabin Automata and the Chromatic Memory Requirements of Muller Conditions
Casares, Antonio
1
https://orcid.org/0000-0002-6539-2020
LaBRI, Université de Bordeaux, France
In this paper, we relate the problem of determining the chromatic memory requirements of Muller conditions with the minimisation of transition-based Rabin automata. Our first contribution is a proof of the NP-completeness of the minimisation of transition-based Rabin automata. Our second contribution concerns the memory requirements of games over graphs using Muller conditions. A memory structure is a finite state machine that implements a strategy and is updated after reading the edges of the game; the special case of chromatic memories being those structures whose update function only consider the colours of the edges. We prove that the minimal amount of chromatic memory required in games using a given Muller condition is exactly the size of a minimal Rabin automaton recognising this condition. Combining these two results, we deduce that finding the chromatic memory requirements of a Muller condition is NP-complete. This characterisation also allows us to prove that chromatic memories cannot be optimal in general, disproving a conjecture by Kopczyński.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.12/LIPIcs.CSL.2022.12.pdf
Automata on Infinite Words
Games on Graphs
Arena-Independent Memory
Complexity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
13:1
13:17
10.4230/LIPIcs.CSL.2022.13
article
Fuzzy Algebraic Theories
Castelnovo, Davide
1
Miculan, Marino
1
https://orcid.org/0000-0003-0755-3444
Department of Mathematics, Computer Science and Physics, University of Udine, Italy
In this work we propose a formal system for fuzzy algebraic reasoning. The sequent calculus we define is based on two kinds of propositions, capturing equality and existence of terms as members of a fuzzy set. We provide a sound semantics for this calculus and show that there is a notion of free model for any theory in this system, allowing us (with some restrictions) to recover models as Eilenberg-Moore algebras for some monad. We will also prove a completeness result: a formula is derivable from a given theory if and only if it is satisfied by all models of the theory. Finally, leveraging results by Milius and Urbat, we give HSP-like characterizations of subcategories of algebras which are categories of models of particular kinds of theories.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.13/LIPIcs.CSL.2022.13.pdf
categorical logic
fuzzy sets
algebraic reasoning
equational axiomatisations
monads
Eilenberg-Moore algebras
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
14:1
14:17
10.4230/LIPIcs.CSL.2022.14
article
Realising Intensional S4 and GL Modalities
Chen, Liang-Ting
1
https://orcid.org/0000-0002-3250-1331
Ko, Hsiang-Shang
1
https://orcid.org/0000-0002-2439-1048
Institute of Information Science, Academia Sinica, Taipei, Taiwan
There have been investigations into type-theoretic foundations for metaprogramming, notably Davies and Pfenning’s (2001) treatment in S4 modal logic, where code evaluating to values of type A is given the modal type Code A (□A in the original paper). Recently Kavvos (2017) extended PCF with Code A and intensional recursion, understood as the deductive form of the GL (Gödel-Löb) axiom in provability logic, but the resulting type system is logically inconsistent. Inspired by staged computation, we observe that a term of type Code A is, in general, code to be evaluated in a next stage, whereas S4 modal type theory is a special case where code can be evaluated in the current stage, and the two types of code should be discriminated. Consequently, we use two separate modalities ⊠ and □ to model S4 and GL respectively in a unified categorical framework while retaining logical consistency. Following Kavvos’ (2017) novel approach to the semantics of intensionality, we interpret the two modalities in the P-category of assemblies and trackable maps. For the GL modality □ in particular, we use guarded type theory to articulate what it means by a “next” stage and to model intensional recursion by guarded recursion together with Kleene’s second recursion theorem. Besides validating the S4 and GL axioms, our model better captures the essence of intensionality by refuting congruence (so that two extensionally equal terms may not be intensionally equal) and internal quoting (both A → □A and A → ⊠A). Our results are developed in (guarded) homotopy type theory and formalised in Agda.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.14/LIPIcs.CSL.2022.14.pdf
provability
guarded recursion
realisability
modal types
metaprogramming
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
15:1
15:17
10.4230/LIPIcs.CSL.2022.15
article
Localisable Monads
Constantin, Carmen
1
https://orcid.org/0000-0003-4508-9312
Dicaire, Nuiok
1
Heunen, Chris
1
https://orcid.org/0000-0001-7393-2640
University of Edinburgh, UK
Monads govern computational side-effects in programming semantics. A collection of monads can be combined together in a local-to-global way to handle several instances of such effects. Indexed monads and graded monads do this in a modular way. Here, instead, we start with a single monad and equip it with a fine-grained structure by using techniques from tensor topology. This provides an intrinsic theory of local computational effects without needing to know how constituent effects interact beforehand.
Specifically, any monoidal category decomposes as a sheaf of local categories over a base space. We identify a notion of localisable monads which characterises when a monad decomposes as a sheaf of monads. Equivalently, localisable monads are formal monads in an appropriate presheaf 2-category, whose algebras we characterise. Three extended examples demonstrate how localisable monads can interpret the base space as locations in a computer memory, as sites in a network of interacting agents acting concurrently, and as time in stochastic processes.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.15/LIPIcs.CSL.2022.15.pdf
Monad
Monoidal category
Presheaf
Central idempotent
Graded monad
Indexed monad
Formal monad
Strong monad
Commutative monad
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
16:1
16:18
10.4230/LIPIcs.CSL.2022.16
article
An Internal Language for Categories Enriched over Generalised Metric Spaces
Dahlqvist, Fredrik
1
Neves, Renato
2
3
University College London, UK
University of Minho, Braga, Portugal
INESC-TEC, Porto, Portugal
Programs with a continuous state space or that interact with physical processes often require notions of equivalence going beyond the standard binary setting in which equivalence either holds or does not hold. In this paper we explore the idea of equivalence taking values in a quantale 𝒱, which covers the cases of (in)equations and (ultra)metric equations among others.
Our main result is the introduction of a 𝒱-equational deductive system for linear λ-calculus together with a proof that it is sound and complete (in fact, an internal language) for a class of enriched autonomous categories. In the case of inequations, we get an internal language for autonomous categories enriched over partial orders. In the case of (ultra)metric equations, we get an internal language for autonomous categories enriched over (ultra)metric spaces.
We use our results to obtain examples of inequational and metric equational systems for higher-order programs that contain real-time and probabilistic behaviour.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.16/LIPIcs.CSL.2022.16.pdf
λ-calculus
enriched category theory
quantale
equational theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
17:1
17:17
10.4230/LIPIcs.CSL.2022.17
article
MSO Undecidability for Hereditary Classes of Unbounded Clique Width
Dawar, Anuj
1
https://orcid.org/0000-0003-4014-8248
Sankaran, Abhisekh
1
https://orcid.org/0000-0003-4474-3562
Department of Computer Science and Technology, University of Cambridge, UK
Seese’s conjecture for finite graphs states that monadic second-order logic (MSO) is undecidable on all graph classes of unbounded clique-width. We show that to establish this it would suffice to show that grids of unbounded size can be interpreted in two families of graph classes: minimal hereditary classes of unbounded clique-width; and antichains of unbounded clique-width under the induced subgraph relation. We explore all the currently known classes of the former category and establish that grids of unbounded size can indeed be interpreted in them.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.17/LIPIcs.CSL.2022.17.pdf
clique width
Seese’s conjecture
antichain
MSO interpretation
grid
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
18:1
18:19
10.4230/LIPIcs.CSL.2022.18
article
Constructive Many-One Reduction from the Halting Problem to Semi-Unification
Dudenhefner, Andrej
1
https://orcid.org/0000-0003-1104-444X
Saarland University, Saarbrücken, Germany
The undecidability of semi-unification (unification combined with matching) has been proven by Kfoury, Tiuryn, and Urzyczyn in the 1990s. The original argument is by Turing reduction from Turing machine immortality (existence of a diverging configuration).
There are several aspects of the existing work which can be improved upon. First, many-one completeness of semi-unification is not established due to the use of Turing reductions. Second, existing mechanizations do not cover a comprehensive reduction from Turing machine halting to semi-unification. Third, reliance on principles such as König’s lemma or the fan theorem does not support constructivity of the arguments.
Improving upon the above aspects, the present work gives a constructive many-one reduction from the Turing machine halting problem to semi-unification. This establishes many-one completeness of semi-unification. Computability of the reduction function, constructivity of the argument, and correctness of the argument is witnessed by an axiom-free mechanization in the Coq proof assistant. The mechanization is incorporated into the existing Coq library of undecidability proofs. Notably, the mechanization relies on a technique invented by Hooper in the 1960s for Turing machine immortality.
An immediate consequence of the present work is an alternative approach to the constructive many-one equivalence of System F typability and System F type checking, compared to the argument established in the 1990s by Wells.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.18/LIPIcs.CSL.2022.18.pdf
constructive mathematics
undecidability
mechanization
semi-unification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
19:1
19:17
10.4230/LIPIcs.CSL.2022.19
article
Dynamic Cantor Derivative Logic
Fernández-Duque, David
1
2
Montacute, Yoàv
3
Department of Mathematics, Ghent University, Belgium
Institute of Computer Science of the Czech Academy of Sciences, Prague, Czech Republic
Computer Laboratory, University of Cambridge, UK
Topological semantics for modal logic based on the Cantor derivative operator gives rise to derivative logics, also referred to as d-logics. Unlike logics based on the topological closure operator, d-logics have not previously been studied in the framework of dynamical systems, which are pairs (X,f) consisting of a topological space X equipped with a continuous function f: X → X.
We introduce the logics wK4C, K4C and GLC and show that they all have the finite Kripke model property and are sound and complete with respect to the d-semantics in this dynamical setting. In particular, we prove that wK4C is the d-logic of all dynamic topological systems, K4C is the d-logic of all T_D dynamic topological systems, and GLC is the d-logic of all dynamic topological systems based on a scattered space. We also prove a general result for the case where f is a homeomorphism, which in particular yields soundness and completeness for the corresponding systems wK4H, K4H and GLH.
The main contribution of this work is the foundation of a general proof method for finite model property and completeness of dynamic topological d-logics. Furthermore, our result for GLC constitutes the first step towards a proof of completeness for the trimodal topo-temporal language with respect to a finite axiomatisation - something known to be impossible over the class of all spaces.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.19/LIPIcs.CSL.2022.19.pdf
dynamic topological logic
Cantor derivative
temporal logic
modal logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
20:1
20:19
10.4230/LIPIcs.CSL.2022.20
article
Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory
Finkbeiner, Bernd
1
https://orcid.org/0000-0002-4280-8441
Gieseking, Manuel
2
https://orcid.org/0000-0001-9073-3002
Hecking-Harbusch, Jesko
1
https://orcid.org/0000-0003-2076-617X
Olderog, Ernst-Rüdiger
2
https://orcid.org/0000-0002-3600-2046
CISPA Helmholtz Center for Information Security, Saarbrücken, Germany
University of Oldenburg, Germany
In the synthesis of distributed systems, we automate the development of distributed programs and hardware by automatically deriving correct implementations from formal specifications. For synchronous distributed systems, the synthesis problem is well known to be undecidable. For asynchronous systems, the boundary between decidable and undecidable synthesis problems is a long-standing open question. We study the problem in the setting of Petri games, a framework for distributed systems where asynchronous processes are equipped with causal memory. Petri games extend Petri nets with a distinction between system places and environment places. The components of a distributed system are the players of the game, represented as tokens that exchange information during each synchronization. Previous decidability results for this model are limited to local winning conditions, i.e., conditions that only refer to individual components.
In this paper, we consider global winning conditions such as mutual exclusion, i.e., conditions that refer to the state of all components. We provide decidability and undecidability results for global winning conditions. First, we prove for winning conditions given as bad markings that it is decidable whether a winning strategy for the system players exists in Petri games with a bounded number of system players and one environment player. Second, we prove for winning conditions that refer to both good and bad markings that it is undecidable whether a winning strategy for the system players exists in Petri games with at least two system players and one environment player. Our results thus show that, on the one hand, it is indeed possible to use global safety specifications like mutual exclusion in the synthesis of distributed systems. However, on the other hand, adding global liveness specifications results in an undecidable synthesis problem for almost all Petri games.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.20/LIPIcs.CSL.2022.20.pdf
Synthesis
distributed systems
reactive systems
Petri games
decidability
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
21:1
21:19
10.4230/LIPIcs.CSL.2022.21
article
Inferring Symbolic Automata
Fisman, Dana
1
Frenkel, Hadar
2
Zilles, Sandra
3
Ben-Gurion University, Be’er Sheva, Israel
CISPA Helmholtz Center for Information Security, Saarbrücken, Germany
University of Regina, Canada
We study the learnability of symbolic finite state automata, a model shown useful in many applications in software verification. The state-of-the-art literature on this topic follows the query learning paradigm, and so far all obtained results are positive. We provide a necessary condition for efficient learnability of SFAs in this paradigm, from which we obtain the first negative result. The main focus of our work lies in the learnability of SFAs under the paradigm of identification in the limit using polynomial time and data. We provide a necessary condition and a sufficient condition for efficient learnability of SFAs in this paradigm, from which we derive a positive and a negative result.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.21/LIPIcs.CSL.2022.21.pdf
Symbolic Finite State Automata
Query Learning
Characteristic Sets
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
22:1
22:18
10.4230/LIPIcs.CSL.2022.22
article
Differential Games, Locality, and Model Checking for FO Logic of Graphs
Gajarský, Jakub
1
Gorsky, Maximilian
2
Kreutzer, Stephan
2
University of Warsaw, Poland
TU Berlin, Germany
We introduce differential games for FO logic of graphs, a variant of Ehrenfeucht-Fraïssé games in which the game is played on only one graph and the moves of both players are restricted. We prove that these games are strong enough to capture essential information about graphs from graph classes which are interpretable in nowhere dense graph classes. This, together with the newly introduced notion of differential locality and the fact that the restriction of possible moves by the players makes it easy to decide the winner of the game in some cases, leads to a new approach to the FO model checking problem which can be used on various graph classes interpretable in classes of sparse graphs.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.22/LIPIcs.CSL.2022.22.pdf
FO model checking
locality
Gaifman’s theorem
EF games
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
23:1
23:18
10.4230/LIPIcs.CSL.2022.23
article
Cyclic Proofs for Transfinite Expressions
Hazard, Emile
1
Kuperberg, Denis
2
https://orcid.org/0000-0001-5406-717X
LIP, ENS Lyon, France
CNRS, LIP, ENS Lyon, France
We introduce a cyclic proof system for proving inclusions of transfinite expressions, describing languages of words of ordinal length. We show that recognising valid cyclic proofs is decidable, that our system is sound and complete, and well-behaved with respect to cuts. Moreover, cyclic proofs can be effectively computed from expressions inclusions. We show how to use this to obtain a Pspace algorithm for transfinite expression inclusion.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.23/LIPIcs.CSL.2022.23.pdf
transfinite expressions
transfinite automata
cyclic proofs
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
24:1
24:23
10.4230/LIPIcs.CSL.2022.24
article
Decidability for Sturmian Words
Hieronymi, Philipp
1
2
Ma, Dun
1
Oei, Reed
1
Schaeffer, Luke
3
Schulz, Christian
1
Shallit, Jeffrey
4
Department of Mathematics, University of Illinois at Urbana-Champaign, IL, USA
Mathematisches Institut, Universität Bonn, Germany
Institute for Quantum Computing, University of Waterloo, Canada
School of Computer Science, University of Waterloo, Canada
We show that the first-order theory of Sturmian words over Presburger arithmetic is decidable. Using a general adder recognizing addition in Ostrowski numeration systems by Baranwal, Schaeffer and Shallit, we prove that the first-order expansions of Presburger arithmetic by a single Sturmian word are uniformly ω-automatic, and then deduce the decidability of the theory of the class of such structures. Using an implementation of this decision algorithm called Pecan, we automatically reprove classical theorems about Sturmian words in seconds, and are able to obtain new results about antisquares and antipalindromes in characteristic Sturmian words.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.24/LIPIcs.CSL.2022.24.pdf
Decidability
Sturmian words
Ostrowski numeration systems
Automated theorem proving
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
25:1
25:18
10.4230/LIPIcs.CSL.2022.25
article
Games, Mobile Processes, and Functions
Jaber, Guilhem
1
Sangiorgi, Davide
2
3
Université de Nantes, France
Università di Bologna, Italy
Inria Sophia Antipolis, France
We establish a tight connection between two models of the λ-calculus, namely Milner’s encoding into the π-calculus (precisely, the Internal π-calculus), and operational game semantics (OGS). We first investigate the operational correspondence between the behaviours of the encoding provided by π and OGS.
We do so for various LTSs: the standard LTS for π and a new "concurrent" LTS for OGS; an "output-prioritised" LTS for π and the standard alternating LTS for OGS. We then show that the equivalences induced on λ-terms by all these LTSs (for π and OGS) coincide.
These connections allow us to transfer results and techniques between π and OGS. In particular we import up-to techniques from π onto OGS and we derive congruence and compositionality results for OGS from those of π. The study is illustrated for call-by-value; similar results hold for call-by-name.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.25/LIPIcs.CSL.2022.25.pdf
λ-calculus
π-calculus
game semantics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
26:1
26:16
10.4230/LIPIcs.CSL.2022.26
article
Parallelism in Soft Linear Logic
Jacobé de Naurois, Paulin
1
CNRS, Université Paris 13, Sorbonne Paris Cité, LIPN, UMR 7030, F-93430 Villetaneuse, France
We extend the Soft Linear Logic of Lafont with a new kind of modality, called parallel. Contractions on parallel modalities are only allowed in the cut and the left ⊸ rules, in a controlled, uniformly distributive way. We show that SLL, extended with this parallel modality, is sound and complete for PSPACE. We propose a corresponding typing discipline for the λ-calculus, extending the STA typing system of Gaboardi and Ronchi, and establish its PSPACE soundness and completeness. The use of the parallel modality in the cut-rule drives a polynomial-time, parallel call-by-value evaluation strategy of the terms.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.26/LIPIcs.CSL.2022.26.pdf
Implicit Complexity
Typing
Linear Logic
Functional Programming
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
27:1
27:20
10.4230/LIPIcs.CSL.2022.27
article
Encoding Tight Typing in a Unified Framework
Kesner, Delia
1
2
https://orcid.org/0000-0003-4254-3129
Viso, Andrés
3
https://orcid.org/0000-0002-6822-8453
Université de Paris, CNRS, IRIF, France
Institut Universitaire de France (IUF), France
Inria, Paris, France
This paper explores how the intersection type theories of call-by-name (CBN) and call-by-value (CBV) can be unified in a more general framework provided by call-by-push-value (CBPV). Indeed, we propose tight type systems for CBN and CBV that can be both encoded in a unique tight type system for CBPV. All such systems are quantitative, i.e. they provide exact information about the length of normalization sequences to normal form as well as the size of these normal forms. Moreover, the length of reduction sequences are discriminated according to their multiplicative and exponential nature, a concept inherited from linear logic. Last but not least, it is possible to extract quantitative measures for CBN and CBV from their corresponding encodings in CBPV.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.27/LIPIcs.CSL.2022.27.pdf
Call-by-Push-Value
Call-by-Name
Call-by-Value
Intersection Types
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
28:1
28:17
10.4230/LIPIcs.CSL.2022.28
article
Generalized Universe Hierarchies and First-Class Universe Levels
Kovács, András
1
https://orcid.org/0000-0002-6375-9781
Eötvös Loránd University, Budapest, Hungary
In type theories, universe hierarchies are commonly used to increase the expressive power of the theory while avoiding inconsistencies arising from size issues. There are numerous ways to specify universe hierarchies, and theories may differ in details of cumulativity, choice of universe levels, specification of type formers and eliminators, and available internal operations on levels. In the current work, we aim to provide a framework which covers a large part of the design space. First, we develop syntax and semantics for cumulative universe hierarchies, where levels may come from any set equipped with a transitive well-founded ordering. In the semantics, we show that induction-recursion can be used to model transfinite hierarchies, and also support lifting operations on type codes which strictly preserve type formers. Then, we consider a setup where universe levels are first-class types and subject to arbitrary internal reasoning. This generalizes the bounded polymorphism features of Coq and at the same time the internal level computations in Agda.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.28/LIPIcs.CSL.2022.28.pdf
type theory
universes
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
29:1
29:18
10.4230/LIPIcs.CSL.2022.29
article
Succinct Graph Representations of μ-Calculus Formulas
Kupke, Clemens
1
Marti, Johannes
2
Venema, Yde
2
University of Strathclyde, UK
University of Amsterdam, The Netherlands
Many algorithmic results on the modal mu-calculus use representations of formulas such as alternating tree automata or hierarchical equation systems. At closer inspection, these results are not always optimal, since the exact relation between the formula and its representation is not clearly understood. In particular, there has been confusion about the definition of the fundamental notion of the size of a mu-calculus formula.
We propose the notion of a parity formula as a natural way of representing a mu-calculus formula, and as a yardstick for measuring its complexity. We discuss the close connection of this concept with alternating tree automata, hierarchical equation systems and parity games. We show that well-known size measures for mu-calculus formulas correspond to a parity formula representation of the formula using its syntax tree, subformula graph or closure graph, respectively. Building on work by Bruse, Friedmann & Lange we argue that for optimal complexity results one needs to work with the closure graph, and thus define the size of a formula in terms of its Fischer-Ladner closure. As a new observation, we show that the common assumption of a formula being clean, that is, with every variable bound in at most one subformula, incurs an exponential blow-up of the size of the closure.
To realise the optimal upper complexity bound of model checking for all formulas, our main result is to provide a construction of a parity formula that (a) is based on the closure graph of a given formula, (b) preserves the alternation-depth but (c) does not assume the input formula to be clean.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.29/LIPIcs.CSL.2022.29.pdf
modal mu-calculus
model checking
alternating tree automata
hierachical equation systems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
30:1
30:17
10.4230/LIPIcs.CSL.2022.30
article
Spatial Existential Positive Logics for Hyperedge Replacement Grammars
Nakamura, Yoshiki
1
https://orcid.org/0000-0003-4106-0408
Tokyo Institute of Technology, Japan
We study a (first-order) spatial logic based on graphs of conjunctive queries for expressing (hyper-)graph languages. In this logic, each primitive positive (resp. existential positive) formula plays a role of an expression of a graph (resp. a finite language of graphs) modulo graph isomorphism. First, this paper presents a sound- and complete axiomatization for the equational theory of primitive/existential positive formulas under this spatial semantics. Second, we show Kleene theorems between this logic and hyperedge replacement grammars (HRGs), namely that over graphs, the class of existential positive first-order (resp. least fixpoint, transitive closure) formulas has the same expressive power as that of non-recursive (resp. all, linear) HRGs.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.30/LIPIcs.CSL.2022.30.pdf
Existential positive logic
spatial logic
Kleene theorem
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
31:1
31:16
10.4230/LIPIcs.CSL.2022.31
article
Structural Properties of the First-Order Transduction Quasiorder
Nešetřil, Jaroslav
1
https://orcid.org/0000-0002-5133-5586
Ossona de Mendez, Patrice
2
3
https://orcid.org/0000-0003-0724-3729
Siebertz, Sebastian
4
https://orcid.org/0000-0002-6347-1198
Computer Science Institute, Charles University (IUUK), Prague, Czech Republic
Centre d'Analyse et de Mathématiques Sociales (CNRS, UMR 8557), Paris, France
Computer Science Institute, Charles University, Prague, Czech Republic
University of Bremen, Germany
Logical transductions provide a very useful tool to encode classes of structures inside other classes of structures. In this paper we study first-order (FO) transductions and the quasiorder they induce on infinite classes of finite graphs. Surprisingly, this quasiorder is very complex, though shaped by the locality properties of first-order logic. This contrasts with the conjectured simplicity of the monadic second order (MSO) transduction quasiorder. We first establish a local normal form for FO transductions, which is of independent interest. Then we prove that the quotient partial order is a bounded distributive join-semilattice, and that the subposet of additive classes is also a bounded distributive join-semilattice. The FO transduction quasiorder has a great expressive power, and many well studied class properties can be defined using it. We apply these structural properties to prove, among other results, that FO transductions of the class of paths are exactly perturbations of classes with bounded bandwidth, that the local variants of monadic stability and monadic dependence are equivalent to their (standard) non-local versions, and that the classes with pathwidth at most k, for k ≥ 1 form a strict hierarchy in the FO transduction quasiorder.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.31/LIPIcs.CSL.2022.31.pdf
Finite model theory
first-order transductions
structural graph theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
32:1
32:17
10.4230/LIPIcs.CSL.2022.32
article
BV and Pomset Logic Are Not the Same
Nguyễn, Lê Thành Dũng (Tito)
1
https://orcid.org/0000-0002-6900-5577
Straßburger, Lutz
2
https://orcid.org/0000-0003-4661-6540
CNRS & IRISA, Rennes, France
Inria Saclay & École Polytechnique, Palaiseau, France
BV and pomset logic are two logics that both conservatively extend unit-free multiplicative linear logic by a third binary connective, which (i) is non-commutative, (ii) is self-dual, and (iii) lies between the "par" and the "tensor". It was conjectured early on (more than 20 years ago), that these two logics, that share the same language, that both admit cut elimination, and whose connectives have essentially the same properties, are in fact the same. In this paper we show that this is not the case. We present a formula that is provable in pomset logic but not in BV.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.32/LIPIcs.CSL.2022.32.pdf
proof nets
deep inference
pomset logic
system BV
cographs
dicographs
series-parallel orders
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
33:1
33:18
10.4230/LIPIcs.CSL.2022.33
article
Revisiting Parameter Synthesis for One-Counter Automata
Pérez, Guillermo A.
1
https://orcid.org/0000-0002-1200-4952
Raha, Ritam
2
3
https://orcid.org/0000-0003-1467-1182
University of Antwerp, Flanders Make, Belgium
University of Antwerp, Belgium
LaBRI, University of Bordeaux, France
We study the synthesis problem for one-counter automata with parameters. One-counter automata are obtained by extending classical finite-state automata with a counter whose value can range over non-negative integers and be tested for zero. The updates and tests applicable to the counter can further be made parametric by introducing a set of integer-valued variables called parameters. The synthesis problem for such automata asks whether there exists a valuation of the parameters such that all infinite runs of the automaton satisfy some ω-regular property. Lechner showed that (the complement of) the problem can be encoded in a restricted one-alternation fragment of Presburger arithmetic with divisibility. In this work (i) we argue that said fragment, called ∀∃_RPAD^+, is unfortunately undecidable. Nevertheless, by a careful re-encoding of the problem into a decidable restriction of ∀∃_RPAD^+, (ii) we prove that the synthesis problem is decidable in general and in 2NEXP for several fixed ω-regular properties. Finally, (iii) we give polynomial-space algorithms for the special cases of the problem where parameters can only be used in counter tests.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.33/LIPIcs.CSL.2022.33.pdf
Parametric one-counter automata
Reachability
Software Verification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
34:1
34:17
10.4230/LIPIcs.CSL.2022.34
article
First-Order Logic with Connectivity Operators
Schirrmacher, Nicole
1
https://orcid.org/0000-0002-1740-7478
Siebertz, Sebastian
1
https://orcid.org/0000-0002-6347-1198
Vigny, Alexandre
1
https://orcid.org/0000-0002-4298-8876
University of Bremen, Germany
First-order logic (FO) can express many algorithmic problems on graphs, such as the independent set and dominating set problem parameterized by solution size. On the other hand, FO cannot express the very simple algorithmic question whether two vertices are connected. We enrich FO with connectivity predicates that are tailored to express algorithmic graph properties that are commonly studied in parameterized algorithmics. By adding the atomic predicates conn_k(x,y,z_1,…,z_k) that hold true in a graph if there exists a path between (the valuations of) x and y after (the valuations of) z_1,…,z_k have been deleted, we obtain separator logic FO+conn. We show that separator logic can express many interesting problems such as the feedback vertex set problem and elimination distance problems to first-order definable classes. Denote by FO+conn_k the fragment of separator logic that is restricted to connectivity predicates with at most k+2 variables (that is, at most k deletions). We show that FO+conn_{k+1} is strictly more expressive than FO+conn_k for all k ≥ 0. We then study the limitations of separator logic and prove that it cannot express planarity, and, in particular, not the disjoint paths problem. We obtain the stronger disjoint-paths logic FO+DP by adding the atomic predicates disjoint-paths_k[(x_1,y_1),…,(x_k,y_k)] that evaluate to true if there are internally vertex-disjoint paths between (the valuations of) x_i and y_i for all 1 ≤ i ≤ k. Disjoint-paths logic can express the disjoint paths problem, the problem of (topological) minor containment, the problem of hitting (topological) minors, and many more. Again we show that the fragments FO+DP_k that use predicates for at most k disjoint paths form a strict hierarchy of expressiveness. Finally, we compare the expressive power of the new logics with that of transitive-closure logics and monadic second-order logic.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.34/LIPIcs.CSL.2022.34.pdf
First-order logic
graph theory
connectivity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
35:1
35:17
10.4230/LIPIcs.CSL.2022.35
article
Planar Realizability via Left and Right Applications
Tomita, Haruka
1
Research Institute for Mathematical Sciences, Kyoto University, Japan
We introduce a class of applicative structures called bi-BDI-algebras. Bi-BDI-algebras are generalizations of partial combinatory algebras and BCI-algebras, and feature two sorts of applications (left and right applications). Applying the categorical realizability construction to bi-BDI-algebras, we obtain monoidal bi-closed categories of assemblies (as well as of modest sets). We further investigate two kinds of comonadic applicative morphisms on bi-BDI-algebras as non-symmetric analogues of linear combinatory algebras, which induce models of exponential and exchange modalities on non-symmetric linear logics.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.35/LIPIcs.CSL.2022.35.pdf
Realizability
combinatory algebra
monoidal bi-closed category
exponential modality
exchange modality
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
36:1
36:18
10.4230/LIPIcs.CSL.2022.36
article
Number of Variables for Graph Differentiation and the Resolution of GI Formulas
Torán, Jacobo
1
https://orcid.org/0000-0003-2168-4969
Wörz, Florian
1
https://orcid.org/0000-0003-2463-8167
Universität Ulm, Germany
We show that the number of variables and the quantifier depth needed to distinguish a pair of graphs by first-order logic sentences exactly match the complexity measures of clause width and positive depth needed to refute the corresponding graph isomorphism formula in propositional narrow resolution.
Using this connection, we obtain upper and lower bounds for refuting graph isomorphism formulas in (normal) resolution. In particular, we show that if k is the number of variables needed to distinguish two graphs with n vertices each, then there is an n^O(k) resolution refutation size upper bound for the corresponding isomorphism formula, as well as lower bounds of 2^(k-1) and k for the tree-like resolution size and resolution clause space for this formula. We also show a (normal) resolution size lower bound of exp(Ω(k²/n)) for the case of colored graphs with constant color class sizes.
Applying these results, we prove the first exponential lower bound for graph isomorphism formulas in the proof system SRC-1, a system that extends resolution with a global symmetry rule, thereby answering an open question posed by Schweitzer and Seebach.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.36/LIPIcs.CSL.2022.36.pdf
Proof Complexity
Resolution
Narrow Width
Graph Isomorphism
k-variable fragment first-order logic 𝔏_k
Immerman’s Pebble Game
Symmetry Rule
SRC-1
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2022-01-27
216
37:1
37:17
10.4230/LIPIcs.CSL.2022.37
article
Anti-Unification of Unordered Goals
Yernaux, Gonzague
1
2
https://orcid.org/0000-0001-6430-8168
Vanhoof, Wim
1
2
https://orcid.org/0000-0003-3769-6294
Faculty of Computer Science, University of Namur, Belgium
Namur Digital Institute, Belgium
Anti-unification in logic programming refers to the process of capturing common syntactic structure among given goals, computing a single new goal that is more general called a generalization of the given goals. Finding an arbitrary common generalization for two goals is trivial, but looking for those common generalizations that are either as large as possible (called largest common generalizations) or as specific as possible (called most specific generalizations) is a non-trivial optimization problem, in particular when goals are considered to be unordered sets of atoms. In this work we provide an in-depth study of the problem by defining two different generalization relations. We formulate a characterization of what constitutes a most specific generalization in both settings. While these generalizations can be computed in polynomial time, we show that when the number of variables in the generalization needs to be minimized, the problem becomes NP-hard. We subsequently revisit an abstraction of the largest common generalization when anti-unification is based on injective variable renamings, and prove that it can be computed in polynomially bounded time.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol216-csl2022/LIPIcs.CSL.2022.37/LIPIcs.CSL.2022.37.pdf
Anti-unification
Logic programming
NP-completeness
Time complexity
Algorithms
Inductive logic programming