Weakest precondition transformers are useful tools in program verification. One of their key properties is composability, that is, the weakest precondition predicate transformer (wppt for short) associated to program $f;\;g$ should be equal to the composition of the wppts associated to f and g. In this paper, we study the categorical structure behind wppts from a fibrational point of view. We characterize the wppts that satisfy composability as the ones constructed from the Cartesian lifting of a monad. We moreover show that Cartesian liftings of monads along lax slice categories bijectively correspond to Eilenberg–Moore monotone algebras. We then instantiate our techniques by deriving wppts for commonplace effects such as the maybe monad, the nonempty powerset monad, the counter monad, or the distribution monad. We also show how to combine them to derive the wppts appearing in the literature of verification of probabilistic programs.

This paper introduces a class of automata and associated languages, suitable to model a computational paradigm of fuzzy systems, in which both vagueness and simultaneity are taken as first-class citizens. This requires a weighted semantics for transitions and a precise notion of a synchronous product to enforce the simultaneous occurrence of actions. The usual relationships between automata and languages are revisited in this setting, including a specific Kleene theorem.

We introduce a novel amortised resource analysis couched in a type-and-effect system. Our analysis is formulated in terms of the physicist’s method of amortised analysis and is potentialbased. The type system makes use of logarithmic potential functions and is the first such system to exhibit logarithmic amortised complexity. With our approach, we target the automated analysis of self-adjusting data structures, like splay trees, which so far have only manually been analysed in the literature. In particular, we have implemented a semi-automated prototype, which successfully analyses the zig-zig case of splaying, once the type annotations are fixed.

Given the complexity of cyber-physical systems (CPS), such as swarms of drones, often deviations, from a planned mission or protocol, occur which may in some cases lead to harm and losses. To increase the robustness of such systems, it is necessary to detect when deviations happen and diagnose the cause(s) for a deviation. We build on our previous work on soft agents, a formal framework based on using rewriting logic for specifying and reasoning about distributed CPS, to develop methods for diagnosis of CPS at design time. We accomplish this by (1) extending the soft agents framework with Fault Models; (2) proposing a protocol specification language and the definition of protocol deviations; and (3) development of workflows/algorithms for detection and diagnosis of protocol deviations. Our approach is partially inspired by existing work using counterfactual reasoning for fault ascription. We demonstrate our machinery with a collection of experiments.

Given a plane graph $G=(V,E)$ , a Petrie tour of G is a tour P of G that alternately turns left and right at each step. A Petrie tour partition of G is a collection ${\mathscr P}=\{P_1,\ldots,P_q\}$ of Petrie tours so that each edge of G is in exactly one tour $P_i \in {\mathscr P}$ . A Petrie tour P is called a Petrie cycle if all its vertices are distinct. A Petrie cycle partition of G is a collection ${\mathscr C}=\{C_1,\ldots,C_p\}$ of Petrie cycles so that each vertex of G is in exactly one cycle $C_i \in {\mathscr C}$ . In this paper, we study the properties of 3-regular plane graphs that have Petrie cycle partitions and 4-regular plane multi-graphs that have Petrie tour partitions. Given a 4-regular plane multi-graph $G=(V,E)$ , a 3-regularization of G is a 3-regular plane graph $G_3$ obtained from G by splitting every vertex $v\in V$ into two degree-3 vertices. G is called Petrie partitionable if it has a 3-regularization that has a Petrie cycle partition. The general version of this problem is motivated by a data compression method, tristrip, used in computer graphics. In this paper, we present a simple characterization of Petrie partitionable graphs and show that the problem of determining if G is Petrie partitionable is NP-complete.

This paper gives a new proof of confluence for Carraro and Guerrieri’s call-by-value lambda calculus λ v σ with permutation rules. We adapt the compositional Z theorem to λ v σ .

Symmetric monoidal theories (SMTs) generalise algebraic theories in a way that make them suitable to express resource-sensitive systems, in which variables cannot be copied or discarded at will. In SMTs, traditional tree-like terms are replaced by string diagrams, topological entities that can be intuitively thought of as diagrams of wires and boxes. Recently, string diagrams have become increasingly popular as a graphical syntax to reason about computational models across diverse fields, including programming language semantics, circuit theory, quantum mechanics, linguistics, and control theory. In applications, it is often convenient to implement the equations appearing in SMTs as rewriting rules. This poses the challenge of extending the traditional theory of term rewriting, which has been developed for algebraic theories, to string diagrams. In this paper, we develop a mathematical theory of string diagram rewriting for SMTs. Our approach exploits the correspondence between string diagram rewriting and double pushout (DPO) rewriting of certain graphs, introduced in the first paper of this series. Such a correspondence is only sound when the SMT includes a Frobenius algebra structure. In the present work, we show how an analogous correspondence may be established for arbitrary SMTs, once an appropriate notion of DPO rewriting (which we call convex) is identified. As proof of concept, we use our approach to show termination of two SMTs of interest: Frobenius semi-algebras and bialgebras.

By using algebraic structures in a presheaf category over finite sets, following Fiore, Plotkin and Turi, we develop sound and complete models of second-order rewriting systems called second-order computation systems (CSs). Restricting the algebraic structures to those equipped with well-founded relations, we obtain a complete characterisation of terminating CSs. We also extend the characterisation to rewriting on meta-terms using the notion of $\Sigma$ -monoid.