Skip to main content
EXTENDED SEARCH
Log in
Top

Open Access 2025 | Open Access | Book

Foundations of Software Science and Computation Structures

28th International Conference, FoSSaCS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3–8, 2025, Proceedings

Editors: Parosh Aziz Abdulla, Delia Kesner

Publisher: Springer Nature Switzerland

Book Series : Lecture Notes in Computer Science

Part of: Springer Professional "Business + Economics & Engineering + Technology" , Springer Professional "Engineering + Technology" , Springer Professional "Business + Economics"

Table of Contents
insite
SEARCH

About this book

This open access book constitutes the proceedings of the 28th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2025, which took place in Hamilton, Canada, during May 2025, held as part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025.

The 19 papers included in these proceedings were carefully reviewed and selected from 58 submissions. They focus on foundational research in software science on theories and methods to support the analysis, integration, synthesis, transformation, and verification of programs and software systems.

Table of Contents

Frontmatter
PDF

Open Access

Context-Free Languages of String Diagrams
Abstract
We introduce context-free languages of morphisms in monoidal categories, extending recent work on the categorification of context-free languages, and regular languages of string diagrams. Context-free languages of string diagrams include classical context-free languages of words, trees, and hypergraphs, when instantiated over appropriate monoidal categories. We prove a representation theorem for context-free languages of string diagrams: every such language arises as the image under a monoidal functor of a regular language of string diagrams.
Matt Earnshaw, Mario Román
PDF View full text

Open Access

A Behavioural Pseudometric for Continuous-Time Markov Processes
Abstract
In this work, we generalize the concept of bisimulation metric in order to metrize the behaviour of continuous-time processes. Similarly to what is done for discrete-time systems, we follow two approaches and show that they coincide: as a fixpoint of a functional and through a real-valued logic.
The whole discrete-time approach relies entirely on the step-based dynamics: the process jumps from state to state. We define a behavioural pseudometric for processes that evolve continuously through time, such as Brownian motion or involve jumps or both.
Linan Chen, Florence Clerc, Prakash Panangaden
PDF View full text

Open Access

Idempotent Resources in Separation Logic
The Heart of core in Iris
Abstract
We revisit the foundational notion of “resources” used by separation logics from a categorical and algebraic viewpoint. In particular, we show that the cameras used by concurrent, higher-order, impredicative separation logics like Iris as a generalization of partial commutative monoids can be simplified and clarified and we introduce a category of cameras in which many vital cameras exhibit simple universal properties. We do this by observing that an important structure on cameras (the core operator) can be uniquely constrained and replaced by the property governing the idempotent elements of the camera. We verify that all cameras used in practice in Iris satisfy this property and use this insight to simplify the existing Iris formalization.
Daniel Gratzer, Mathias Adam Møller, Lars Birkedal
PDF View full text

Open Access

Alternative Characterizations of Hereditary History-Preserving Bisimilarity via Backward Ready Multisets
Abstract
We provide two alternative characterizations of hereditary history-preserving bisimilarity: a denotational one, on stable configuration structures, and an operational one, on a reversible process calculus. The characterizing equivalence is forward-reverse bisimilarity extended with a check for backward ready multiset equality. Unlike previous approaches, the focus is thus on counting identically labeled events rather than uniquely identifying them. We also investigate the relationships between event identifier logic, characterizing the former bisimilarity, and backward ready multiset logic, characterizing the latter bisimilarity.
Marco Bernardo, Andrea Esposito, Claudio A. Mezzina
PDF View full text

Open Access

Complementation of Emerson-Lei Automata
Abstract
We give new constructions for complementing subclasses of Emerson-Lei automata using modifications of rank-based Büchi automata complementation. In particular, we propose a specialized rank-based construction for a Boolean combination of Inf acceptance conditions, which heavily relies on a novel way of a run DAG labelling enhancing the ranking functions with models of the acceptance condition. Moreover, we propose a technique for complementing generalized Rabin automata, which are structurally as concise as general Emerson-Lei automata (but can have a larger acceptance condition). The construction is modular in the sense that it extends a given complementation algorithm for a condition \(\varphi \) in a way that the resulting procedure handles conditions of the form \(\text {Fin}\wedge \varphi \). The proposed constructions give upper bounds that are exponentially better than the state of the art for some of the classes.
Vojtěch Havlena, Ondřej Lengál, Barbora Šmahlíková
PDF View full text

Open Access

Relational Connectors and Heterogeneous Simulations
Abstract
While behavioural equivalences among systems of the same type, such as Park/Milner bisimilarity of labelled transition systems, are an established notion, a systematic treatment of relationships between systems of different types is currently missing. We provide such a treatment in the framework of universal coalgebra, in which the type of a system (nondeterministic, probabilistic, weighted, game-based etc.) is abstracted as a set functor: We introduce relational connectors among set functors, which induce notions of heterogeneous (bi)simulation among coalgebras of the respective types. We give a number of constructions on relational connectors. In particular, we identify composition and converse operations on relational connectors; we construct corresponding identity relational connectors, showing that the latter generalize the standard Barr extension of weak-pullback-preserving functors; and we introduce a Kantorovich construction in which relational connectors are induced from relations between modalities. For Kantorovich relational connectors, one has a notion of dual-purpose modal logic interpreted over both system types, and we prove a corresponding Hennessy-Milner-type theorem stating that generalized (bi)similarity coincides with theory inclusion on finitely-branching systems. We apply these results to a number of example scenarios involving labelled transition systems with different label alphabets, probabilistic systems, and input/output conformances.
Pedro Nora, Jurriaan Rot, Lutz Schröder, Paul Wild
PDF View full text

Open Access

On the cut-elimination of the modal -calculus: Linear Logic to the rescue
Abstract
This paper presents a proof-theoretic analysis of the modal \(\mu \)-calculus. More precisely, we prove a syntactic cut-elimination for the non-wellfounded modal \(\mu \)-calculus, using methods from linear logic. and its exponential modalities. To achieve this, we introduce a new system, \(\mu \textsf {LL}_{\Box }^{\infty }\), which is a linear version of the modal \(\mu \)-calculus, intertwining the modalities from the modal \(\mu \)-calculus with the exponential modalities from linear logic. Our strategy for proving cut-elimination involves (i) proving cut-elimination for \(\mu \textsf {LL}_{\Box }^{\infty }\) and (ii) translating proofs of the modal mu-calculus into this new system via a “linear translation”, allowing us to extract the cut-elimination result.
Esaïe Bauer, Alexis Saurin
PDF View full text

Open Access

Combining quantum and classical control: syntax, semantics and adequacy
Abstract
The two main notions of control in quantum programming languages are often referred to as “quantum” control and “classical” control. With the latter, the control flow is based on classical information, potentially resulting from a quantum measurement, and this paradigm is well-suited to mixed state quantum computation. Whereas with quantum control, we are primarily focused on pure quantum computation and there the “control” is based on superposition.  The two paradigms have not mixed well traditionally and they are almost always treated separately. In this work, we show that the paradigms may be combined within the same system. The key ingredients for achieving this are: (1) syntactically: a modality for incorporating pure quantum types into a mixed state quantum type system; (2) operationally: an adaptation of the notion of “quantum configuration” from quantum lambda-calculi, where the quantum data is replaced with pure quantum primitives; (3) denotationally: suitable (sub)categories of Hilbert spaces, for pure computation and von Neumann algebras, for mixed state computation in the Heisenberg picture of quantum mechanics.
Kinnari Dave, Louis Lemonnier, Romain Péchoux, Vladimir Zamdzhiev
PDF View full text

Open Access

Quantifier Elimination and Craig Interpolation: The Quantitative Way
Abstract
Quantifier elimination (QE) and Craig interpolation (CI) are central to various state-of-the-art automated approaches to hardware- and software verification. They are rooted in the Boolean setting and are successful for, e.g., first-order theories such as linear rational arithmetic. What about their applicability in the quantitative setting where formulae evaluate to numbers and quantitative supremum/infimum quantifiers are the natural pendant to traditional Boolean quantifiers? Applications include establishing quantitative properties of programs such as bounds on expected outcomes of probabilistic programs featuring unbounded non-determinism and analyzing the flow of information through programs.
In this paper, we present the - to the best of our knowledge - first QE algorithm for possibly unbounded, \(\infty \)- or \((-\infty )\)-valued, or discontinuous piecewise linear quantities. They are the quantitative counterpart to linear rational arithmetic, and are a popular quantitative assertion language for probabilistic program verification. We provide rigorous soundness proofs as well as upper space complexity bounds. Moreover, our algorithm yields a quantitative CI theorem: Given arbitrary piecewise linear quantities \(f,g\) with \(f\models g\), both the strongest and the weakest Craig interpolant of \(f\) and \(g\) are quantifier-free and effectively constructible.
Kevin Batz, Joost-Pieter Katoen, Nora Orhan
PDF View full text

Open Access

Complete Test Suites for Automata in Monoidal Closed Categories
Abstract
Conformance testing of automata is about checking the equivalence of a known specification and a black-box implementation. An important notion in conformance testing is that of a complete test suite, which guarantees that if an implementation satisfying certain conditions passes all tests, then it is equivalent to the specification.
We introduce a framework for proving completeness of test suites at the general level of automata in monoidal closed categories. Moreover, we provide a generalization of a classical conformance testing technique, the W-method. We demonstrate the applicability of our results by recovering the W-method for deterministic finite automata, Moore machines, and Mealy machines, and by deriving new instances of complete test suites for weighted automata and deterministic nominal automata.
Bálint Kocsis, Jurriaan Rot
PDF View full text

Open Access

Temporal Hyperproperties for Population Protocols
Abstract
Hyperproperties are properties over sets of traces (or runs) of a system, as opposed to properties of just one trace. They were introduced in 2010 and have been much studied since, in particular via an extension of the temporal logic LTL called HyperLTL. Most verification efforts for HyperLTL are restricted to finite-state systems, usually defined as Kripke structures. In this paper we study hyperproperties for an important class of infinite-state systems. We consider population protocols, a popular distributed computing model in which arbitrarily many identical finite-state agents interact in pairs. Population protocols are a good candidate for studying hyperproperties because the main decidable verification problem, well-specification, is a hyperproperty. We first show that even for simple (monadic) formulas, HyperLTL verification for population protocols is undecidable. We then turn our attention to immediate observation population protocols, a simpler and well-studied subclass of population protocols. We show that verification of monadic HyperLTL formulas without the next operator is decidable in 2-EXPSPACE, but that all extensions make the problem undecidable.
Nicolas Waldburger, Chana Weil-Kennedy, Pierre Ganty, César Sánchez
PDF View full text

Open Access

BiGKAT: An Algebraic Framework for Relational Verification of Probabilistic Programs
Abstract
This work is devoted to formal reasoning on relational properties of probabilistic imperative programs. Relational properties are properties which relate the execution of two programs (possibly the same one) on two initial memories. We aim at extending the algebraic approach of Kleene Algebras with Tests (KAT) to relational properties of probabilistic programs. For that we consider the approach of Guarded Kleene Algebras with Tests (GKAT), which can be used for representing probabilistic programs, and define a relational version of it, called Bi-guarded Kleene Algebras with Tests (BiGKAT) together with a semantics. We show that the setting of BiGKAT is expressive enough to encode a finitary version of probabilistic Relational Hoare Logic (pRHL) (without the While rule), a program logic that has been introduced in the literature for the verification of relational properties of probabilistic programs. We also discuss the additional expressivity brought by BiGKAT.
Leandro Gomes, Patrick Baillot, Marco Gaboardi
PDF View full text

Open Access

A General Completeness Theorem for Skip-Free Star Algebras
Abstract
We consider process algebras with branching parametrized by an equational theory \(\textsf{T}\), and show that it is possible to axiomatize bisimilarity under certain conditions on \(\textsf{T}\). Our proof abstracts an earlier argument due to Grabmayer and Fokkink (LICS’20), and yields new completeness theorems for skip-free process algebras with probabilistic (guarded) branching, while also covering existing completeness results.
Tobias Kappé, Todd Schmid
PDF View full text

Open Access

Sharing and Linear Logic with Restricted Access
Abstract
The two Girard translations provide two different means of obtaining embeddings of Intuitionistic Logic into Linear Logic, corresponding to different lambda-calculus calling mechanisms. The translations, mapping \(A\rightarrow B\) respectively to \({!}{A}\multimap B\) and \({!}{(A\multimap B)}\), have been shown to correspond respectively to call-by-name and call-by-value.
In this work, we split the of-course modality of linear logic into two modalities, written “\({!} \)” and “\(\bullet \)”. Intuitively, the modality “\({!} \)” specifies a subproof that can be duplicated and erased, but may not necessarily be “accessed”, i.e. interacted with, while the combined modality “\({!}{\bullet }\)” specifies a subproof that can moreover be accessed. The resulting system, called \(\textsf{MSCLL}\), enjoys cut-elimination and is conservative over \(\textsf{MELL}\).
We study how restricting access to subproofs provides ways to control sharing in evaluation strategies. For this, we introduce a term-assignment for an intuitionistic fragment of \(\textsf{MSCLL}\), called the \(\lambda ^{{!}{\bullet }}\)-calculus, which we show to enjoy subject reduction, confluence, and strong normalization of the simply typed fragment. We propose three sound and complete translations that respectively simulate call-by-name, call-by-value, and a variant of call-by-name that shares the evaluation of its arguments (similarly as in call-by-need). The translations are extended to simulate the Bang-calculus, as well as weak reduction strategies.
Pablo Barenbaum, Eduardo Bonelli
PDF View full text

Open Access

A Diagrammatic Algebra for Program Logics
Abstract
Tape diagrams provide a convenient graphical notation for arrows of rig categories, i.e., categories equipped with two monoidal products, \(\oplus \) and \(\otimes \). In this work, we introduce Kleene-Cartesian rig categories, namely rig categories where \(\otimes \) provides a Cartesian bicategory, while \(\oplus \) a Kleene bicategory.We show that the associated tape diagrams can conveniently deal with Hoare logic.
Filippo Bonchi, Alessandro Di Giorgio, Elena Di Lavore
PDF View full text

Open Access

Fair Quantitative Games
Abstract
We examine two-player games over finite weighted graphs with quantitative (mean-payoff or energy) objective, where one of the players additionally needs to satisfy a fairness objective. The specific fairness we consider is called strong transition fairness, given by a subset of edges of one of the players, which asks the player to take fair edges infinitely often if their source nodes are visited infinitely often. We show that when fairness is imposed on player 1, these games fall within the class of previously studied \(\omega \)-regular mean-payoff and energy games. On the other hand, when the fairness is on player 2, to the best of our knowledge, these games have not been previously studied. We provide gadget-based algorithms for fair mean-payoff games where fairness is imposed on either player, and for fair energy games where the fairness is imposed on player 1. For all variants of fair mean-payoff and fair energy (under unknown initial credit) games, we give pseudo-polynomial algorithms to compute the winning regions of both players. Additionally, we analyze the strategy complexities required for these games. Our work is the first to extend the study of strong transition fairness, as well as gadget-based approaches, to the quantitative setting. We thereby demonstrate that the simplicity of strong transition fairness, as well as the applicability of gadget-based techniques, can be leveraged beyond the \(\omega \)-regular domain.
Ashwani Anand, Satya Prakash Nayak, Ritam Raha, Irmak Sağlam, Anne-Kathrin Schmuck
PDF View full text

Open Access

Structural Liveness of Conservative Petri Nets
Abstract
We show that the EXPSPACE-hardness result for structural liveness of Petri nets [Jančar and Purser, 2019] holds even for a simple subclass of conservative nets. As the main result we then show that for structurally live conservative nets the values of the least live markings are at most double exponential in the size of the nets, which entails the EXPSPACE-completeness of structural liveness for conservative Petri nets; the complexity of the general case remains unclear. As a proof ingredient with a potential of wider applicability, we present an extension of the known results bounding the smallest integer solutions of boolean combinations of linear (in)equations and divisibility constraints.
Petr Jančar, Jérôme Leroux, Jiří Valůšek
PDF View full text

Open Access

Two-sorted algebraic decompositions of Brookes’s shared-state denotational semantics
Abstract
We define a two sorted equational theory of algebraic effects that models concurrent shared state with preemptive interleaving, recovering Brookes’s seminal 1996 trace-based model precisely. The decomposition allows us to analyse Brookes’s model algebraically in terms of separate but interacting components. The multiple sorts partition terms into layers. We use two sorts: a “hold” sort for layers that disallow interleaving of environment memory accesses, analogous to holding a global lock on the memory; and a “cede” sort for the opposite. The algebraic signature comprises of independent interlocking components: two new operators that switch between these sorts, delimiting the atomic layers, thought of as acquiring and releasing the global lock; non-deterministic choice; and state-accessing operators. The axioms similarly divide cleanly: the delimiters behave as a closure pair; all operators are strict, and distribute over non-empty non-deterministic choice; and non-deterministic global state obeys Plotkin and Power’s presentation of global state. Our representation theorem expresses the free algebras over a two-sorted family of variables as sets of traces with suitable closure conditions. When the held sort has no variables, we recover Brookes’s trace semantics. We define several other single-and two-sorted theories to elucidate the connection to Brookes’s model via translation embeddings and equivalences.
Yotam Dvir, Ohad Kammar, Ori Lahav, Gordon Plotkin
PDF View full text

Open Access

Model-Checking Real-Time Systems: Revisiting the Alternating Automaton Route
Abstract
Alternating timed automata (ATA) are an extension of timed automata, that are closed under complementation and hence amenable to logic-to-automata translations. Several timed logics, including Metric Temporal Logic (MTL), can be converted to equivalent 1-clock ATAs (1-ATAs). Satisfiability of an MTL formula reduces to checking emptiness of a 1-ATA. Furthermore, algorithms for 1-ATA emptiness can be adapted for model-checking timed automata models against 1-ATA specifications. However, existing emptiness algorithms for 1-ATA proceed by an extended region construction, and are not suitable for implementations.
In this work, we initiate the study of zone-based methods for 1-ATAs. The challenge here, as opposed to timed automata, is the fact that the zone graph may generate an unbounded number of variables. We first introduce a deactivation operation to the 1-ATA syntax that allows for an explicit deactivation of the clock in transitions. Using the deactivation operation, we improve the existing MTL-to-1-ATA conversion and present a fragment of MTL for which the equivalent 1-ATA generate a bounded number of variables. Secondly, we develop the idea of zones for 1-ATA and present an emptiness algorithm which explores a corresponding zone graph. For termination, a special entailment check between zones is necessary. Our main technical contributions are: (1) an algorithm for the entailment check using simple zone operations and (2) an \(\textsf{NP}\)-hardness for the entailment check in the general case. Finally, for 1-ATA which generate a bounded number of variables, we present a modified entailment check with quadratic complexity.
Patricia Bouyer, B. Srivathsan, Vaishnavi Vishwanath
PDF View full text
Backmatter
PDF
Metadata
Title
Foundations of Software Science and Computation Structures
Editors
Parosh Aziz Abdulla
Delia Kesner
Copyright Year
2025
Electronic ISBN
978-3-031-90897-2
Print ISBN
978-3-031-90896-5
DOI
https://doi.org/10.1007/978-3-031-90897-2

Premium Partner

    Image Credits