Relations and Kleene Algebra in Computer Science

Frontmatter

Knowledge and Structure in Social Algorithms

Abstract

While contemporary Game Theory has concentrated much on strategy, there is somewhat less attention paid to the role of knowledge and information transfer. There are exceptions to this rule of course, especially starting with the work of Aumann [2], and with contributions made by ourselves with coauthors Cogan, Krasucki and Pacuit [17,13]. But we have still only scratched the surface and there is still a lot more that can be done. In this paper we point to the important role which knowledge plays in social procedures (colorfully called Social Software [15]).

Rohit Parikh

Computational Social Choice Using Relation Algebra and RelView

Abstract

We present an overview of the potential of relation algebra and the software tool RelView, based on it, to compute solutions for problems from social choice. Using one leading example throughout the text, we subsequently show how the RelView  tool may be used to compute and visualize minimal winning coalitions, swingers of a given coalition, vulnerable winning coalitions, central players, dominant players, Banzhaf power indices of the different players, Hoede Bakker indices of the different players in a network, and finally stable coalitions/governments. Although problems from social choice and games are mostly exponential, due to the BDD implementation of RelView, computations are feasible for the examples which appear in practice.

Harrie de Swart, Rudolf Berghammer, Agnieszka Rusinowska

A Model of Internet Routing Using Semi-modules

Abstract

Current Internet routing protocols exhibit several types of anomalies that can reduce network reliability. In order to design more robust protocols we need better formal models to capture the complexities of Internet routing. In this paper we develop an algebraic model that clarifies the distinction between routing tables and forwarding tables. We hope that this suggests new approaches to the design of routing protocols.

John N. Billings, Timothy G. Griffin

Visibly Pushdown Kleene Algebra and Its Use in Interprocedural Analysis of (Mutually) Recursive Programs

Abstract

Kleene algebra is a great formalism for doing intraprocedural analysis and verification of programs, but it seems difficult to deal with interprocedural analysis where the power of context-free languages is often needed to represent both the program and the property. In the model checking framework, Alur and Madhusudan defined visibly pushdown automata, which accept a subclass of context-free languages called visibly pushdown languages, to do some interprocedural analyses of programs while remaining decidable. We present visibly pushdown Kleene algebra, an extension of Kleene algebra that axiomatises exactly the equational theory of visibly pushdown languages. The algebra is simply Kleene algebra along with a family of implicit least fixed point operators. Some interprocedural analyses of (mutually) recursive programs are possible in this formalism and it can deal with some non-regular properties.

Claude Bolduc, Béchir Ktari

Towards Algebraic Separation Logic

Abstract

We present an algebraic approach to separation logic. In particular, we give algebraic characterisations for all constructs of separation logic. The algebraic view does not only yield new insights on separation logic but also shortens proofs and enables the use of automated theorem provers for verifying properties at a more abstract level.

Han-Hing Dang, Peter Höfner, Bernhard Möller

Domain and Antidomain Semigroups

Abstract

We axiomatise and study operations for relational domain and antidomain on semigroups and monoids. We relate this approach with previous axiomatisations for semirings, partial transformation semigroups and dynamic predicate logic.

Jules Desharnais, Peter Jipsen, Georg Struth

Composing Partially Ordered Monads

Abstract

Composition of the many-valued powerset partially ordered monad with the term monad provides extensions to non-classical relations and also new examples for Kleene algebras.

Patrik Eklund, Robert Helgesson

A Relation-Algebraic Approach to Liveness of Place/Transition Nets

Abstract

We provide a relation-algebraic characterization of liveness in Petri nets based on a relation-algebraic definition of both the structure and the state space of Petri nets. Such an approach, compared to the common ones that apply predicate logic and set theory, shifts the formalization to a more abstract level. As a main benefit, Petri net properties can be proved in a rigorous mathematical style. Since the characterizations are executable relational specifications, they provide the possibility for tool support.

Alexander Fronk, Rudolf Berghammer

∗-Continuous Idempotent Left Semirings and Their Ideal Completion

Abstract

In this paper, we introduce two notions of continuity for idempotent left semirings, which are called ∗-continuity and D-continuity. Also, for a ∗-continuous idempotent left semiring, we introduce a notion of ∗-ideals. Then, we show that the set of ∗-ideals of a ∗-continuous idempotent left semiring forms a D-continuous idempotent left semiring and the construction satisfies a universal property.

Hitoshi Furusawa, Fumiya Sanda

A Semiring Approach to Equivalences, Bisimulations and Control

Abstract

Equivalences, partitions and (bi)simulations are usually tackled using concrete relations. There are only few treatments by abstract relation algebra or category theory. We give an approach based on the theory of semirings and quantales. This allows applying the results directly to structures such as path and tree algebras which is not as straightforward in the other approaches mentioned. Also, the amount of higher-order formulations used is low and only a one-sorted algebra is used. This makes the theory suitable for fully automated first-order proof systems. As a small application we show how to use the algebra to construct a simple control policy for infinite-state transition systems.

Roland Glück, Bernhard Möller, Michel Sintzoff

General Correctness Algebra

Abstract

General correctness offers a finer semantics of programs than partial and total correctness. We give an algebraic account continuing and extending previous approaches. In particular, we propose axioms, correctness statements, a correctness calculus, specification constructs and a loop refinement rule. The Egli-Milner order is treated algebraically and we show how to obtain least fixpoints, used to solve recursion equations, in terms of the natural order.

Walter Guttmann

Foundations of Concurrent Kleene Algebra

Abstract

A Concurrent Kleene Algebra offers two composition operators, one that stands for sequential execution and the other for concurrent execution [10]. In this paper we investigate the abstract background of this law in terms of independence relations on which a concrete trace model of the algebra is based. Moreover, we show the interdependence of the basic properties of such relations and two further laws that are essential in the application of the algebra to a Jones style rely/guarantee calculus. Finally we reconstruct the trace model in a more abstract setting based on the notion of atoms from lattice theory.

C. A. R. Hoare, Bernhard Möller, Georg Struth, Ian Wehrman

Armstrong’s Inference Rules in Dedekind Categories

Abstract

It is well-known that Armstrong’s inference rules are sound and complete for functional dependencies of relational data bases and for implication in the theory of formal concepts by Wille and Ganter. In this paper the authors treat Armstrong’s inference rules and the implication as (binary) relations in an upper semi lattice in a Dedekind category, and give a relation algebraic proof of the completeness theorem for Armstrong’s inference rules in a Schröder category.

Toshikazu Ishida, Kazumasa Honda, Yasuo Kawahara

Data Mining, Reasoning and Incremental Information Retrieval through Non Enlargeable Rectangular Relation Coverage

Abstract

Association rules extraction from a binary relation as well as reasoning and information retrieval are generally based on the initial representation of the binary relation as an adjacency matrix. This presents some inconvenience in terms of space memory and knowledge organization. A coverage of a binary relation by a minimal number of non enlargeable rectangles generally reduces memory space consumption without any loss of information. It also has the advantage of organizing objects and attributes contained in the binary relation into a conceptual representation. In this paper, we propose new algorithms to extract association rules (i.e. data mining), conclusions from initial attributes (i.e. reasoning), as well as retrieving the total objects satisfying some initial attributes, by using only the minimal coverage. Finally we propose an incremental approximate algorithm to update a binary relation organized as a set of non enlargeable rectangles. Two main operations are mostly used during the organization process: First, separation of existing rectangles when we delete some pairs. Second, join of rectangles when common properties are discovered, after addition or removal of elements from a binary context. The objective is the minimization of the number of rectangles and the maximization of their structure. The article also raises the problems of equational modeling of the minimization criteria, as well as incrementally providing equations to maintain them.

Ali Jaoua, Rehab Duwairi, Samir Elloumi, Sadok Ben Yahia

Collagories for Relational Adhesive Rewriting

Abstract

We define collagories essentially as “distributive allegories without zero morphisms”, and show that they are sufficient for accommodating the relation-algebraic approach to graph transformation. Collagories closely correspond to the adhesive categories important for the categorical DPO approach to graph transformation. but thanks to their relation-algebraic flavour provide a more accessible and more flexible setting.

Wolfram Kahl

Cardinal Addition in Distributive Allegories

Abstract

In this paper we want to extend the abstract approach to the size of a relation based on a cardinality function. Assuming suitable extra structure on the underlying distributive allegory we are going to define addition on cardinalities and investigate its basic properties.

Yasuo Kawahara, Michael Winter

Relational Methods in the Analysis of While Loops: Observations of Versatility

Abstract

Despite much progress in the design of programming languages, the vast majority of software being written and deployed nowadays remains written in languages where iteration is the main inductive construct, and the main source of algorithmic complexity. For the past four decades, the analysis of iterative constructs has been dominated, not undeservedly, by the concept of invariant assertions. In this paper we submit relation-based alternatives, namely invariant relations and invariant functions, and show how these can provide complementary perspectives, and can enrich the analysis of iterations. Whereas loop invariants can be used to establish the correctness of iterative programs in Hoare logics, invariant relations and invariant functions are used to derive program functions in Mills’ logic. In keeping with the conference format, we do not delve too much into theoretical results, and focus instead on the applied aspects of our relation-theoretic approach.

Asma Louhichi, Olfa Mraihi, Lamia Labed Jilani, Khaled Bsaies, Ali Mili

Modalities, Relations, and Learning

A Relational Interpretation of Learning Approaches

Abstract

While the popularity of statistical, probabilistic and exhaustive machine learning techniques still increases, relational and logic approaches are still a niche market in research. While the former approaches focus on predictive accuracy, the latter ones prove to be indispensable in knowledge discovery.

In this paper we present a relational description of machine learning problems. We demonstrate how common ensemble learning methods as used in classifier learning can be reformulated in a relational setting. It is shown that multimodal logics and relational data analysis with rough sets are closely related. Finally, we give an interpretation of logic programs as approximations of hypotheses.

It is demonstrated that at a certain level of abstraction all these methods unify into one and the same formalisation which nicely connects to multimodal operators.

Martin Eric Müller

The Cube of Kleene Algebras and the Triangular Prism of Multirelations

Abstract

We refine and extend the known results that the set of ordinary binary relations forms a Kleene algebra, the set of up-closed multirelations forms a lazy Kleene algebra, the set of up-closed finite multirelations forms a monodic tree Kleene algebra, and the set of total up-closed finite multirelations forms a probabilistic Kleene algebra. For the refinement, we introduce a notion of type of multirelations. For each of eight classes of relaxation of Kleene algebra, we give a sufficient condition on type T so that the set of up-closed multirelations of T belongs to the class. Some of the conditions are not only sufficient, but also necessary.

Koki Nishizawa, Norihiro Tsumagari, Hitoshi Furusawa

Discrete Duality for Relation Algebras and Cylindric Algebras

Abstract

Following the representation theorems for relation algebras and cylindric algebras presented in [5] and [7] we develop discrete duality for relation algebras and relation frames, and for cylindric algebras and cylindric frames.

Ewa Orłowska, Ingrid Rewitzky

Contact Relations with Applications

Abstract

Using relation algebra, we generalize Aumann’s notion of a contact relation and that of a closure operation from powersets to general membership relations and their induced partial orders. We also investigate the relationship between contacts and closures in this general setting and use contacts to establish a one-to-one correspondence between the column space and the row space of a relation.

Gunther Schmidt, Rudolf Berghammer

A While Program Normal Form Theorem in Total Correctness

Abstract

A classical while-program normal-form theorem is derived in demonic refinement algebra. In contrast to Kozen’s partial-correctness proof of the theorem in Kleene algebra with tests, the derivation in demonic refinement algebra provides a proof that the theorem holds in total correctness.

Kim Solin

Complements in Distributive Allegories

Abstract

It is known in topos theory that the axiom of choice implies that the topos is Boolean. In this paper we want to prove and generalize this result in the context of allegories. In particular, we will show that partial identities do have complements in distributive allegories with relational sums and total splittings assuming the axiom of choice. Furthermore, we will discuss possible modifications of the assumptions used in that theorem.

Michael Winter

On the Skeleton of Stonian p-Ortholattices

Abstract

Boolean Contact Algebras (BCA) establish the algebraic counterpart of the mereotopolopy induced by the Region Connection Calculus (RCC). Similarly, Stonian p-ortholattices serve as a lattice theoretic version of the ontology RT ⁻ of Asher and Vieu. In this paper we study the relationship between BCAs and Stonian p-ortholattices. We show that the skeleton of every Stonian p-ortholattice is a BCA, and, conversely, that every BCA is isomorphic to the skeleton of a Stonian p-ortholattice. Furthermore, we prove the equivalence between algebraic conditions on Stonian p-ortholattices and the axioms C5, C6, and C7 for BCAs.

Michael Winter, Torsten Hahmann, Michael Gruninger

Backmatter