Volume
LIPIcs, Volume 216
30th EACSL Annual Conference on Computer Science Logic (CSL 2022)
-
Part of:
Series:
Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL)
Publication Details
- published at: 2022-01-27
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-95977-218-1
- DBLP: db/conf/csl/csl2022
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 216, CSL 2022, Complete Volume
Abstract
LIPIcs, Volume 216, CSL 2022, Complete Volume
Cite as
30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 1-684, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@Proceedings{manea_et_al:LIPIcs.CSL.2022,
title = {{LIPIcs, Volume 216, CSL 2022, Complete Volume}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {1--684},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022},
URN = {urn:nbn:de:0030-drops-157199},
doi = {10.4230/LIPIcs.CSL.2022},
annote = {Keywords: LIPIcs, Volume 216, CSL 2022, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{manea_et_al:LIPIcs.CSL.2022.0,
author = {Manea, Florin and Simpson, Alex},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {0:i--0:xx},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.0},
URN = {urn:nbn:de:0030-drops-157202},
doi = {10.4230/LIPIcs.CSL.2022.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
Between Deterministic and Nondeterministic Quantitative Automata (Invited Talk)
Abstract
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.
Cite as
Udi Boker. Between Deterministic and Nondeterministic Quantitative Automata (Invited Talk). In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 1:1-1:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{boker:LIPIcs.CSL.2022.1,
author = {Boker, Udi},
title = {{Between Deterministic and Nondeterministic Quantitative Automata}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {1:1--1:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.1},
URN = {urn:nbn:de:0030-drops-157218},
doi = {10.4230/LIPIcs.CSL.2022.1},
annote = {Keywords: Quantitative Automata, Measure of Nondeterminism, Determinism}
}
Document
Invited Talk
How to Develop an Intuition for Risk... and Other Invisible Phenomena (Invited Talk)
Abstract
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.
Cite as
Natasha Fernandes, Annabelle McIver, and Carroll Morgan. How to Develop an Intuition for Risk... and Other Invisible Phenomena (Invited Talk). In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{fernandes_et_al:LIPIcs.CSL.2022.2,
author = {Fernandes, Natasha and McIver, Annabelle and Morgan, Carroll},
title = {{How to Develop an Intuition for Risk... and Other Invisible Phenomena}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {2:1--2:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.2},
URN = {urn:nbn:de:0030-drops-157227},
doi = {10.4230/LIPIcs.CSL.2022.2},
annote = {Keywords: Geometry, Quantitative Information Flow, Proof, Explainability, Privacy}
}
Document
Simulation by Rounds of Letter-To-Letter Transducers
Abstract
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.
Cite as
Antonio Abu Nassar and Shaull Almagor. Simulation by Rounds of Letter-To-Letter Transducers. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 3:1-3:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{abunassar_et_al:LIPIcs.CSL.2022.3,
author = {Abu Nassar, Antonio and Almagor, Shaull},
title = {{Simulation by Rounds of Letter-To-Letter Transducers}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {3:1--3:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.3},
URN = {urn:nbn:de:0030-drops-157231},
doi = {10.4230/LIPIcs.CSL.2022.3},
annote = {Keywords: Transducers, Permutations, Parikh, Simulation, Equivalence}
}
Document
Useful Open Call-By-Need
Abstract
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.
Cite as
Beniamino Accattoli and Maico Leberle. Useful Open Call-By-Need. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{accattoli_et_al:LIPIcs.CSL.2022.4,
author = {Accattoli, Beniamino and Leberle, Maico},
title = {{Useful Open Call-By-Need}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {4:1--4:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.4},
URN = {urn:nbn:de:0030-drops-157242},
doi = {10.4230/LIPIcs.CSL.2022.4},
annote = {Keywords: lambda calculus, call-by-need, operational semantics, sharing, cost models}
}
Document
Gardening with the Pythia A Model of Continuity in a Dependent Setting
Abstract
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.
Cite as
Martin Baillon, Assia Mahboubi, and Pierre-Marie Pédrot. Gardening with the Pythia A Model of Continuity in a Dependent Setting. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 5:1-5:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{baillon_et_al:LIPIcs.CSL.2022.5,
author = {Baillon, Martin and Mahboubi, Assia and P\'{e}drot, Pierre-Marie},
title = {{Gardening with the Pythia A Model of Continuity in a Dependent Setting}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {5:1--5:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.5},
URN = {urn:nbn:de:0030-drops-157256},
doi = {10.4230/LIPIcs.CSL.2022.5},
annote = {Keywords: Type theory, continuity, syntactic model}
}
Document
Weighted Automata and Expressions over Pre-Rational Monoids
Abstract
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.
Cite as
Nicolas Baudru, Louis-Marie Dando, Nathan Lhote, Benjamin Monmege, Pierre-Alain Reynier, and Jean-Marc Talbot. Weighted Automata and Expressions over Pre-Rational Monoids. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{baudru_et_al:LIPIcs.CSL.2022.6,
author = {Baudru, Nicolas and Dando, Louis-Marie and Lhote, Nathan and Monmege, Benjamin and Reynier, Pierre-Alain and Talbot, Jean-Marc},
title = {{Weighted Automata and Expressions over Pre-Rational Monoids}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {6:1--6:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.6},
URN = {urn:nbn:de:0030-drops-157266},
doi = {10.4230/LIPIcs.CSL.2022.6},
annote = {Keywords: Weighted Automata and Expressions, Inverse Monoids, Two-Way Automata}
}
Document
Optimal Strategies in Concurrent Reachability Games
Abstract
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.
Cite as
Benjamin Bordais, Patricia Bouyer, and Stéphane Le Roux. Optimal Strategies in Concurrent Reachability Games. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{bordais_et_al:LIPIcs.CSL.2022.7,
author = {Bordais, Benjamin and Bouyer, Patricia and Le Roux, St\'{e}phane},
title = {{Optimal Strategies in Concurrent Reachability Games}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {7:1--7:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.7},
URN = {urn:nbn:de:0030-drops-157278},
doi = {10.4230/LIPIcs.CSL.2022.7},
annote = {Keywords: Concurrent reachability games, Game forms, Optimal strategies}
}
Document
Finite-Memory Strategies in Two-Player Infinite Games
Abstract
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.
Cite as
Patricia Bouyer, Stéphane Le Roux, and Nathan Thomasset. Finite-Memory Strategies in Two-Player Infinite Games. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{bouyer_et_al:LIPIcs.CSL.2022.8,
author = {Bouyer, Patricia and Le Roux, St\'{e}phane and Thomasset, Nathan},
title = {{Finite-Memory Strategies in Two-Player Infinite Games}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {8:1--8:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.8},
URN = {urn:nbn:de:0030-drops-157285},
doi = {10.4230/LIPIcs.CSL.2022.8},
annote = {Keywords: Two-player win/lose games, Infinite trees, Finite-memory winning strategies, Well partial orders, Hausdorff difference hierarchy}
}
Document
Constructing the Space of Valuations of a Quasi-Polish Space as a Space of Ideals
Abstract
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.
Cite as
Matthew de Brecht. Constructing the Space of Valuations of a Quasi-Polish Space as a Space of Ideals. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 9:1-9:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{debrecht:LIPIcs.CSL.2022.9,
author = {de Brecht, Matthew},
title = {{Constructing the Space of Valuations of a Quasi-Polish Space as a Space of Ideals}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {9:1--9:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.9},
URN = {urn:nbn:de:0030-drops-157293},
doi = {10.4230/LIPIcs.CSL.2022.9},
annote = {Keywords: Quasi-Polish spaces, space of valuations, domain theory, measure theory}
}
Document
On the Complexity of SPEs in Parity Games
Abstract
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.
Cite as
Léonard Brice, Jean-François Raskin, and Marie van den Bogaard. On the Complexity of SPEs in Parity Games. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{brice_et_al:LIPIcs.CSL.2022.10,
author = {Brice, L\'{e}onard and Raskin, Jean-Fran\c{c}ois and van den Bogaard, Marie},
title = {{On the Complexity of SPEs in Parity Games}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {10:1--10:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.10},
URN = {urn:nbn:de:0030-drops-157306},
doi = {10.4230/LIPIcs.CSL.2022.10},
annote = {Keywords: Games on graphs, subgame-perfect equilibria, parity objectives}
}
Document
Synthetic Integral Cohomology in Cubical Agda
Abstract
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.
Cite as
Guillaume Brunerie, Axel Ljungström, and Anders Mörtberg. Synthetic Integral Cohomology in Cubical Agda. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{brunerie_et_al:LIPIcs.CSL.2022.11,
author = {Brunerie, Guillaume and Ljungstr\"{o}m, Axel and M\"{o}rtberg, Anders},
title = {{Synthetic Integral Cohomology in Cubical Agda}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {11:1--11:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.11},
URN = {urn:nbn:de:0030-drops-157310},
doi = {10.4230/LIPIcs.CSL.2022.11},
annote = {Keywords: Synthetic Homotopy Theory, Cohomology Theory, Cubical Agda}
}
Document
On the Minimisation of Transition-Based Rabin Automata and the Chromatic Memory Requirements of Muller Conditions
Abstract
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.
Cite as
Antonio Casares. On the Minimisation of Transition-Based Rabin Automata and the Chromatic Memory Requirements of Muller Conditions. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{casares:LIPIcs.CSL.2022.12,
author = {Casares, Antonio},
title = {{On the Minimisation of Transition-Based Rabin Automata and the Chromatic Memory Requirements of Muller Conditions}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {12:1--12:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.12},
URN = {urn:nbn:de:0030-drops-157322},
doi = {10.4230/LIPIcs.CSL.2022.12},
annote = {Keywords: Automata on Infinite Words, Games on Graphs, Arena-Independent Memory, Complexity}
}
Document
Fuzzy Algebraic Theories
Abstract
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.
Cite as
Davide Castelnovo and Marino Miculan. Fuzzy Algebraic Theories. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{castelnovo_et_al:LIPIcs.CSL.2022.13,
author = {Castelnovo, Davide and Miculan, Marino},
title = {{Fuzzy Algebraic Theories}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {13:1--13:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.13},
URN = {urn:nbn:de:0030-drops-157332},
doi = {10.4230/LIPIcs.CSL.2022.13},
annote = {Keywords: categorical logic, fuzzy sets, algebraic reasoning, equational axiomatisations, monads, Eilenberg-Moore algebras}
}
Document
Realising Intensional S4 and GL Modalities
Abstract
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.
Cite as
Liang-Ting Chen and Hsiang-Shang Ko. Realising Intensional S4 and GL Modalities. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{chen_et_al:LIPIcs.CSL.2022.14,
author = {Chen, Liang-Ting and Ko, Hsiang-Shang},
title = {{Realising Intensional S4 and GL Modalities}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {14:1--14:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.14},
URN = {urn:nbn:de:0030-drops-157341},
doi = {10.4230/LIPIcs.CSL.2022.14},
annote = {Keywords: provability, guarded recursion, realisability, modal types, metaprogramming}
}
Document
Localisable Monads
Abstract
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.
Cite as
Carmen Constantin, Nuiok Dicaire, and Chris Heunen. Localisable Monads. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{constantin_et_al:LIPIcs.CSL.2022.15,
author = {Constantin, Carmen and Dicaire, Nuiok and Heunen, Chris},
title = {{Localisable Monads}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {15:1--15:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.15},
URN = {urn:nbn:de:0030-drops-157353},
doi = {10.4230/LIPIcs.CSL.2022.15},
annote = {Keywords: Monad, Monoidal category, Presheaf, Central idempotent, Graded monad, Indexed monad, Formal monad, Strong monad, Commutative monad}
}
Document
An Internal Language for Categories Enriched over Generalised Metric Spaces
Abstract
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.
Cite as
Fredrik Dahlqvist and Renato Neves. An Internal Language for Categories Enriched over Generalised Metric Spaces. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{dahlqvist_et_al:LIPIcs.CSL.2022.16,
author = {Dahlqvist, Fredrik and Neves, Renato},
title = {{An Internal Language for Categories Enriched over Generalised Metric Spaces}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {16:1--16:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.16},
URN = {urn:nbn:de:0030-drops-157362},
doi = {10.4230/LIPIcs.CSL.2022.16},
annote = {Keywords: \lambda-calculus, enriched category theory, quantale, equational theory}
}
Document
MSO Undecidability for Hereditary Classes of Unbounded Clique Width
Abstract
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.
Cite as
Anuj Dawar and Abhisekh Sankaran. MSO Undecidability for Hereditary Classes of Unbounded Clique Width. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{dawar_et_al:LIPIcs.CSL.2022.17,
author = {Dawar, Anuj and Sankaran, Abhisekh},
title = {{MSO Undecidability for Hereditary Classes of Unbounded Clique Width}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {17:1--17:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.17},
URN = {urn:nbn:de:0030-drops-157373},
doi = {10.4230/LIPIcs.CSL.2022.17},
annote = {Keywords: clique width, Seese’s conjecture, antichain, MSO interpretation, grid}
}
Document
Constructive Many-One Reduction from the Halting Problem to Semi-Unification
Abstract
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.
Cite as
Andrej Dudenhefner. Constructive Many-One Reduction from the Halting Problem to Semi-Unification. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 18:1-18:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{dudenhefner:LIPIcs.CSL.2022.18,
author = {Dudenhefner, Andrej},
title = {{Constructive Many-One Reduction from the Halting Problem to Semi-Unification}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {18:1--18:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.18},
URN = {urn:nbn:de:0030-drops-157380},
doi = {10.4230/LIPIcs.CSL.2022.18},
annote = {Keywords: constructive mathematics, undecidability, mechanization, semi-unification}
}
Document
Dynamic Cantor Derivative Logic
Abstract
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.
Cite as
David Fernández-Duque and Yoàv Montacute. Dynamic Cantor Derivative Logic. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{fernandezduque_et_al:LIPIcs.CSL.2022.19,
author = {Fern\'{a}ndez-Duque, David and Montacute, Yo\`{a}v},
title = {{Dynamic Cantor Derivative Logic}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {19:1--19:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.19},
URN = {urn:nbn:de:0030-drops-157397},
doi = {10.4230/LIPIcs.CSL.2022.19},
annote = {Keywords: dynamic topological logic, Cantor derivative, temporal logic, modal logic}
}
Document
Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory
Abstract
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.
Cite as
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{finkbeiner_et_al:LIPIcs.CSL.2022.20,
author = {Finkbeiner, Bernd and Gieseking, Manuel and Hecking-Harbusch, Jesko and Olderog, Ernst-R\"{u}diger},
title = {{Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {20:1--20:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.20},
URN = {urn:nbn:de:0030-drops-157400},
doi = {10.4230/LIPIcs.CSL.2022.20},
annote = {Keywords: Synthesis, distributed systems, reactive systems, Petri games, decidability}
}
Document
Inferring Symbolic Automata
Abstract
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.
Cite as
Dana Fisman, Hadar Frenkel, and Sandra Zilles. Inferring Symbolic Automata. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 21:1-21:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{fisman_et_al:LIPIcs.CSL.2022.21,
author = {Fisman, Dana and Frenkel, Hadar and Zilles, Sandra},
title = {{Inferring Symbolic Automata}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {21:1--21:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.21},
URN = {urn:nbn:de:0030-drops-157412},
doi = {10.4230/LIPIcs.CSL.2022.21},
annote = {Keywords: Symbolic Finite State Automata, Query Learning, Characteristic Sets}
}
Document
Differential Games, Locality, and Model Checking for FO Logic of Graphs
Abstract
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.
Cite as
Jakub Gajarský, Maximilian Gorsky, and Stephan Kreutzer. Differential Games, Locality, and Model Checking for FO Logic of Graphs. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{gajarsky_et_al:LIPIcs.CSL.2022.22,
author = {Gajarsk\'{y}, Jakub and Gorsky, Maximilian and Kreutzer, Stephan},
title = {{Differential Games, Locality, and Model Checking for FO Logic of Graphs}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {22:1--22:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.22},
URN = {urn:nbn:de:0030-drops-157426},
doi = {10.4230/LIPIcs.CSL.2022.22},
annote = {Keywords: FO model checking, locality, Gaifman’s theorem, EF games}
}
Document
Cyclic Proofs for Transfinite Expressions
Abstract
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.
Cite as
Emile Hazard and Denis Kuperberg. Cyclic Proofs for Transfinite Expressions. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{hazard_et_al:LIPIcs.CSL.2022.23,
author = {Hazard, Emile and Kuperberg, Denis},
title = {{Cyclic Proofs for Transfinite Expressions}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {23:1--23:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.23},
URN = {urn:nbn:de:0030-drops-157433},
doi = {10.4230/LIPIcs.CSL.2022.23},
annote = {Keywords: transfinite expressions, transfinite automata, cyclic proofs}
}
Document
Decidability for Sturmian Words
Abstract
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.
Cite as
Philipp Hieronymi, Dun Ma, Reed Oei, Luke Schaeffer, Christian Schulz, and Jeffrey Shallit. Decidability for Sturmian Words. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 24:1-24:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{hieronymi_et_al:LIPIcs.CSL.2022.24,
author = {Hieronymi, Philipp and Ma, Dun and Oei, Reed and Schaeffer, Luke and Schulz, Christian and Shallit, Jeffrey},
title = {{Decidability for Sturmian Words}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {24:1--24:23},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.24},
URN = {urn:nbn:de:0030-drops-157440},
doi = {10.4230/LIPIcs.CSL.2022.24},
annote = {Keywords: Decidability, Sturmian words, Ostrowski numeration systems, Automated theorem proving}
}
Document
Games, Mobile Processes, and Functions
Abstract
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.
Cite as
Guilhem Jaber and Davide Sangiorgi. Games, Mobile Processes, and Functions. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{jaber_et_al:LIPIcs.CSL.2022.25,
author = {Jaber, Guilhem and Sangiorgi, Davide},
title = {{Games, Mobile Processes, and Functions}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {25:1--25:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.25},
URN = {urn:nbn:de:0030-drops-157450},
doi = {10.4230/LIPIcs.CSL.2022.25},
annote = {Keywords: \lambda-calculus, \pi-calculus, game semantics}
}
Document
Parallelism in Soft Linear Logic
Abstract
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.
Cite as
Paulin Jacobé de Naurois. Parallelism in Soft Linear Logic. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{jacobedenaurois:LIPIcs.CSL.2022.26,
author = {Jacob\'{e} de Naurois, Paulin},
title = {{Parallelism in Soft Linear Logic}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {26:1--26:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.26},
URN = {urn:nbn:de:0030-drops-157468},
doi = {10.4230/LIPIcs.CSL.2022.26},
annote = {Keywords: Implicit Complexity, Typing, Linear Logic, Functional Programming}
}
Document
Encoding Tight Typing in a Unified Framework
Abstract
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.
Cite as
Delia Kesner and Andrés Viso. Encoding Tight Typing in a Unified Framework. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 27:1-27:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{kesner_et_al:LIPIcs.CSL.2022.27,
author = {Kesner, Delia and Viso, Andr\'{e}s},
title = {{Encoding Tight Typing in a Unified Framework}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {27:1--27:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.27},
URN = {urn:nbn:de:0030-drops-157479},
doi = {10.4230/LIPIcs.CSL.2022.27},
annote = {Keywords: Call-by-Push-Value, Call-by-Name, Call-by-Value, Intersection Types}
}
Document
Generalized Universe Hierarchies and First-Class Universe Levels
Abstract
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.
Cite as
András Kovács. Generalized Universe Hierarchies and First-Class Universe Levels. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{kovacs:LIPIcs.CSL.2022.28,
author = {Kov\'{a}cs, Andr\'{a}s},
title = {{Generalized Universe Hierarchies and First-Class Universe Levels}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {28:1--28:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.28},
URN = {urn:nbn:de:0030-drops-157485},
doi = {10.4230/LIPIcs.CSL.2022.28},
annote = {Keywords: type theory, universes}
}
Document
Succinct Graph Representations of μ-Calculus Formulas
Abstract
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.
Cite as
Clemens Kupke, Johannes Marti, and Yde Venema. Succinct Graph Representations of μ-Calculus Formulas. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{kupke_et_al:LIPIcs.CSL.2022.29,
author = {Kupke, Clemens and Marti, Johannes and Venema, Yde},
title = {{Succinct Graph Representations of \mu-Calculus Formulas}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {29:1--29:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.29},
URN = {urn:nbn:de:0030-drops-157491},
doi = {10.4230/LIPIcs.CSL.2022.29},
annote = {Keywords: modal mu-calculus, model checking, alternating tree automata, hierachical equation systems}
}
Document
Spatial Existential Positive Logics for Hyperedge Replacement Grammars
Abstract
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.
Cite as
Yoshiki Nakamura. Spatial Existential Positive Logics for Hyperedge Replacement Grammars. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{nakamura:LIPIcs.CSL.2022.30,
author = {Nakamura, Yoshiki},
title = {{Spatial Existential Positive Logics for Hyperedge Replacement Grammars}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {30:1--30:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.30},
URN = {urn:nbn:de:0030-drops-157504},
doi = {10.4230/LIPIcs.CSL.2022.30},
annote = {Keywords: Existential positive logic, spatial logic, Kleene theorem}
}
Document
Structural Properties of the First-Order Transduction Quasiorder
Abstract
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.
Cite as
Jaroslav Nešetřil, Patrice Ossona de Mendez, and Sebastian Siebertz. Structural Properties of the First-Order Transduction Quasiorder. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{nesetril_et_al:LIPIcs.CSL.2022.31,
author = {Ne\v{s}et\v{r}il, Jaroslav and Ossona de Mendez, Patrice and Siebertz, Sebastian},
title = {{Structural Properties of the First-Order Transduction Quasiorder}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {31:1--31:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.31},
URN = {urn:nbn:de:0030-drops-157514},
doi = {10.4230/LIPIcs.CSL.2022.31},
annote = {Keywords: Finite model theory, first-order transductions, structural graph theory}
}
Document
BV and Pomset Logic Are Not the Same
Abstract
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.
Cite as
Lê Thành Dũng (Tito) Nguyễn and Lutz Straßburger. BV and Pomset Logic Are Not the Same. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 32:1-32:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{nguyen_et_al:LIPIcs.CSL.2022.32,
author = {Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng (Tito) and Stra{\ss}burger, Lutz},
title = {{BV and Pomset Logic Are Not the Same}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {32:1--32:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.32},
URN = {urn:nbn:de:0030-drops-157521},
doi = {10.4230/LIPIcs.CSL.2022.32},
annote = {Keywords: proof nets, deep inference, pomset logic, system BV, cographs, dicographs, series-parallel orders}
}
Document
Revisiting Parameter Synthesis for One-Counter Automata
Abstract
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.
Cite as
Guillermo A. Pérez and Ritam Raha. Revisiting Parameter Synthesis for One-Counter Automata. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 33:1-33:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{perez_et_al:LIPIcs.CSL.2022.33,
author = {P\'{e}rez, Guillermo A. and Raha, Ritam},
title = {{Revisiting Parameter Synthesis for One-Counter Automata}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {33:1--33:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.33},
URN = {urn:nbn:de:0030-drops-157534},
doi = {10.4230/LIPIcs.CSL.2022.33},
annote = {Keywords: Parametric one-counter automata, Reachability, Software Verification}
}
Document
First-Order Logic with Connectivity Operators
Abstract
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.
Cite as
Nicole Schirrmacher, Sebastian Siebertz, and Alexandre Vigny. First-Order Logic with Connectivity Operators. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{schirrmacher_et_al:LIPIcs.CSL.2022.34,
author = {Schirrmacher, Nicole and Siebertz, Sebastian and Vigny, Alexandre},
title = {{First-Order Logic with Connectivity Operators}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {34:1--34:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.34},
URN = {urn:nbn:de:0030-drops-157548},
doi = {10.4230/LIPIcs.CSL.2022.34},
annote = {Keywords: First-order logic, graph theory, connectivity}
}
Document
Planar Realizability via Left and Right Applications
Abstract
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.
Cite as
Haruka Tomita. Planar Realizability via Left and Right Applications. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 35:1-35:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{tomita:LIPIcs.CSL.2022.35,
author = {Tomita, Haruka},
title = {{Planar Realizability via Left and Right Applications}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {35:1--35:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.35},
URN = {urn:nbn:de:0030-drops-157558},
doi = {10.4230/LIPIcs.CSL.2022.35},
annote = {Keywords: Realizability, combinatory algebra, monoidal bi-closed category, exponential modality, exchange modality}
}
Document
Number of Variables for Graph Differentiation and the Resolution of GI Formulas
Abstract
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.
Cite as
Jacobo Torán and Florian Wörz. Number of Variables for Graph Differentiation and the Resolution of GI Formulas. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 36:1-36:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{toran_et_al:LIPIcs.CSL.2022.36,
author = {Tor\'{a}n, Jacobo and W\"{o}rz, Florian},
title = {{Number of Variables for Graph Differentiation and the Resolution of GI Formulas}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {36:1--36:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.36},
URN = {urn:nbn:de:0030-drops-157564},
doi = {10.4230/LIPIcs.CSL.2022.36},
annote = {Keywords: Proof Complexity, Resolution, Narrow Width, Graph Isomorphism, k-variable fragment first-order logic 𝔏\underlinek, Immerman’s Pebble Game, Symmetry Rule, SRC-1}
}
Document
Anti-Unification of Unordered Goals
Abstract
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.
Cite as
Gonzague Yernaux and Wim Vanhoof. Anti-Unification of Unordered Goals. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 37:1-37:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
Copy BibTex To Clipboard
@InProceedings{yernaux_et_al:LIPIcs.CSL.2022.37,
author = {Yernaux, Gonzague and Vanhoof, Wim},
title = {{Anti-Unification of Unordered Goals}},
booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
pages = {37:1--37:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-218-1},
ISSN = {1868-8969},
year = {2022},
volume = {216},
editor = {Manea, Florin and Simpson, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.37},
URN = {urn:nbn:de:0030-drops-157574},
doi = {10.4230/LIPIcs.CSL.2022.37},
annote = {Keywords: Anti-unification, Logic programming, NP-completeness, Time complexity, Algorithms, Inductive logic programming}
}