Volume 20, Issue 4

2024 Oct-Dec


1. History-deterministic Timed Automata

Sougata Bose ; Thomas A. Henzinger ; Karoliina Lehtinen ; Sven Schewe ; Patrick Totzke.
We explore the notion of history-determinism in the context of timed automata (TA) over infinite timed words. History-deterministic (HD) automata are those in which nondeterminism can be resolved on the fly, based on the run constructed thus far. History-determinism is a robust property that admits different game-based characterisations, and HD specifications allow for game-based verification without an expensive determinization step. We show that the class of timed $\omega$-languages recognized by HD timed automata strictly extends that of deterministic ones, and is strictly included in those recognised by fully non-deterministic TA. For non-deterministic timed automata it is known that universality is already undecidable for safety/reachability TA. For history-deterministic TA with arbitrary parity acceptance, we show that timed universality, inclusion, and synthesis all remain decidable and are EXPTIME-complete. For the subclass of TA with safety or reachability acceptance, one can decide (in EXPTIME) whether such an automaton is history-deterministic. If so, it can effectively determinized without introducing new automaton states.

2. Pre-measure spaces and pre-integration spaces in predicative Bishop-Cheng measure theory

Iosif Petrakis ; Max Zeuner.
Bishop's measure theory (BMT) is an abstraction of the measure theory of a locally compact metric space $X$, and the use of an informal notion of a set-indexed family of complemented subsets is crucial to its predicative character. The more general Bishop-Cheng measure theory (BCMT) is a constructive version of the classical Daniell approach to measure and integration, and highly impredicative, as many of its fundamental notions, such as the integration space of $p$-integrable functions $L^p$, rely on quantification over proper classes (from the constructive point of view). In this paper we introduce the notions of a pre-measure and pre-integration space, a predicative variation of the Bishop-Cheng notion of a measure space and of an integration space, respectively. Working within Bishop Set Theory (BST), and using the theory of set-indexed families of complemented subsets and set-indexed families of real-valued partial functions within BST, we apply the implicit, predicative spirit of BMT to BCMT. As a first example, we present the pre-measure space of complemented detachable subsets of a set $X$ with the Dirac-measure, concentrated at a single point. Furthermore, we translate in our predicative framework the non-trivial, Bishop-Cheng construction of an integration space from a given measure space, showing that a pre-measure space induces the pre-integration space of simple functions associated to it. Finally, a predicative construction of the canonically integrable […]

3. Formalising the Double-Pushout Approach to Graph Transformation

Robert Söldner ; Detlef Plump.
In this paper, we utilize Isabelle/HOL to develop a formal framework for the basic theory of double-pushout graph transformation. Our work includes defining essential concepts like graphs, morphisms, pushouts, and pullbacks, and demonstrating their properties. We establish the uniqueness of derivations, drawing upon Rosens 1975 research, and verify the Church-Rosser theorem using Ehrigs and Kreowskis 1976 proof, thereby demonstrating the effectiveness of our formalisation approach. The paper details our methodology in employing Isabelle/HOL, including key design decisions that shaped the current iteration. We explore the technical complexities involved in applying higher-order logic, aiming to give readers an insightful perspective into the engaging aspects of working with an Interactive Theorem Prover. This work emphasizes the increasing importance of formal verification tools in clarifying complex mathematical concepts.

4. A higher-order transformation approach to the formalization and analysis of BPMN using graph transformation systems

Tim Kräuter ; Adrian Rutle ; Harald König ; Yngve Lamo.
The Business Process Modeling Notation (BPMN) is a widely used standard notation for defining intra- and inter-organizational workflows. However, the informal description of the BPMN execution semantics leads to different interpretations of BPMN elements and difficulties in checking behavioral properties. In this article, we propose a formalization of the execution semantics of BPMN that, compared to existing approaches, covers more BPMN elements while also facilitating property checking. Our approach is based on a higher-order transformation from BPMN models to graph transformation systems. To show the capabilities of our approach, we implemented it as an open-source web-based tool.

5. Fair Asynchronous Session Subtyping

Mario Bravetti ; Julien Lange ; Gianluigi Zavattaro.
Session types are widely used as abstractions of asynchronous message passing systems. Refinement for such abstractions is crucial as it allows improvements of a given component without compromising its compatibility with the rest of the system. In the context of session types, the most general notion of refinement is asynchronous session subtyping, which allows message emissions to be anticipated w.r.t. a bounded amount of message consumptions. In this paper we investigate the possibility to anticipate emissions w.r.t. an unbounded amount of consumptions: to this aim we propose to consider fair compliance over asynchronous session types and fair refinement as the relation that preserves it. This allows us to propose a novel variant of session subtyping that leverages the notion of controllability from service contract theory and that is a sound characterisation of fair refinement. In addition, we show that both fair refinement and our novel subtyping are undecidable. We also present a sound algorithm which deals with examples that feature potentially unbounded buffering. Finally, we present an implementation of our algorithm and an empirical evaluation of it on synthetic benchmarks.

6. Asynchronous Session-Based Concurrency: Deadlock-freedom in Cyclic Process Networks

Bas van den Heuvel ; Jorge A. Pérez.
We tackle the challenge of ensuring the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks. Our contributions are twofold. First, we present Asynchronous Priority-based Classical Processes (APCP), a session-typed process framework that supports asynchronous communication, delegation, and recursion in cyclic process networks. Building upon the Curry-Howard correspondences between linear logic and session types, we establish essential meta-theoretical results for APCP, most notably deadlock freedom. Second, we present a new concurrent $\lambda$-calculus with asynchronous session types, dubbed LASTn. We illustrate LASTn by example and establish its meta-theoretical results; in particular, we show how to soundly transfer the deadlock-freedom guarantee from APCP. To this end, we develop a translation of terms in LASTn into processes in APCP that satisfies a strong formulation of operational correspondence.

7. A cone-theoretic barycenter existence theorem

Jean Goubault-Larrecq ; Xiaodong Jia.
We show that every continuous valuation on a locally convex, locally convex-compact, sober topological cone $\mathfrak{C}$ has a barycenter. This barycenter is unique, and the barycenter map $\beta$ is continuous, hence is the structure map of a $\mathbf V_{\mathrm w}$-algebra, i.e., an Eilenberg-Moore algebra of the extended valuation monad on the category of $T_0$ topological spaces; it is, in fact, the unique $\mathbf V_{\mathrm w}$-algebra that induces the cone structure on $\mathfrak{C}$.

8. String diagrams for Strictification and Coherence

Paul Wilson ; Dan Ghica ; Fabio Zanasi.
Whereas string diagrams for strict monoidal categories are well understood, and have found application in several fields of Computer Science, graphical formalisms for non-strict monoidal categories are far less studied. In this paper, we provide a presentation by generators and relations of string diagrams for non-strict monoidal categories, and show how this construction can handle applications in domains such as digital circuits and programming languages. We prove the correctness of our construction, which yields a novel proof of Mac Lane's strictness theorem. This in turn leads to an elementary graphical proof of Mac Lane's coherence theorem, and in particular allows for the inductive construction of the canonical isomorphisms in a monoidal category.

9. Sum and Tensor of Quantitative Effects

Giorgio Bacci ; Radu Mardare ; Prakash Panangaden ; Gordon Plotkin.
Inspired by the seminal work of Hyland, Plotkin, and Power on the combination of algebraic computational effects via sum and tensor, we develop an analogous theory for the combination of quantitative algebraic effects. Quantitative algebraic effects are monadic computational effects on categories of metric spaces, which, moreover, have an algebraic presentation in the form of quantitative equational theories, a logical framework introduced by Mardare, Panangaden, and Plotkin that generalises equational logic to account for a concept of approximate equality. As our main result, we show that the sum and tensor of two quantitative equational theories correspond to the categorical sum (i.e., coproduct) and tensor, respectively, of their effects qua monads. We further give a theory of quantitative effect transformers based on these two operations, essentially providing quantitative analogues to the following monad transformers due to Moggi: exception, resumption, reader, and writer transformers. Finally, as an application, we provide the first quantitative algebraic axiomatizations to the following coalgebraic structures: Markov processes, labelled Markov processes, Mealy machines, and Markov decision processes, each endowed with their respective bisimilarity metrics. Apart from the intrinsic interest in these axiomatizations, it is pleasing they have been obtained as the composition, via sum and tensor, of simpler quantitative equational theories.

10. Constructing Concise Characteristic Samples for Acceptors of Omega Regular Languages

Dana Angluin ; Dana Fisman.
A characteristic sample for a language $L$ and a learning algorithm $\textbf{L}$ is a finite sample of words $T_L$ labeled by their membership in $L$ such that for any sample $T \supseteq T_L$ consistent with $L$, on input $T$ the learning algorithm $\textbf{L}$ returns a hypothesis equivalent to $L$. Which omega automata have characteristic sets of polynomial size, and can these sets be constructed in polynomial time? We address these questions here. In brief, non-deterministic omega automata of any of the common types, in particular Büchi, do not have characteristic samples of polynomial size. For deterministic omega automata that are isomorphic to their right congruence automata, the fully informative languages, polynomial time algorithms for constructing characteristic samples and learning from them are given. The algorithms for constructing characteristic sets in polynomial time for the different omega automata (of types Büchi, coBüchi, parity, Rabin, Street, or Muller), require deterministic polynomial time algorithms for (1) equivalence of the respective omega automata, and (2) testing membership of the language of the automaton in the informative classes, which we provide.

11. Stochastic Processes with Expected Stopping Time

Krishnendu Chatterjee ; Laurent Doyen.
Markov chains are the de facto finite-state model for stochastic dynamical systems, and Markov decision processes (MDPs) extend Markov chains by incorporating non-deterministic behaviors. Given an MDP and rewards on states, a classical optimization criterion is the maximal expected total reward where the MDP stops after T steps, which can be computed by a simple dynamic programming algorithm. We consider a natural generalization of the problem where the stopping times can be chosen according to a probability distribution, such that the expected stopping time is T, to optimize the expected total reward. Quite surprisingly we establish inter-reducibility of the expected stopping-time problem for Markov chains with the Positivity problem (which is related to the well-known Skolem problem), for which establishing either decidability or undecidability would be a major breakthrough. Given the hardness of the exact problem, we consider the approximate version of the problem: we show that it can be solved in exponential time for Markov chains and in exponential space for MDPs.

12. Termination of Graph Transformation Systems Using Weighted Subgraph Counting

Roy Overbeek ; Jörg Endrullis.
We introduce a termination method for the algebraic graph transformation framework PBPO+, in which we weigh objects by summing a class of weighted morphisms targeting them. The method is well-defined in rm-adhesive quasitoposes (which include toposes and therefore many graph categories of interest), and is applicable to non-linear rules. The method is also defined for other frameworks, including SqPO and left-linear DPO, because we have previously shown that they are naturally encodable into PBPO+ in the quasitopos setting. We have implemented our method, and the implementation includes a REPL that can be used for guiding relative termination proofs.

13. On the relative asymptotic expressivity of inference frameworks

Vera Koponen ; Felix Weitkämper.
We consider logics with truth values in the unit interval $[0,1]$. Such logics are used to define queries and to define probability distributions. In this context the notion of almost sure equivalence of formulas is generalized to the notion of asymptotic equivalence. We prove two new results about the asymptotic equivalence of formulas where each result has a convergence law as a corollary. These results as well as several older results can be formulated as results about the relative asymptotic expressivity of inference frameworks. An inference framework $\mathbf{F}$ is a class of pairs $(\mathbb{P}, L)$, where $\mathbb{P} = (\mathbb{P}_n : n = 1, 2, 3, \ldots)$, $\mathbb{P}_n$ are probability distributions on the set $\mathbf{W}_n$ of all $\sigma$-structures with domain $\{1, \ldots, n\}$ (where $\sigma$ is a first-order signature) and $L$ is a logic with truth values in the unit interval $[0, 1]$. An inference framework $\mathbf{F}'$ is asymptotically at least as expressive as an inference framework $\mathbf{F}$ if for every $(\mathbb{P}, L) \in \mathbf{F}$ there is $(\mathbb{P}', L') \in \mathbf{F}'$ such that $\mathbb{P}$ is asymptotically total variation equivalent to $\mathbb{P}'$ and for every $\varphi(\bar{x}) \in L$ there is $\varphi'(\bar{x}) \in L'$ such that $\varphi'(\bar{x})$ is asymptotically equivalent to $\varphi(\bar{x})$ with respect to $\mathbb{P}$. This relation is a preorder. If, in addition, $\mathbf{F}$ is at […]

14. On the Semantic Expressiveness of Iso- and Equi-Recursive Types

Dominique Devriese ; Eric Mark Martin ; Marco Patrignani.
Recursive types extend the simply-typed lambda calculus (STLC) with the additional expressive power to enable diverging computation and to encode recursive data-types (e.g., lists). Two formulations of recursive types exist: iso-recursive and equi-recursive. The relative advantages of iso- and equi-recursion are well-studied when it comes to their impact on type-inference. However, the relative semantic expressiveness of the two formulations remains unclear so far. This paper studies the semantic expressiveness of STLC with iso- and equi-recursive types, proving that these formulations are equally expressive. In fact, we prove that they are both as expressive as STLC with only term-level recursion. We phrase these equi-expressiveness results in terms of full abstraction of three canonical compilers between these three languages (STLC with iso-, with equi-recursive types and with term-level recursion). Our choice of languages allows us to study expressiveness when interacting over both a simply-typed and a recursively-typed interface. The three proofs all rely on a typed version of a proof technique called approximate backtranslation. Together, our results show that there is no difference in semantic expressiveness between STLCs with iso- and equi-recursive types. In this paper, we focus on a simply-typed setting but we believe our results scale to more powerful type systems like System F.

15. Reasonable Space for the ${\lambda}$-Calculus, Logarithmically

Beniamino Accattoli ; Ugo Dal Lago ; Gabriele Vanoni.
Can the $\lambda$-calculus be considered a reasonable computational model? Can we use it for measuring the time $\textit{and}$ space consumption of algorithms? While the literature contains positive answers about time, much less is known about space. This paper presents a new reasonable space cost model for the $\lambda$-calculus, based on a variant over the Krivine abstract machine. For the first time, this cost model is able to accommodate logarithmic space. Moreover, we study the time behavior of our machine and show how to transport our results to the call-by-value $\lambda$-calculus.

16. Refl-Spanners: A Purely Regular Approach to Non-Regular Core Spanners

Markus L. Schmid ; Nicole Schweikardt.
The regular spanners (characterised by vset-automata) are closed under the algebraic operations of union, join and projection, and have desirable algorithmic properties. The core spanners (introduced by Fagin, Kimelfeld, Reiss, and Vansummeren (PODS 2013, JACM 2015) as a formalisation of the core functionality of the query language AQL used in IBM's SystemT) additionally need string-equality selections and it has been shown by Freydenberger and Holldack (ICDT 2016, Theory of Computing Systems 2018) that this leads to high complexity and even undecidability of the typical problems in static analysis and query evaluation. We propose an alternative approach to core spanners: by incorporating the string-equality selections directly into the regular language that represents the underlying regular spanner (instead of treating it as an algebraic operation on the table extracted by the regular spanner), we obtain a fragment of core spanners that, while having slightly weaker expressive power than the full class of core spanners, arguably still covers the intuitive applications of string-equality selections for information extraction and has much better upper complexity bounds of the typical problems in static analysis and query evaluation.

17. A Calculus for Scoped Effects & Handlers

Roger Bosman ; Birthe van den Berg ; Wenhao Tang ; Tom Schrijvers.
Algebraic effects & handlers have become a standard approach for side-effects in functional programming. Their modular composition with other effects and clean separation of syntax and semantics make them attractive to a wide audience. However, not all effects can be classified as algebraic; some need a more sophisticated handling. In particular, effects that have or create a delimited scope need special care, as their continuation consists of two parts-in and out of the scope-and their modular composition introduces additional complexity. These effects are called scoped and have gained attention by their growing applicability and adoption in popular libraries. While calculi have been designed with algebraic effects & handlers built in to facilitate their use, a calculus that supports scoped effects & handlers in a similar manner does not yet exist. This work fills this gap: we present $\lambda_{\mathit{sc}}$, a calculus with native support for both algebraic and scoped effects & handlers. It addresses the need for polymorphic handlers and explicit clauses for forwarding unknown scoped operations to other handlers. Our calculus is based on Eff, an existing calculus for algebraic effects, extended with Koka-style row polymorphism, and consists of a formal grammar, operational semantics, a (type-safe) type-and-effect system and type inference. We demonstrate $\lambda_{\mathit{sc}}$ on a range of examples.

18. Fine-grained Meta-Theorems for Vertex Integrity

Michael Lampis ; Valia Mitsou.
Vertex Integrity is a graph measure which sits squarely between two more well-studied notions, namely vertex cover and tree-depth, and that has recently gained attention as a structural graph parameter. In this paper we investigate the algorithmic trade-offs involved with this parameter from the point of view of algorithmic meta-theorems for First-Order (FO) and Monadic Second Order (MSO) logic. Our positive results are the following: (i) given a graph $G$ of vertex integrity $k$ and an FO formula $\phi$ with $q$ quantifiers, deciding if $G$ satisfies $\phi$ can be done in time $2^{O(k^2q+q\log q)}+n^{O(1)}$; (ii) for MSO formulas with $q$ quantifiers, the same can be done in time $2^{2^{O(k^2+kq)}}+n^{O(1)}$. Both results are obtained using kernelization arguments, which pre-process the input to sizes $2^{O(k^2)}q$ and $2^{O(k^2+kq)}$ respectively. The complexities of our meta-theorems are significantly better than the corresponding meta-theorems for tree-depth, which involve towers of exponentials. However, they are worse than the roughly $2^{O(kq)}$ and $2^{2^{O(k+q)}}$ complexities known for corresponding meta-theorems for vertex cover. To explain this deterioration we present two formula constructions which lead to fine-grained complexity lower bounds and establish that the dependence of our meta-theorems on $k$ is the best possible. More precisely, we show that it is not possible to decide FO formulas with $q$ quantifiers in time $2^{o(k^2q)}$, and that there exists a […]

19. Universal Quantitative Algebra for Fuzzy Relations and Generalised Metric Spaces

Matteo Mio ; Ralph Sarkis ; Valeria Vignudelli.
We present a generalisation of the theory of quantitative algebras of Mardare, Panangaden and Plotkin where (i) the carriers of quantitative algebras are not restricted to be metric spaces and can be arbitrary fuzzy relations or generalised metric spaces, and (ii) the interpretations of the algebraic operations are not required to be nonexpansive. Our main results include: a novel sound and complete proof system, the proof that free quantitative algebras always exist, the proof of strict monadicity of the induced Free-Forgetful adjunction, the result that all monads (on fuzzy relations) that lift finitary monads (on sets) admit a quantitative equational presentation.

20. A Truly Concurrent Semantics for Reversible CCS

Hernán Melgratti ; Claudio Antares Mezzina ; G. Michele Pinna.
Reversible CCS (RCCS) is a well-established, formal model for reversible communicating systems, which has been built on top of the classical Calculus of Communicating Systems (CCS). In its original formulation, each CCS process is equipped with a memory that records its performed actions, which is then used to reverse computations. More recently, abstract models for RCCS have been proposed in the literature, basically, by directly associating RCCS processes with (reversible versions of) event structures. In this paper we propose a different abstract model: starting from one of the well-known encoding of CCS into Petri nets we apply a recently proposed approach to incorporate causally-consistent reversibility to Petri nets, obtaining as result the (reversible) net counterpart of every RCCS term.

21. Kleene Theorem for Higher-Dimensional Automata

Uli Fahrenberg ; Christian Johansen ; Georg Struth ; Krzysztof Ziemiański.
We prove a Kleene theorem for higher-dimensional automata. It states that the languages they recognise are precisely the rational subsumption-closed sets of finite interval pomsets. The rational operations on these languages include a gluing composition, for which we equip pomsets with interfaces. For our proof, we introduce higher-dimensional automata with interfaces, which are modelled as presheaves over labelled precube categories, and develop tools and techniques inspired by algebraic topology, such as cylinders and (co)fibrations. Higher-dimensional automata form a general model of non-interleaving concurrency, which subsumes many other approaches. Interval orders are used as models for concurrent and distributed systems where events extend in time. Our tools and techniques may therefore yield templates for Kleene theorems in various models and applications.

22. On the Home-Space Problem for Petri Nets and its Ackermannian Complexity

Petr Jančar ; Jérôme Leroux.
A set of configurations $H$ is a home-space for a set of configurations $X$ of aPetri net if every configuration reachable from (any configuration in) $X$ can reach (some configuration in) $H$. The semilinear home-space problem for Petri nets asks, given a Petri net and semilinear sets of configurations $X$, $H$, if $H$ is a home-space for $X$. In 1989, David de Frutos Escrig and Colette Johnen proved that the problem is decidable when $X$ is a singleton and $H$ is a finite union of linear sets with the same periods. In this paper, we show that the general (semilinear) problem is decidable. This result is obtained by proving a duality between the reachability problem and the non-home-space problem. In particular, we prove that for any Petri net and any semilinear set of configurations $H$ we can effectively compute a semilinear set $C$ of configurations, called a non-reachability core for $H$, such that for every set $X$ the set $H$ is not a home-space for $X$ if, and only if, $C$ is reachable from $X$. We show that the established relation to the reachability problem yields the Ackermann-completeness of the (semilinear) home-space problem. For this we also show that, given a Petri net with an initial marking, the set of minimal reachable markings can be constructed in Ackermannian time.