-
Interacting Monoidal Structures with Applications in Computing
Authors:
James Cranch,
Georg Struth
Abstract:
With a view on applications in computing, in particular concurrency theory and higher-dimensional rewriting, we develop notions of $n$-fold monoid and comonoid objects in $n$-fold monoidal categories and bicategories. We present a series of examples for these structures from various domains, including a categorical model for a communication protocol and a lax $n$-fold relational monoid, which has…
▽ More
With a view on applications in computing, in particular concurrency theory and higher-dimensional rewriting, we develop notions of $n$-fold monoid and comonoid objects in $n$-fold monoidal categories and bicategories. We present a series of examples for these structures from various domains, including a categorical model for a communication protocol and a lax $n$-fold relational monoid, which has previously been used implicitly for higher-dimensional rewriting and which specialises in a natural way to strict $n$-categories. A special set of examples is built around modules and algebras of the boolean semiring, which allows us to deal with semilattices, additively idempotent semirings and quantales using tools from classical algebra.
△ Less
Submitted 6 November, 2024;
originally announced November 2024.
-
Presheaf automata
Authors:
Georg Struth,
Krzysztof Ziemiański
Abstract:
We introduce presheaf automata as a generalisation of different variants of higher-dimensional automata and other automata-like formalisms, including Petri nets and vector addition systems. We develop the foundations of a language theory for them based on notions of paths and track objects. We also define open maps for presheaf automata, extending the standard notions of simulation and bisimulatio…
▽ More
We introduce presheaf automata as a generalisation of different variants of higher-dimensional automata and other automata-like formalisms, including Petri nets and vector addition systems. We develop the foundations of a language theory for them based on notions of paths and track objects. We also define open maps for presheaf automata, extending the standard notions of simulation and bisimulation for transition systems. Apart from these conceptual contributions, we show that certain finite-type presheaf automata subsume all Petri nets, generalising a previous result by van Glabbeek, which applies to higher-dimensional automata and safe Petri nets.
△ Less
Submitted 6 September, 2024;
originally announced September 2024.
-
Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL
Authors:
Jonathan Julián Huerta y Munive,
Simon Foster,
Mario Gleirscher,
Georg Struth,
Christian Pardillo Laursen,
Thomas Hickman
Abstract:
We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), a framework for the verification of cyber-physical systems. We describe the semantic foundations of the framework's formalisation in the Isabelle/HOL proof assistant. A user-friendly language specification based on a robust state model makes our framework flexible and adaptable to various engineering workf…
▽ More
We formally introduce IsaVODEs (Isabelle verification with Ordinary Differential Equations), a framework for the verification of cyber-physical systems. We describe the semantic foundations of the framework's formalisation in the Isabelle/HOL proof assistant. A user-friendly language specification based on a robust state model makes our framework flexible and adaptable to various engineering workflows. New additions to the framework increase both its expressivity and proof automation. Specifically, formalisations related to forward diamond correctness specifications, certification of unique solutions to ordinary differential equations (ODEs) as flows, and invariant reasoning for systems of ODEs contribute to the framework's scalability and usability. Various examples and an evaluation validate the effectiveness of our framework.
△ Less
Submitted 22 January, 2024;
originally announced January 2024.
-
Single-set cubical categories and their formalisation with a proof assistant (extended version)
Authors:
Philippe Malbos,
Tanguy Massacrier,
Georg Struth
Abstract:
We introduce a single-set axiomatisation of cubical $ω$-categories, including connections and inverses. We justify these axioms by establishing a series of equivalences between the category of single-set cubical $ω$-categories, and their variants with connections and inverses, and the corresponding cubical $ω$-categories. We also report on the formalisation of cubical $ω$-categories with the Isabe…
▽ More
We introduce a single-set axiomatisation of cubical $ω$-categories, including connections and inverses. We justify these axioms by establishing a series of equivalences between the category of single-set cubical $ω$-categories, and their variants with connections and inverses, and the corresponding cubical $ω$-categories. We also report on the formalisation of cubical $ω$-categories with the Isabelle/HOL proof assistant, which has been instrumental in developing the single-set axiomatisation.
△ Less
Submitted 4 July, 2024; v1 submitted 19 January, 2024;
originally announced January 2024.
-
Higher Catoids, Higher Quantales and their Correspondences
Authors:
Cameron Calk,
Philippe Malbos,
Damien Pous,
Georg Struth
Abstract:
This article is part of a programme on the formalisation of higher categories and the categorification of rewriting theory. Set-valued structures such as catoids are used in this context to formalise local categorical composition operations. We introduce omega-catoids as set-valued generalisations of (strict) omega-categories. We establish modal correspondences between omega-catoids and convolutio…
▽ More
This article is part of a programme on the formalisation of higher categories and the categorification of rewriting theory. Set-valued structures such as catoids are used in this context to formalise local categorical composition operations. We introduce omega-catoids as set-valued generalisations of (strict) omega-categories. We establish modal correspondences between omega-catoids and convolution omega-quantales. These are related to Jónsson-Tarski-style dualities between relational structures and lattices with operators. Convolution omega-quantales generalise the powerset omega-Kleene algebras recently proposed for algebraic coherence proofs in higher rewriting to weighted variants in the style of category algebras. In order to capture homotopic constructions and proofs in rewriting theory, we extend these correspondances to higher catoids with a groupoid structure above some dimension, which is reflected by an involution in higher quantales.
△ Less
Submitted 11 February, 2024; v1 submitted 18 July, 2023;
originally announced July 2023.
-
Modal Algebra of Multirelations
Authors:
Hitoshi Furusawa,
Walter Guttmann,
Georg Struth
Abstract:
We formalise the modal operators from the concurrent dynamic logics of Peleg, Nerode and Wijesekera in a multirelational algebraic language based on relation algebra and power allegories, using relational approximation operators on multirelations developed in a companion article. We relate Nerode and Wijesekera's box operator with a relational approximation operator for multirelations and two rela…
▽ More
We formalise the modal operators from the concurrent dynamic logics of Peleg, Nerode and Wijesekera in a multirelational algebraic language based on relation algebra and power allegories, using relational approximation operators on multirelations developed in a companion article. We relate Nerode and Wijesekera's box operator with a relational approximation operator for multirelations and two related operators that approximate multirelations by different kinds of deterministic multirelations. We provide an algebraic soundness proof of Goldblatt's axioms for concurrent dynamic logic as an application.
△ Less
Submitted 14 June, 2023; v1 submitted 18 May, 2023;
originally announced May 2023.
-
Determinism of Multirelations
Authors:
Hitoshi Furusawa,
Walter Guttmann,
Georg Struth
Abstract:
Binary multirelations can model alternating nondeterminism, for instance, in games or nondeterministically evolving systems interacting with an environment. Such systems can show partial or total functional behaviour at both levels of alternation, so that nondeterministic behaviour may occur only at one level or both levels, or not at all. We study classes of inner and outer partial and total func…
▽ More
Binary multirelations can model alternating nondeterminism, for instance, in games or nondeterministically evolving systems interacting with an environment. Such systems can show partial or total functional behaviour at both levels of alternation, so that nondeterministic behaviour may occur only at one level or both levels, or not at all. We study classes of inner and outer partial and total functional multirelations in a multirelational language based on relation algebra and power allegories. While it is known that general multirelations do not form a category, we show that the classes of deterministic multirelations mentioned form categories with respect to Peleg composition from concurrent dynamic logic, and sometimes quantaloids. Some of these are isomorphic to the category of binary relations. We also introduce determinisation maps that approximate multirelations either by binary relations or by deterministic multirelations. Such maps are useful for defining modal operators on multirelations.
△ Less
Submitted 14 June, 2023; v1 submitted 18 May, 2023;
originally announced May 2023.
-
On the Inner Structure of Multirelations
Authors:
Hitoshi Furusawa,
Walter Guttmann,
Georg Struth
Abstract:
Binary multirelations form a model of alternating nondeterminism useful for analysing games, interactions of computing systems with their environments or abstract interpretations of probabilistic programs. We investigate this alternating structure with inner or demonic and outer or angelic choices in a relation-algebraic language extended with specific operations on multirelations that relate to t…
▽ More
Binary multirelations form a model of alternating nondeterminism useful for analysing games, interactions of computing systems with their environments or abstract interpretations of probabilistic programs. We investigate this alternating structure with inner or demonic and outer or angelic choices in a relation-algebraic language extended with specific operations on multirelations that relate to the inner layer of alternation.
△ Less
Submitted 12 June, 2023; v1 submitted 18 May, 2023;
originally announced May 2023.
-
Kleene Theorem for Higher-Dimensional Automata
Authors:
Uli Fahrenberg,
Christian Johansen,
Georg Struth,
Krzysztof Ziemiański
Abstract:
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 preshe…
▽ More
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.
△ Less
Submitted 8 December, 2024; v1 submitted 8 February, 2022;
originally announced February 2022.
-
Posets with Interfaces as a Model for Concurrency
Authors:
Uli Fahrenberg,
Christian Johansen,
Georg Struth,
Krzysztof Ziemiański
Abstract:
We introduce posets with interfaces (iposets) and generalise their standard serial composition to a new gluing composition. In the partial order semantics of concurrency, interfaces and gluing allow modelling events that extend in time and across components. Alternatively, taking a decompositional view, interfaces allow cutting through events, while serial composition may only cut through edges of…
▽ More
We introduce posets with interfaces (iposets) and generalise their standard serial composition to a new gluing composition. In the partial order semantics of concurrency, interfaces and gluing allow modelling events that extend in time and across components. Alternatively, taking a decompositional view, interfaces allow cutting through events, while serial composition may only cut through edges of a poset. We show that iposets under gluing composition form a category, which generalises the monoid of posets under serial composition up to isomorphism. They form a 2-category when a subsumption order and a lax tensor in the form of a non-commutative parallel composition are added, which generalises the interchange monoids used for modelling series-parallel posets. We also study the gluing-parallel hierarchy of iposets, which generalises the standard series-parallel one. The class of gluing-parallel iposets contains that of series-parallel posets and the class of interval orders, which are well studied in concurrency theory, too. We also show that it is strictly contained in the class of all iposets by identifying several forbidden substructures.
△ Less
Submitted 4 November, 2022; v1 submitted 21 June, 2021;
originally announced June 2021.
-
Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs
Authors:
Simon Foster,
Jonathan Julián Huerta y Munive,
Mario Gleirscher,
Georg Struth
Abstract:
We extend a semantic verification framework for hybrid systems with the Isabelle/HOL proof assistant by an algebraic model for hybrid program stores, a shallow expression model for hybrid programs and their correctness specifications, and domain-specific deductive and calculational support. The new store model yields clean separations and dynamic local views of variables, e.g. discrete/continuous,…
▽ More
We extend a semantic verification framework for hybrid systems with the Isabelle/HOL proof assistant by an algebraic model for hybrid program stores, a shallow expression model for hybrid programs and their correctness specifications, and domain-specific deductive and calculational support. The new store model yields clean separations and dynamic local views of variables, e.g. discrete/continuous, mutable/immutable, program/logical, and enhanced ways of manipulating them using combinators, projections and framing. This leads to more local inference rules, procedures and tactics for reasoning with invariant sets, certifying solutions of hybrid specifications or calculating derivatives with increased proof automation and scalability. The new expression model provides more user-friendly syntax, better control of name spaces and interfaces connecting the framework with real-world modelling languages.
△ Less
Submitted 10 June, 2021;
originally announced June 2021.
-
lr-Multisemigroups and Modal Convolution Algebras
Authors:
Uli Fahrenberg,
Christian Johnsen,
Georg Struth,
Krzysztof Ziemiański
Abstract:
We show how modal quantales arise as convolution algebras of functions from lr-multisemigroups that is, multisemigroups with a source map l and a target map r, into modal quantales which can be seen as weight or value algebras. In the tradition of boolean algebras with operators we study modal correspondences between algebraic laws in the three algebras. The class of lr-multisemigroups introduced…
▽ More
We show how modal quantales arise as convolution algebras of functions from lr-multisemigroups that is, multisemigroups with a source map l and a target map r, into modal quantales which can be seen as weight or value algebras. In the tradition of boolean algebras with operators we study modal correspondences between algebraic laws in the three algebras. The class of lr-multisemigroups introduced in this article generalises Schweizer and Sklar's function systems and object-free categories to a setting isomorphic to algebras of ternary relations as used in boolean algebras with operators and in substructural logics. Our results provide a generic construction recipe for weighted modal quantales from such multisemigroups. This is illustrated by many examples, ranging from modal algebras of weighted relations as used in fuzzy mathematics, category quantales in the tradition of category algebras or group rings, incidence algebras over partial orders, discrete and continuous weighted path algebras, weighted languages of pomsets with interfaces, and weighted languages associated with presimplicial and precubical sets. We also discuss how these results can be combined with previous ones for concurrent quantales and generalised to a setting that supports reasoning with stochastic matrices or probabilistic predicate transformers.
△ Less
Submitted 1 May, 2021;
originally announced May 2021.
-
Languages of Higher-Dimensional Automata
Authors:
Uli Fahrenberg,
Christian Johansen,
Georg Struth,
Krzysztof Ziemiański
Abstract:
We introduce languages of higher-dimensional automata (HDAs) and develop some of their properties. To this end, we define a new category of precubical sets, uniquely naturally isomorphic to the standard one, and introduce a notion of event consistency. HDAs are then finite, labeled, event-consistent precubical sets with distinguished subsets of initial and accepting cells. Their languages are sets…
▽ More
We introduce languages of higher-dimensional automata (HDAs) and develop some of their properties. To this end, we define a new category of precubical sets, uniquely naturally isomorphic to the standard one, and introduce a notion of event consistency. HDAs are then finite, labeled, event-consistent precubical sets with distinguished subsets of initial and accepting cells. Their languages are sets of interval orders closed under subsumption; as a major technical step we expose a bijection between interval orders and a subclass of HDAs. We show that any finite subsumption-closed set of interval orders is the language of an HDA, that languages of HDAs are closed under binary unions and parallel composition, and that bisimilarity implies language equivalence.
△ Less
Submitted 3 September, 2021; v1 submitted 12 March, 2021;
originally announced March 2021.
-
Domain Semirings United
Authors:
Uli Fahrenberg,
Christian Johansen,
Georg Struth,
Krzysztof Ziemiánski
Abstract:
Domain operations on semirings have been axiomatised in two different ways: by a map from an additively idempotent semiring into a boolean subalgebra of the semiring bounded by the additive and multiplicative unit of the semiring, or by an endofunction on a semiring that induces a distributive lattice bounded by the two units as its image. This note presents classes of semirings where these approa…
▽ More
Domain operations on semirings have been axiomatised in two different ways: by a map from an additively idempotent semiring into a boolean subalgebra of the semiring bounded by the additive and multiplicative unit of the semiring, or by an endofunction on a semiring that induces a distributive lattice bounded by the two units as its image. This note presents classes of semirings where these approaches coincide.
△ Less
Submitted 22 March, 2021; v1 submitted 9 November, 2020;
originally announced November 2020.
-
Algebraic coherent confluence and higher globular Kleene algebras
Authors:
Cameron Calk,
Eric Goubault,
Philippe Malbos,
Georg Struth
Abstract:
We extend the formalisation of confluence results in Kleene algebras to a formalisation of coherent confluence proofs. For this, we introduce the structure of higher globular Kleene algebra, a higher-dimensional generalisation of modal and concurrent Kleene algebra. We calculate a coherent Church-Rosser theorem and a coherent Newman's lemma in higher Kleene algebras by equational reasoning. We ins…
▽ More
We extend the formalisation of confluence results in Kleene algebras to a formalisation of coherent confluence proofs. For this, we introduce the structure of higher globular Kleene algebra, a higher-dimensional generalisation of modal and concurrent Kleene algebra. We calculate a coherent Church-Rosser theorem and a coherent Newman's lemma in higher Kleene algebras by equational reasoning. We instantiate these results in the context of higher rewriting systems modelled by polygraphs.
△ Less
Submitted 24 November, 2022; v1 submitted 29 June, 2020;
originally announced June 2020.
-
Convolution and Concurrency
Authors:
James Cranch,
Simon Doherty,
Georg Struth
Abstract:
We show how concurrent quantales and concurrent Kleene algebras arise as convolution algebras $Q^X$ of functions from structures $X$ with two ternary relations that satisfy relational interchange laws into concurrent quantales or Kleene algebras $Q$. The elements of $Q$ can be understood as weights; the case $Q=\bool$ corresponds to a powerset lifting. We develop a correspondence theory between re…
▽ More
We show how concurrent quantales and concurrent Kleene algebras arise as convolution algebras $Q^X$ of functions from structures $X$ with two ternary relations that satisfy relational interchange laws into concurrent quantales or Kleene algebras $Q$. The elements of $Q$ can be understood as weights; the case $Q=\bool$ corresponds to a powerset lifting. We develop a correspondence theory between relational properties in $X$ and algebraic properties in $Q$ and $Q^X$ in the sense of modal and substructural logics, and boolean algebras with operators. As examples, we construct the concurrent quantales and Kleene algebras of $Q$-weighted words, digraphs, posets, isomorphism classes of finite digraphs and pomsets.
△ Less
Submitted 6 February, 2020;
originally announced February 2020.
-
Relational Semigroups and Object-Free Categories
Authors:
James Cranch,
Simon Doherty,
Georg Struth
Abstract:
This note relates axioms for partial semigroups and monoids with those for small object-free categories, either with multiple monoidal units or with source and target maps. We discuss the adjunction of a zero element to both kinds of category and provide examples that separate the algebras considered.
This note relates axioms for partial semigroups and monoids with those for small object-free categories, either with multiple monoidal units or with source and target maps. We discuss the adjunction of a zero element to both kinds of category and provide examples that separate the algebras considered.
△ Less
Submitted 31 January, 2020;
originally announced January 2020.
-
Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
Authors:
Simon Foster,
Jonathan Julián Huerta y Munive,
Georg Struth
Abstract:
We present simple new Hoare logics and refinement calculi for hybrid systems in the style of differential dynamic logic. (Refinement) Kleene algebra with tests is used for reasoning about the program structure and generating verification conditions at this level. Lenses capture hybrid program stores in a generic algebraic way. The approach has been formalised with the Isabelle/HOL proof assistant.…
▽ More
We present simple new Hoare logics and refinement calculi for hybrid systems in the style of differential dynamic logic. (Refinement) Kleene algebra with tests is used for reasoning about the program structure and generating verification conditions at this level. Lenses capture hybrid program stores in a generic algebraic way. The approach has been formalised with the Isabelle/HOL proof assistant. A number of examples explains the workflow with the resulting verification components.
△ Less
Submitted 29 October, 2019;
originally announced October 2019.
-
Generating Posets Beyond N
Authors:
Uli Fahrenberg,
Christian Johansen,
Georg Struth,
Ratan Bahadur Thapa
Abstract:
We introduce iposets---posets with interfaces---equipped with a novel gluing composition along interfaces and the standard parallel composition. We study their basic algebraic properties as well as the hierarchy of gluing-parallel posets generated from singletons by finitary applications of the two compositions. We show that not only series-parallel posets, but also interval orders, which seem mor…
▽ More
We introduce iposets---posets with interfaces---equipped with a novel gluing composition along interfaces and the standard parallel composition. We study their basic algebraic properties as well as the hierarchy of gluing-parallel posets generated from singletons by finitary applications of the two compositions. We show that not only series-parallel posets, but also interval orders, which seem more interesting for modelling concurrent and distributed systems, can be generated, but not all posets. Generating posets is also important for constructing free algebras for concurrent semirings and Kleene algebras that allow compositional reasoning about such systems.
△ Less
Submitted 14 October, 2019;
originally announced October 2019.
-
Predicate Transformer Semantics for Hybrid Systems: Verification Components for Isabelle/HOL
Authors:
Jonathan Julián Huerta y Munive,
Georg Struth
Abstract:
We present a semantic framework for the deductive verification of hybrid systems with Isabelle/HOL. It supports reasoning about the temporal evolutions of hybrid programs in the style of differential dynamic logic modelled by flows or invariant sets for vector fields. We introduce the semantic foundations of this framework and summarise their Isabelle formalisation as well as the resulting verific…
▽ More
We present a semantic framework for the deductive verification of hybrid systems with Isabelle/HOL. It supports reasoning about the temporal evolutions of hybrid programs in the style of differential dynamic logic modelled by flows or invariant sets for vector fields. We introduce the semantic foundations of this framework and summarise their Isabelle formalisation as well as the resulting verification components. A series of simple examples shows our approach at work.
△ Less
Submitted 20 September, 2021; v1 submitted 12 September, 2019;
originally announced September 2019.
-
Completeness Theorems for Pomset Languages and Concurrent Kleene Algebras
Authors:
Michael R Laurence,
Georg Struth
Abstract:
Pomsets constitute one of the most basic models of concurrency. A pomset is a generalisation of a word over an alphabet in that letters may be partially ordered. A term $t$ using the bi-Kleene operations $0,1, +, \cdot\, ,^*, \parallel, ^{(*)}$ defines a language $ \mathopen{[\![ } t \mathclose{]\!] } $ of pomsets in a natural way.
We prove that every valid universal equality over pomset languag…
▽ More
Pomsets constitute one of the most basic models of concurrency. A pomset is a generalisation of a word over an alphabet in that letters may be partially ordered. A term $t$ using the bi-Kleene operations $0,1, +, \cdot\, ,^*, \parallel, ^{(*)}$ defines a language $ \mathopen{[\![ } t \mathclose{]\!] } $ of pomsets in a natural way.
We prove that every valid universal equality over pomset languages using these operations is a consequence of the equational theory of regular languages (in which parallel multiplication and iteration are undefined) plus that of the commutative-regular languages (in which sequential multiplication and iteration are undefined). We also show that the class of $\textit{rational}$ pomset languages (that is, those languages generated from singleton pomsets using the bi-Kleene operations) is closed under all Boolean operations.
An $ \textit{ideal}$ of a pomset $p$ is a pomset using the letters of $p$, but having an ordering at least as strict as $p$. A bi-Kleene term $t$ thus defines the set $ \textbf{Id} (\mathopen{[\![ } t \mathclose{]\!] }) $ of ideals of pomsets in $ \mathopen{[\![ } t \mathclose{]\!] } $. We prove that if $t$ does not contain commutative iteration $^{(*)}$ (in our terminology, $t$ is bw-rational) then $\textbf{Id} (\mathopen{[\![ } t \mathclose{]\!] }) \cap \textbf{Pom}_{sp}$, where $ \textbf{Pom}_{sp}$ is the set of pomsets generated from singleton pomsets using sequential and parallel multiplication ($ \cdot$ and $ \parallel$) is defined by a bw-rational term, and if two such terms $t,t'$ define the same ideal language, then $t'=t$ is provable from the Kleene axioms for $0,1, +, \cdot\, ,^*$ plus the commutative idempotent semiring axioms for $0,1, +, \parallel$ plus the exchange law $ (u \parallel v)\cdot ( x \parallel y) \le v \cdot y \parallel u \cdot x $.
△ Less
Submitted 16 May, 2017;
originally announced May 2017.
-
Kleisli, Parikh and Peleg Compositions and Liftings for Multirelations
Authors:
Hitoshi Furusawa,
Yasuo Kawahara,
Georg Struth,
Norihiro Tsumagari
Abstract:
Multirelations provide a semantic domain for computing systems that involve two dual kinds of nondeterminism. This paper presents relational formalisations of Kleisli, Parikh and Peleg compositions and liftings of multirelations. These liftings are similar to those that arise in the Kleisli category of the powerset monad. We show that Kleisli composition of multirelations is associative, but need…
▽ More
Multirelations provide a semantic domain for computing systems that involve two dual kinds of nondeterminism. This paper presents relational formalisations of Kleisli, Parikh and Peleg compositions and liftings of multirelations. These liftings are similar to those that arise in the Kleisli category of the powerset monad. We show that Kleisli composition of multirelations is associative, but need not have units. Parikh composition may neither be associative nor have units, but yields a category on the subclass of up-closed multirelations. Finally, Peleg composition has units, but need not be associative; a category is obtained when multirelations are union-closed.
△ Less
Submitted 16 May, 2017;
originally announced May 2017.
-
Convolution Algebras: Relational Convolution, Generalised Modalities and Incidence Algebras
Authors:
Brijesh Dongol,
Ian J. Hayes,
Georg Struth
Abstract:
Convolution is a ubiquitous operation in mathematics and computing. The Kripke semantics for substructural and interval logics motivates its study for quantale-valued functions relative to ternary relations. The resulting notion of relational convolution leads to generalised binary and unary modal operators for qualitative and quantitative models, and to more conventional variants, when ternary re…
▽ More
Convolution is a ubiquitous operation in mathematics and computing. The Kripke semantics for substructural and interval logics motivates its study for quantale-valued functions relative to ternary relations. The resulting notion of relational convolution leads to generalised binary and unary modal operators for qualitative and quantitative models, and to more conventional variants, when ternary relations arise from identities over partial semigroups. Convolution-based semantics for fragments of categorial, linear and incidence (segment or interval) logics are provided as qualitative applications. Quantitative examples include algebras of durations and mean values in the duration calculus.
△ Less
Submitted 8 February, 2021; v1 submitted 15 February, 2017;
originally announced February 2017.
-
On the Expressive Power of Kleene Algebra with Domain
Authors:
Georg Struth
Abstract:
It is shown that antidomain semirings are more expressive than test semirings and that Kleene algebras with domain are more expressive than Kleene algebras with tests. It is also shown that Kleene algebras with domain are expressive for propositional Hoare logic whereas Kleene algebras with tests are not.
It is shown that antidomain semirings are more expressive than test semirings and that Kleene algebras with domain are more expressive than Kleene algebras with tests. It is also shown that Kleene algebras with domain are expressive for propositional Hoare logic whereas Kleene algebras with tests are not.
△ Less
Submitted 2 August, 2015; v1 submitted 26 July, 2015;
originally announced July 2015.
-
Taming Multirelations
Authors:
Hitoshi Furusawa,
Georg Struth
Abstract:
Binary multirelations generalise binary relations by associating elements of a set to its subsets. We study the structure and algebra of multirelations under the operations of union, intersection, sequential and parallel composition, as well as finite and infinite iteration. Starting from a set-theoretic investigation, we propose axiom systems for multirelations in contexts ranging from bi-monoids…
▽ More
Binary multirelations generalise binary relations by associating elements of a set to its subsets. We study the structure and algebra of multirelations under the operations of union, intersection, sequential and parallel composition, as well as finite and infinite iteration. Starting from a set-theoretic investigation, we propose axiom systems for multirelations in contexts ranging from bi-monoids to bi-quantales.
△ Less
Submitted 13 June, 2015; v1 submitted 21 January, 2015;
originally announced January 2015.
-
Principles for Verification Tools: Separation Logic
Authors:
Brijesh Dongol,
Victor B. F. Gomes,
Georg Struth
Abstract:
A principled approach to the design of program verification and con- struction tools is applied to separation logic. The control flow is modelled by power series with convolution as separating conjunction. A generic construction lifts resource monoids to assertion and predicate transformer quantales. The data flow is captured by concrete store/heap models. These are linked to the separation algebr…
▽ More
A principled approach to the design of program verification and con- struction tools is applied to separation logic. The control flow is modelled by power series with convolution as separating conjunction. A generic construction lifts resource monoids to assertion and predicate transformer quantales. The data flow is captured by concrete store/heap models. These are linked to the separation algebra by soundness proofs. Verification conditions and transformation laws are derived by equational reasoning within the predicate transformer quantale. This separation of concerns makes an implementation in the Isabelle/HOL proof as- sistant simple and highly automatic. The resulting tool is correct by construction; it is explained on the classical linked list reversal example.
△ Less
Submitted 16 October, 2014;
originally announced October 2014.
-
Convolution, Separation and Concurrency
Authors:
Brijesh Dongol,
Ian J. Hayes,
Georg Struth
Abstract:
A notion of convolution is presented in the context of formal power series together with lifting constructions characterising algebras of such series, which usually are quantales. A number of examples underpin the universality of these constructions, the most prominent ones being separation logics, where convolution is separating conjunction in an assertion quantale; interval logics, where convolu…
▽ More
A notion of convolution is presented in the context of formal power series together with lifting constructions characterising algebras of such series, which usually are quantales. A number of examples underpin the universality of these constructions, the most prominent ones being separation logics, where convolution is separating conjunction in an assertion quantale; interval logics, where convolution is the chop operation; and stream interval functions, where convolution is used for analysing the trajectories of dynamical or real-time systems. A Hoare logic is constructed in a generic fashion on the power series quantale, which applies to each of these examples. In many cases, commutative notions of convolution have natural interpretations as concurrency operations.
△ Less
Submitted 15 October, 2014;
originally announced October 2014.
-
Probabilistic Rely-guarantee Calculus
Authors:
Annabelle McIver,
Tahiry Rabehaja,
Georg Struth
Abstract:
Jones' rely-guarantee calculus for shared variable concurrency is extended to include probabilistic behaviours. We use an algebraic approach which combines and adapts probabilistic Kleene algebras with concurrent Kleene algebra. Soundness of the algebra is shown relative to a general probabilistic event structure semantics. The main contribution of this paper is a collection of rely-guarantee rule…
▽ More
Jones' rely-guarantee calculus for shared variable concurrency is extended to include probabilistic behaviours. We use an algebraic approach which combines and adapts probabilistic Kleene algebras with concurrent Kleene algebra. Soundness of the algebra is shown relative to a general probabilistic event structure semantics. The main contribution of this paper is a collection of rely-guarantee rules built on top of that semantics. In particular, we show how to obtain bounds on probabilities by deriving rely-guarantee rules within the true-concurrent denotational semantics. The use of these rules is illustrated by a detailed verification of a simple probabilistic concurrent program: a faulty Eratosthenes sieve.
△ Less
Submitted 2 June, 2015; v1 submitted 1 September, 2014;
originally announced September 2014.
-
Concurrent Dynamic Algebra
Authors:
Hitoshi Furusawa,
Georg Struth
Abstract:
We reconstruct Peleg's concurrent dynamic logic in the context of modal Kleene algebras. We explore the algebraic structure of its multirelational semantics and develop an abstract axiomatisation of concurrent dynamic algebras from that basis. In this axiomatisation, sequential composition is not associative. It interacts with concurrent composition through a weak distributivity law. The modal ope…
▽ More
We reconstruct Peleg's concurrent dynamic logic in the context of modal Kleene algebras. We explore the algebraic structure of its multirelational semantics and develop an abstract axiomatisation of concurrent dynamic algebras from that basis. In this axiomatisation, sequential composition is not associative. It interacts with concurrent composition through a weak distributivity law. The modal operators of concurrent dynamic algebra are obtained from abstract axioms for domain and antidomain operators; the Kleene star is modelled as a least fixpoint. Algebraic variants of Peleg's axioms are shown to be valid in these algebras and their soundness is proved relative to the multirelational model. Additional results include iteration principles for the Kleene star and a refutation of variants of Segerberg's axiom in the multirelational setting. The most important results have been verified formally with Isabelle/HOL.
△ Less
Submitted 22 July, 2014;
originally announced July 2014.
-
Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools
Authors:
Alasdair Armstrong,
Victor B. F. Gomes,
Georg Struth
Abstract:
We provide simple equational principles for deriving rely-guarantee-style inference rules and refinement laws based on idempotent semirings. We link the algebraic layer with concrete models of programs based on languages and execution traces. We have implemented the approach in Isabelle/HOL as a lightweight concurrency verification tool that supports reasoning about the control and data flow of co…
▽ More
We provide simple equational principles for deriving rely-guarantee-style inference rules and refinement laws based on idempotent semirings. We link the algebraic layer with concrete models of programs based on languages and execution traces. We have implemented the approach in Isabelle/HOL as a lightweight concurrency verification tool that supports reasoning about the control and data flow of concurrent programs with shared variables at different levels of abstraction. This is illustrated on two simple verification examples.
△ Less
Submitted 4 December, 2013;
originally announced December 2013.
-
An Event Structure Model for Probabilistic Concurrent Kleene Algebra
Authors:
Annabelle McIver,
Tahiry Rabehaja,
Georg Struth
Abstract:
We give a new true-concurrent model for probabilistic concurrent Kleene algebra. The model is based on probabilistic event structures, which combines ideas from Katoen's work on probabilistic concurrency and Varacca's probabilistic prime event structures. The event structures are compared with a true-concurrent version of Segala's probabilistic simulation. Finally, the algebraic properties of the…
▽ More
We give a new true-concurrent model for probabilistic concurrent Kleene algebra. The model is based on probabilistic event structures, which combines ideas from Katoen's work on probabilistic concurrency and Varacca's probabilistic prime event structures. The event structures are compared with a true-concurrent version of Segala's probabilistic simulation. Finally, the algebraic properties of the model are summarised to the extent that they can be used to derive techniques such as probabilistic rely/guarantee inference rules.
△ Less
Submitted 8 October, 2013;
originally announced October 2013.
-
Probabilistic Concurrent Kleene Algebra
Authors:
Annabelle McIver,
Tahiry Rabehaja,
Georg Struth
Abstract:
We provide an extension of concurrent Kleene algebras to account for probabilistic properties. The algebra yields a unified framework containing nondeterminism, concurrency and probability and is sound with respect to the set of probabilistic automata modulo probabilistic simulation. We use the resulting algebra to generalise the algebraic formulation of a variant of Jones' rely/guarantee calculus…
▽ More
We provide an extension of concurrent Kleene algebras to account for probabilistic properties. The algebra yields a unified framework containing nondeterminism, concurrency and probability and is sound with respect to the set of probabilistic automata modulo probabilistic simulation. We use the resulting algebra to generalise the algebraic formulation of a variant of Jones' rely/guarantee calculus.
△ Less
Submitted 11 June, 2013;
originally announced June 2013.
-
Weak Concurrent Kleene Algebra with Application to Algebraic Verification
Authors:
Annabelle McIver,
Tahiry Rabehaja,
Georg Struth
Abstract:
We propose a generalisation of concurrent Kleene algebra \cite{Hoa09} that can take account of probabilistic effects in the presence of concurrency. The algebra is proved sound with respect to a model of automata modulo a variant of rooted $η$-simulation equivalence. Applicability is demonstrated by algebraic treatments of two examples: algebraic may testing and Rabin's solution to the choice coor…
▽ More
We propose a generalisation of concurrent Kleene algebra \cite{Hoa09} that can take account of probabilistic effects in the presence of concurrency. The algebra is proved sound with respect to a model of automata modulo a variant of rooted $η$-simulation equivalence. Applicability is demonstrated by algebraic treatments of two examples: algebraic may testing and Rabin's solution to the choice coordination problem.
△ Less
Submitted 30 January, 2013;
originally announced January 2013.
-
Dependently Typed Programming based on Automated Theorem Proving
Authors:
Alasdair Armstrong,
Simon Foster,
Georg Struth
Abstract:
Mella is a minimalistic dependently typed programming language and interactive theorem prover implemented in Haskell. Its main purpose is to investigate the effective integration of automated theorem provers in a pure and simple setting. Such integrations are essential for supporting program development in dependently typed languages. We integrate the equational theorem prover Waldmeister and test…
▽ More
Mella is a minimalistic dependently typed programming language and interactive theorem prover implemented in Haskell. Its main purpose is to investigate the effective integration of automated theorem provers in a pure and simple setting. Such integrations are essential for supporting program development in dependently typed languages. We integrate the equational theorem prover Waldmeister and test it on more than 800 proof goals from the TPTP library. In contrast to previous approaches, the reconstruction of Waldmeister proofs within Mella is quite robust and does not generate a significant overhead to proof search. Mella thus yields a template for integrating more expressive theorem provers in more sophisticated languages.
△ Less
Submitted 16 December, 2011;
originally announced December 2011.
-
Kleene algebra with domain
Authors:
J. Desharnais,
B. Möller,
G. Struth
Abstract:
We propose Kleene algebra with domain (KAD), an extension of Kleene algebra with two equational axioms for a domain and a codomain operation, respectively. KAD considerably augments the expressiveness of Kleene algebra, in particular for the specification and analysis of state transition systems. We develop the basic calculus, discuss some related theories and present the most important models o…
▽ More
We propose Kleene algebra with domain (KAD), an extension of Kleene algebra with two equational axioms for a domain and a codomain operation, respectively. KAD considerably augments the expressiveness of Kleene algebra, in particular for the specification and analysis of state transition systems. We develop the basic calculus, discuss some related theories and present the most important models of KAD. We demonstrate applicability by two examples: First, an algebraic reconstruction of Noethericity and well-foundedness; second, an algebraic reconstruction of propositional Hoare logic.
△ Less
Submitted 28 October, 2003;
originally announced October 2003.
