15 Search Results for "Levy, Paul Blain"

Document
DOI: 10.4230/LIPIcs.CSL.2026.16
On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions

Authors: Nicolas Peltier

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Separation Logic (SL) is a well-established framework for reasoning about programs that manipulate dynamic memory. To express and verify properties of custom recursive data structures, SL is extended with spatial predicates defined by user-specified inductive rules. Many verification problems reduce to deciding entailments between formulas involving these predicates. While the general entailment problem is undecidable, a broad class of inductive rules - known as PCE (Progressing, Connected, and Established) - has been identified for which entailment is decidable. In this work, we extend the study of the entailment problem to Dynamic Separation Logic (DSL), an extension of SL that includes dynamic modalities for reasoning about actions on the heap and store. We show that entailment in DSL remains decidable for PCE rules by proving that dynamic modalities can be automatically eliminated.
Cite as

Nicolas Peltier. On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 16:1-16:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{peltier:LIPIcs.CSL.2026.16,
  author =	{Peltier, Nicolas},
  title =	{{On the Entailment Problem in Dynamic Separation Logic with Inductive Definitions}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{16:1--16:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.16},
  URN =		{urn:nbn:de:0030-drops-254402},
  doi =		{10.4230/LIPIcs.CSL.2026.16},
  annote =	{Keywords: Separation logic, Dynamic logic, Entailment problem}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.28
Resourceful Traces for Commuting Processes

Authors: Matthew Earnshaw, Chad Nester, and Mario Román

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We show that, when the actions of a Mazurkiewicz trace are considered not merely as atomic but as transformations from a specified type of inputs to a specified type of outputs, we obtain a novel notion of presentation for effectful categories (also known as generalized Freyd categories), a well-known algebraic structure in the semantics of side-effecting computation. Like the usual representation of traces as graphs, our notion of presentation gives rise to a graphical representation of morphisms in effectful categories. We use our presentations to give a construction of the commuting tensor product of free effectful categories, capturing the combination of systems in which the actions of each must commute with one another, while still permitting exchange of resources.
Cite as

Matthew Earnshaw, Chad Nester, and Mario Román. Resourceful Traces for Commuting Processes. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{earnshaw_et_al:LIPIcs.CSL.2026.28,
  author =	{Earnshaw, Matthew and Nester, Chad and Rom\'{a}n, Mario},
  title =	{{Resourceful Traces for Commuting Processes}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{28:1--28:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.28},
  URN =		{urn:nbn:de:0030-drops-254522},
  doi =		{10.4230/LIPIcs.CSL.2026.28},
  annote =	{Keywords: Mazurkiewicz traces, premonoidal categories, monoidal categories, effectful categories}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CSL.2026.3
Rational Lawvere Logic (Invited Paper)

Authors: Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon Plotkin

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We study Rational Lawvere logic (RL). This logic is defined over the extended positive reals with an algebraic structure combining the Lawvere quantale (with the reversed order on the extended reals and a sum as tensor) and a multiplicative quantale (with the usual order on the extended reals and a multiplication as tensor); together they provide a semiring structure. The logic is designed for complex quantitative reasoning, including sequents expressing inequalities between rational functions over the extended positive reals. We give a deduction system and demonstrate its expressiveness by deriving a classical result from probability theory relating the Kantorovich and total variation distances. Our deductive system is complete for finitely axiomatizable theories. The proof of completeness relies on the Krivine-Stengle Positivstellensatz. We additionally provide complexity results for both RL and its affine fragment AL. We consider two decision problems: the satisfiability of a set of sequents and whether a sequent follows from a finite set of sequent. We show that both problems lie in PSPACE for RL, and we give sharper complexity bounds for AL: the first problem is NP-complete, while the second is co-NP-complete.
Cite as

Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Rational Lawvere Logic (Invited Paper). In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bacci_et_al:LIPIcs.CSL.2026.3,
  author =	{Bacci, Giorgio and Mardare, Radu and Panangaden, Prakash and Plotkin, Gordon},
  title =	{{Rational Lawvere Logic}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{3:1--3:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.3},
  URN =		{urn:nbn:de:0030-drops-254277},
  doi =		{10.4230/LIPIcs.CSL.2026.3},
  annote =	{Keywords: Quantitative reasoning, complete deductive system, Lawvere’s quantale}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.7
A Verified Cost Model for Call-By-Push-Value

Authors: Zhuo Zoey Chen, Johannes Åman Pohjola, and Christine Rizkallah

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
The call-by-push-value λ-calculus allows for syntactically specifying the order of evaluation as part of the term language. Hence, it serves as a unifying language for embedding various evaluation strategies including call-by-value and call-by-name. Given the impact of call-by-push-value, it is remarkable that its adequacy as a model for computational complexity theory has not yet been studied. In this paper, we show that the call-by-push-value λ-calculus is reasonable for both time and space complexity. A reasonable cost model can encode other reasonable cost models with polynomial overhead in time and constant factor overhead in space. We achieve this by encoding call-by-push-value λ-calculus into Turing machines, following a simulation strategy by Forster et al.; for the converse direction, we prove that Levy’s encoding of the call-by-value λ-calculus has reasonable complexity bounds. The main results have been formalised in the HOL4 theorem prover.
Cite as

Zhuo Zoey Chen, Johannes Åman Pohjola, and Christine Rizkallah. A Verified Cost Model for Call-By-Push-Value. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.ITP.2025.7,
  author =	{Chen, Zhuo Zoey and \r{A}man Pohjola, Johannes and Rizkallah, Christine},
  title =	{{A Verified Cost Model for Call-By-Push-Value}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.7},
  URN =		{urn:nbn:de:0030-drops-246067},
  doi =		{10.4230/LIPIcs.ITP.2025.7},
  annote =	{Keywords: lambda calculus, formalizations of computational models, computability theory, HOL, call-by-push-value reduction, time and space complexity, abstract machines}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.15
On the Metric Nature of (Differential) Logical Relations

Authors: Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Differential logical relations are a method to measure distances between higher-order programs. They differ from standard methods based on program metrics in that differences between functional programs are themselves functions, relating errors in input with errors in output, this way providing a more fine grained, contextual, information. The aim of this paper is to clarify the metric nature of differential logical relations. While previous work has shown that these do not give rise, in general, to (quasi-)metric spaces nor to partial metric spaces, we show that the distance functions arising from such relations, that we call quasi-quasi-metrics, can be related to both quasi-metrics and partial metrics, the latter being also captured by suitable relational definitions. Moreover, we exploit such connections to deduce some new compositional reasoning principles for program differences.
Cite as

Ugo Dal Lago, Naohiko Hoshino, and Paolo Pistone. On the Metric Nature of (Differential) Logical Relations. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 15:1-15:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dallago_et_al:LIPIcs.FSCD.2025.15,
  author =	{Dal Lago, Ugo and Hoshino, Naohiko and Pistone, Paolo},
  title =	{{On the Metric Nature of (Differential) Logical Relations}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{15:1--15:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.15},
  URN =		{urn:nbn:de:0030-drops-236300},
  doi =		{10.4230/LIPIcs.FSCD.2025.15},
  annote =	{Keywords: Differential Logical Relations, Quantales, Quasi-Metrics, Partial Metrics}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.29
Linear Logic Using Negative Connectives

Authors: Dale Miller

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
In linear logic, the invertibility of a connective’s right-introduction rule is equivalent to the non-invertibility of its left-introduction rule. This duality motivates the concept of polarity: a connective is termed negative if its right-introduction rule is invertible, and positive otherwise. A two-sided sequent calculus for first-order linear logic featuring only negative connectives exhibits a compelling proof theory. Proof search in such a system unfolds through alternating phases of invertible (right-introduction) rules and non-invertible (left-introduction) rules, mirroring the processes of goal-reduction and backchaining, respectively. These phases are formalized here using the framework of multifocused proofs. We analyze linear logic by dissecting it into three sublogics: L₀ (first-order intuitionistic logic with conjunction, implication, and universal quantification); L₁ (an extension of L₀ incorporating linear implication which preserves its intuitionistic nature); and L₂ (which includes multiplicative falsity ⊥ and encompasses classical linear logic). It is worth noting that the single-conclusion restriction on sequents, a constraint imposed by Gentzen, is not a prerequisite for defining intuitionistic logic proofs within this framework, as it emerges naturally by restricting the formulas to those of L₀ and L₁. While multifocused proofs of L₂ sequents can accommodate parallel applications of left-introduction rules, proofs of L₀ and L₁ sequents cannot leverage such parallel rule applications. This notion of parallelism within proofs enables a novel approach to handling disjunctions and existential quantifiers in the natural deduction system for intuitionistic logic.
Cite as

Dale Miller. Linear Logic Using Negative Connectives. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 29:1-29:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{miller:LIPIcs.FSCD.2025.29,
  author =	{Miller, Dale},
  title =	{{Linear Logic Using Negative Connectives}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{29:1--29:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.29},
  URN =		{urn:nbn:de:0030-drops-236442},
  doi =		{10.4230/LIPIcs.FSCD.2025.29},
  annote =	{Keywords: Linear logic, multifocused proofs, sequent calculus}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2024.6
Data Types with Symmetries via Action Containers

Authors: Philipp Joram and Niccolò Veltri

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

Abstract
We study two kinds of containers for data types with symmetries in homotopy type theory, and clarify their relationship by introducing the intermediate notion of action containers. Quotient containers are set-valued containers with groups of permissible permutations of positions, interpreted as (possibly non-finitary) analytic functors on the category of sets. Symmetric containers encode symmetries in a groupoid of shapes, and are interpreted accordingly as polynomial functors on the 2-category of groupoids. Action containers are endowed with groups that act on their positions, with morphisms preserving the actions. We show that, as a category, action containers are equivalent to the free coproduct completion of a category of group actions. We derive that they model non-inductive single-variable strictly positive types in the sense of Abbott et al.: The category of action containers is closed under arbitrary (co)products and exponentiation with constants. We equip this category with the structure of a locally groupoidal 2-category, and prove that it locally embeds into the 2-category of symmetric containers. This follows from the embedding of a 2-category of groups into the 2-category of groupoids, extending the delooping construction.
Cite as

Philipp Joram and Niccolò Veltri. Data Types with Symmetries via Action Containers. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{joram_et_al:LIPIcs.TYPES.2024.6,
  author =	{Joram, Philipp and Veltri, Niccol\`{o}},
  title =	{{Data Types with Symmetries via Action Containers}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{6:1--6:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-376-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{336},
  editor =	{M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.6},
  URN =		{urn:nbn:de:0030-drops-233681},
  doi =		{10.4230/LIPIcs.TYPES.2024.6},
  annote =	{Keywords: Containers, Homotopy Type Theory, Agda, 2-categories}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2025.165
Algebraic Language Theory with Effects

Authors: Fabian Lenke, Stefan Milius, Henning Urbat, and Thorsten Wißmann

Published in: LIPIcs, Volume 334, 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)

Abstract
Regular languages - the languages accepted by deterministic finite automata - are known to be precisely the languages recognized by finite monoids. This characterization is the origin of algebraic language theory. In this paper, we generalize the correspondence between automata and monoids to automata with generic computational effects given by a monad, providing the foundations of an effectful algebraic language theory. We show that, under suitable conditions on the monad, a language is computable by an effectful automaton precisely when it is recognizable by (1) an effectful monoid morphism into an effect-free finite monoid, and (2) a monoid morphism into a monad-monoid bialgebra whose carrier is a finitely generated algebra for the monad, the former mode of recognition being conceptually completely new. Our prime application is a novel algebraic approach to languages computed by probabilistic finite automata. Additionally, we derive new algebraic characterizations for nondeterministic probabilistic finite automata and for weighted finite automata over unrestricted semirings, generalizing previous results on weighted algebraic recognition over commutative rings.
Cite as

Fabian Lenke, Stefan Milius, Henning Urbat, and Thorsten Wißmann. Algebraic Language Theory with Effects. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 165:1-165:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lenke_et_al:LIPIcs.ICALP.2025.165,
  author =	{Lenke, Fabian and Milius, Stefan and Urbat, Henning and Wi{\ss}mann, Thorsten},
  title =	{{Algebraic Language Theory with Effects}},
  booktitle =	{52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025)},
  pages =	{165:1--165:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-372-0},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{334},
  editor =	{Censor-Hillel, Keren and Grandoni, Fabrizio and Ouaknine, Jo\"{e}l and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2025.165},
  URN =		{urn:nbn:de:0030-drops-235423},
  doi =		{10.4230/LIPIcs.ICALP.2025.165},
  annote =	{Keywords: Automaton, Monoid, Monad, Effect, Algebraic language theory}
}
Document
DOI: 10.4230/LIPIcs.STACS.2025.40
Identity-Preserving Lax Extensions and Where to Find Them

Authors: Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
Generic notions of bisimulation for various types of systems (nondeterministic, probabilistic, weighted etc.) rely on identity-preserving (normal) lax extensions of the functor encapsulating the system type, in the paradigm of universal coalgebra. It is known that preservation of weak pullbacks is a sufficient condition for a functor to admit a normal lax extension (the Barr extension, which in fact is then even strict); in the converse direction, nothing is currently known about necessary (weak) pullback preservation conditions for the existence of normal lax extensions. In the present work, we narrow this gap by showing on the one hand that functors admitting a normal lax extension preserve 1/4-iso pullbacks, i.e. pullbacks in which at least one of the projections is an isomorphism. On the other hand, we give sufficient conditions, showing that a functor admits a normal lax extension if it weakly preserves either 1/4-iso pullbacks and 4/4-epi pullbacks (i.e. pullbacks in which all morphisms are epic) or inverse images. We apply these criteria to concrete examples, in particular to functors modelling neighbourhood systems and weighted systems.
Cite as

Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Identity-Preserving Lax Extensions and Where to Find Them. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 40:1-40:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{goncharov_et_al:LIPIcs.STACS.2025.40,
  author =	{Goncharov, Sergey and Hofmann, Dirk and Nora, Pedro and Schr\"{o}der, Lutz and Wild, Paul},
  title =	{{Identity-Preserving Lax Extensions and Where to Find Them}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{40:1--40:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.40},
  URN =		{urn:nbn:de:0030-drops-228665},
  doi =		{10.4230/LIPIcs.STACS.2025.40},
  annote =	{Keywords: (Bi-)simulations, lax extensions, modal logics, coalgebra}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.26
The Complexity of Deciding Characteristic Formulae in Van Glabbeek’s Branching-Time Spectrum

Authors: Luca Aceto, Antonis Achilleos, Aggeliki Chalki, and Anna Ingólfsdóttir

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Characteristic formulae give a complete logical description of the behaviour of processes modulo some chosen notion of behavioural semantics. They allow one to reduce equivalence or preorder checking to model checking, and are exactly the formulae in the modal logics characterizing classic behavioural equivalences and preorders for which model checking can be reduced to equivalence or preorder checking. This paper studies the complexity of determining whether a formula is characteristic for some process in each of the logics providing modal characterizations of the simulation-based semantics in van Glabbeek’s branching-time spectrum. Since characteristic formulae in each of those logics are exactly the satisfiable and prime ones, this article presents complexity results for the satisfiability and primality problems, and investigates the boundary between modal logics for which those problems can be solved in polynomial time and those for which they become computationally hard. Amongst other contributions, this article also studies the complexity of constructing characteristic formulae in the modal logics characterizing simulation-based semantics, both when such formulae are presented in explicit form and via systems of equations.
Cite as

Luca Aceto, Antonis Achilleos, Aggeliki Chalki, and Anna Ingólfsdóttir. The Complexity of Deciding Characteristic Formulae in Van Glabbeek’s Branching-Time Spectrum. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CSL.2025.26,
  author =	{Aceto, Luca and Achilleos, Antonis and Chalki, Aggeliki and Ing\'{o}lfsd\'{o}ttir, Anna},
  title =	{{The Complexity of Deciding Characteristic Formulae in Van Glabbeek’s Branching-Time Spectrum}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{26:1--26:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.26},
  URN =		{urn:nbn:de:0030-drops-227836},
  doi =		{10.4230/LIPIcs.CSL.2025.26},
  annote =	{Keywords: Characteristic formulae, prime formulae, bisimulation, simulation relations, modal logics, complexity theory, satisfiability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.33
Quantitative Graded Semantics and Spectra of Behavioural Metrics

Authors: Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Behavioural metrics provide a quantitative refinement of classical two-valued behavioural equivalences on systems with quantitative data, such as metric or probabilistic transition systems. In analogy to the linear-time/ branching-time spectrum of two-valued behavioural equivalences on transition systems, behavioural metrics vary in granularity, and are often characterized by fragments of suitable modal logics. In the latter respect, the quantitative case is, however, more involved than the two-valued one; in fact, we show that probabilistic metric trace distance cannot be characterized by any compositionally defined modal logic with unary modalities. We go on to provide a unifying treatment of spectra of behavioural metrics in the emerging framework of graded monads, working in coalgebraic generality, that is, parametrically in the system type. In the ensuing development of quantitative graded semantics, we introduce algebraic presentations of graded monads on the category of metric spaces. Moreover, we provide a general criterion for a given real-valued modal logic to characterize a given behavioural distance. As a case study, we apply this criterion to obtain a new characteristic modal logic for trace distance in fuzzy metric transition systems.
Cite as

Jonas Forster, Lutz Schröder, Paul Wild, Harsh Beohar, Sebastian Gurke, Barbara König, and Karla Messing. Quantitative Graded Semantics and Spectra of Behavioural Metrics. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{forster_et_al:LIPIcs.CSL.2025.33,
  author =	{Forster, Jonas and Schr\"{o}der, Lutz and Wild, Paul and Beohar, Harsh and Gurke, Sebastian and K\"{o}nig, Barbara and Messing, Karla},
  title =	{{Quantitative Graded Semantics and Spectra of Behavioural Metrics}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{33:1--33:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.33},
  URN =		{urn:nbn:de:0030-drops-227907},
  doi =		{10.4230/LIPIcs.CSL.2025.33},
  annote =	{Keywords: transition systems, modal logics, coalgebras, behavioural metrics}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.31
Simple Types for Probabilistic Termination

Authors: Willem Heijltjes and Georgina Majury

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We present a new typing discipline to guarantee the probability of termination in probabilistic lambda-calculi. The main contribution is a particular naturality and simplicity: our probabilistic types are as simple types, but generated from probabilities as base types, representing a least probability of termination. Simple types are recovered by restricting probabilities to one. Our vehicle is the Probabilistic Event Lambda-Calculus by Dal Lago, Guerrieri, and Heijltjes, which presents a solution to the issue of confluence in probabilistic lambda-calculi. Our probabilistic type system provides an alternative solution to that using counting quantifiers by Antonelli, Dal Lago, and Pistone, for the same calculus. The problem that both type systems address is to give a lower bound on the probability that terms head-normalize. Following the recent Functional Machine Calculus by Heijltjes, our development takes the (simplified) Krivine machine as primary, and proceeds via an extension of the calculus with sequential composition and identity on the machine. Our type system then gives a natural account of termination probability on the Krivine machine, reflected back onto head-normalization for the original calculus. In this way we are able to avoid the use of counting quantifiers, while improving on the termination bounds given by Antonelli, Dal Lago, and Pistone.
Cite as

Willem Heijltjes and Georgina Majury. Simple Types for Probabilistic Termination. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{heijltjes_et_al:LIPIcs.CSL.2025.31,
  author =	{Heijltjes, Willem and Majury, Georgina},
  title =	{{Simple Types for Probabilistic Termination}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{31:1--31:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.31},
  URN =		{urn:nbn:de:0030-drops-227885},
  doi =		{10.4230/LIPIcs.CSL.2025.31},
  annote =	{Keywords: lambda-calculus, probabilistic termination, simple types}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2019.13
Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot

Authors: Paul Blain Levy and Sergey Goncharov

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

Abstract
We introduce a new notion of "guarded Elgot monad", that is a monad equipped with a form of iteration. It requires every guarded morphism to have a specified fixpoint, and classical equational laws of iteration to be satisfied. This notion includes Elgot monads, but also further examples of partial non-unique iteration, emerging in the semantics of processes under infinite trace equivalence. We recall the construction of the "coinductive resumption monad" from a monad and endofunctor, that is used for modelling programs up to bisimilarity. We characterize this construction via a universal property: if the given monad is guarded Elgot, then the coinductive resumption monad is the guarded Elgot monad that freely extends it by the given endofunctor.
Cite as

Paul Blain Levy and Sergey Goncharov. Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{levy_et_al:LIPIcs.CALCO.2019.13,
  author =	{Levy, Paul Blain and Goncharov, Sergey},
  title =	{{Coinductive Resumption Monads: Guarded Iterative and Guarded Elgot}},
  booktitle =	{8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
  pages =	{13:1--13:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-120-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{139},
  editor =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.13},
  URN =		{urn:nbn:de:0030-drops-114414},
  doi =		{10.4230/LIPIcs.CALCO.2019.13},
  annote =	{Keywords: Guarded iteration, guarded monads, coalgebraic resumptions}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.221
Final Coalgebras from Corecursive Algebras

Authors: Paul Blain Levy

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

Abstract
We give a technique to construct a final coalgebra in which each element is a set of formulas of modal logic. The technique works for both the finite and the countable powerset functors. Starting with an injectively structured, corecursive algebra, we coinductively obtain a suitable subalgebra called the "co-founded part". We see—first with an example, and then in the general setting of modal logic on a dual adjunction—that modal theories form an injectively structured, corecursive algebra, so that this construction may be applied. We also obtain an initial algebra in a similar way. We generalize the framework beyond Set to categories equipped with a suitable factorization system, and look at the examples of Poset and Set-op .
Cite as

Paul Blain Levy. Final Coalgebras from Corecursive Algebras. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 221-237, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{levy:LIPIcs.CALCO.2015.221,
  author =	{Levy, Paul Blain},
  title =	{{Final Coalgebras from Corecursive Algebras}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{221--237},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.221},
  URN =		{urn:nbn:de:0030-drops-55365},
  doi =		{10.4230/LIPIcs.CALCO.2015.221},
  annote =	{Keywords: coalgebra, modal logic, bisimulation, category theory, factorization system}
}
Document
DOI: 10.4230/DagSemProc.10351.4
Limitations of Applicative Bisimulation (Preliminary Report)

Authors: Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii

Published in: Dagstuhl Seminar Proceedings, Volume 10351, Modelling, Controlling and Reasoning About State (2010)

Abstract
We present a series of examples that illuminate an important aspect of the semantics of higher-order functions with local state. Namely that certain behaviour of such functions can only be observed by pro- viding them with arguments that contain the functions themselves. This provides evidence for the necessity of complex conditions for functions in modern semantics for state, such as logical relations and Kripke-like bisimulations, where related functions are applied to related arguments (that may contain the functions). It also suggests that simpler semantics, such as those based on applicative bisimulations where functions are ap- plied to identical arguments, would not scale to higher-order languages with local state.
Cite as

Vasileios Koutavas, Paul Blain Levy, and Eijiro Sumii. Limitations of Applicative Bisimulation (Preliminary Report). In Modelling, Controlling and Reasoning About State. Dagstuhl Seminar Proceedings, Volume 10351, pp. 1-9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{koutavas_et_al:DagSemProc.10351.4,
  author =	{Koutavas, Vasileios and Levy, Paul Blain and Sumii, Eijiro},
  title =	{{Limitations of Applicative Bisimulation (Preliminary Report)}},
  booktitle =	{Modelling, Controlling and Reasoning About State},
  pages =	{1--9},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10351},
  editor =	{Amal Ahmed and Nick Benton and Lars Birkedal and Martin Hofmann},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10351.4},
  URN =		{urn:nbn:de:0030-drops-28074},
  doi =		{10.4230/DagSemProc.10351.4},
  annote =	{Keywords: Imperative languages, higher-order functions, local state}
}
  • Refine by Type
  • 15 Document/PDF
  • 12 Document/HTML

  • Refine by Publication Year
  • 3 2026
  • 9 2025
  • 1 2019
  • 1 2015
  • 1 2010

  • Refine by Author
  • 3 Levy, Paul Blain
  • 2 Goncharov, Sergey
  • 2 Schröder, Lutz
  • 2 Wild, Paul
  • 1 Aceto, Luca
  • Show More...

  • Refine by Series/Journal
  • 14 LIPIcs
  • 1 DagSemProc

  • Refine by Classification
  • 3 Theory of computation → Categorical semantics
  • 3 Theory of computation → Modal and temporal logics
  • 2 Theory of computation → Concurrency
  • 2 Theory of computation → Lambda calculus
  • 2 Theory of computation → Type theory
  • Show More...

  • Refine by Keyword
  • 3 modal logics
  • 2 bisimulation
  • 2 coalgebra
  • 1 (Bi-)simulations
  • 1 2-categories
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact