Recent Papers

D. Kozen, B. Möller: Separability in Domain Semirings.
Institut für Informatik, Universität Augsburg, Report 2004-16

First, we show with two examples that in test semirings with an incomplete test algebra a domain operation may or may not exist. Second, we show that two notions of separability in test semirings coincide, respectively, with locality of composition and with extensionality of the diamond operators in domain semirings. We conclude with a brief comparison of dynamic algebras and modal Kleene algebras.

J. Desharnais, B. Möller, F. Tchier: Kleene under a Modal Demonic star.
Institut für Informatik, Universität Augsburg, Report 2004-11. Revised version to appear in Journal of Logic and Algebraic Programming

In relational semantics, the input-output semantics of a program is a relation on its set of states. We generalize this in considering elements of Kleene algebras as semantical values. In a nondeterministic context, the demonic semantics is calculated by considering the worst behavior of the program. In this paper, we concentrate on while loops. Calculating the semantics of a loop is difficult, but showing the correctness of any candidate abstraction is much easier. For deterministic programs, Mills has described a checking method known as the while statement verification rule. A corresponding programming theorem for nondeterministic iterative constructs is proposed, proved and applied to an example. This theorem can be considered as a generalization of the while statement erification rule to nondeterministic loops. The paper generalizes earlier relation-algebraic work to the setting of modal Kleene algebra, an extension of Kozen's Kleene algebra with tests that allows the internalization of weakest liberal precondition and strongest liberal postcondition operators.

J. Desharnais, B. Möller, G. Struth: Modal Kleene algebra and applications - a survey.
Journal on Relational Methods in Computer Science 1, 93-131 (2004)

Modal Kleene algebras are Kleene algebras with forward and backward modal operators defined via domain and codomain operations. They provide a concise and convenient algebraic framework that subsumes various other calculi and allows treating quite a variety of areas. We survey the basic theory and some prominent applications. These include, on the system semantics side, Hoare logic and PDL (Propositional Dynamic Logic), wp calculus and predicate transformer semantics, temporal logics and termination analysis of rewrite and state transition systems. On the derivation side we apply the framework to game analysis and greedy-like algorithms.

J. Desharnais, B. Möller, G. Struth: Termination in Modal Kleene Algebra.
Institut für Informatik, Universität Augsburg, Report 2004-04. Revised version in J.-J. Lévy, E. Mayr, J. Mitchell (eds.): Exploring new frontiers of theoretical informatics. IFIP International Federation for Information Processing Series 155. Kluwer 2004, 653-666

Modal Kleene algebras are Kleene algebras with forward and backward modal operators defined via domain and codomain operations. The paper investigates the algebraic structure of modal operators. It studies and compares different notions of termination in this class, including an algebraic correspondence proof of Löb's formula from modal logic. It gives calculational proofs of two fundamental statements from rewriting theory that involve termination: Bachmair's and Dershowitz's well-founded union theorem and Newman's lemma. These results are also of general interest for the termination analysis of programs and state transition systems.

B. Möller: Lazy Kleene Algebra
Institut für Informatik, Universität Augsburg, Report 2003-17. Revised version in D. Kozen (ed.): Mathematics of Program Construction. LNCS 3125. Springer 2004, 252--273

We propose a relaxation of Kleene algebra by giving up strictness and right-distributivity of composition. This allows the subsumption of Dijkstra's computation calculus, Cohen's omega algebra and von Wright's demonic refinement algebra. Moreover, by adding domain and codomain operators we can also incorporate modal operators. Finally, it is shown that the predicate transformers form lazy Kleene algebras again, the disjunctive and conjunctive ones even lazy Kleene algebras with an omega operation.

B. Möller, G. Struth: Greedy-Like Algorithms in Kleene Algebra.
Institut für Informatik, Universität Augsburg, Report 2003-11. Revised version to appear in R. Berghammer, B. Möller, and G. Struth (eds.), Relational and Kleene-Algebraic Methods in Computer Science, LNCS 3051. Springer 2004, 202-214

This paper provides an algebraic background for the formal derivation of greedy-like algorithms. Such derivations have previously been done in various frameworks including relation algebra. We propose Kleene algebra as a particularly simple alternative. Instead of converse and residuation we use modal operators that are definable in a wide class of algebras, based on domain/codomain or image/pre-image operations. By abstracting from earlier approaches we arrive at a very general theorem about the correctness of loops that covers particular forms of greedy algorithms as special cases.

T. Ehm, B. Möller, G. Struth: Kleene Modules.
Institut für Informatik, Universität Augsburg, Report 2003-10. Revised version to appear in R. Berghammer, B. Möller, and G. Struth (eds.), Relational and Kleene-Algebraic Methods in Computer Science, LNCS 3051. Springer 2004, 112-123

We propose axioms for Kleene modules (KM). These structures have a Kleene algebra K and a Boolean algebra B as sorts. The scalar products are mappings from K and B to B; they arise as algebraic abstractions of relational image and preimage operations. KM is the basis of algebraic variants of dynamic logics. We develop a calculus for KM and discuss its relation to Kleene algebra with domain and to dynamic and test algebras. As an example, we apply KM to the reachability analysis in directed graphs.

B. Möller, G. Struth: Modal Kleene Algebra and Partial Correctness.
Institut für Informatik, Universität Augsburg, Report 2003-08. Revised version in C. Rattray, S. Maharaj, C. Shankland (eds.): Algebraic Methodology and Software Technology. LNCS 3116. Springer 2004, 379-393 (Best Paper Award)

We enrich Kleene algebra by domain and codomain operators. These abstractions of relational notions give rise to four modal operators. The boxes and diamonds enjoy various symmetries via Galois connections and dualities. Lifting modal statements to modal operator semirings yields a further abstraction and thus a more elegant and concise ``statefree'' reasoning about modalities. We use this modal Kleene algebra for calculating soundness and completeness proofs for propositional Hoare logic. While our soundness proof is more direct than related ones, our algebraic completeness proof seems entirely novel. It uses a modal symmetry that relates the wlp predicate transformer with partial correctness assertions and that is beyond the expressibility of formalisms like propositional dynamic logic.

J. Desharnais, B. Möller, G. Struth: Kleene Algebra With Domain.
Revised version to appear in ACM Transactions on Computational Logic. Previous version: Institut für Informatik, Universität Augsburg, Report 2003-7.

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 expressibility 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.

J. Desharnais, B. Möller: Least reflexive points of relations.
Institut für Informatik, Universität Augsburg, Report 2000-5. Revised version to appear in Higher Order and Symbolic Computation.

Assume a partially ordered set (S,<=) and a relation R on S. We consider various sets of conditions in order to determine whether they ensure the existence of a least reflexive point, that is, a least x such that xRx. This is a generalization of the problem of determining the least fixed point of a function and the conditions under which it exists. To motivate the investigation we first present a theorem by Cai and Paige giving conditions under which iterating R from the bottom element necessarily leads to a minimal reflexive point; the proof is by a concise relation-algebraic calculation. Then, we assume a complete lattice and exhibit sufficient conditions, depending on whether R is partial or not, for the existence of a least reflexive point. Further results concern the structure of the set of all reflexive points; among other results we give a sufficient condition that these form a complete lattice, thus generalizing Tarski's classical result to the nondeterministic case.

J. Desharnais, B. Möller: Characterizing determinacy in Kleene algebras.
Institut für Informatik, Universität Augsburg, Report 2000-5. Revised version in Information Sciences - An international Journal 139, 253-273 (2001).

Elements of Kleene algebras can be used, among others, as abstractions of the input-output semantics of nondeterministic programs or as models for the association of pointers with their target objects. In the first case, one seeks to distinguish the subclass of elements that correspond to deterministic programs. In the second case one is only interested in functional correspondences, since it does not make sense for a pointer to point to two different objects. We discuss several candidate notions of determinacy and clarify their relationship. Some characterizations that are equivalent in the case where the underlying Kleene algebra is an (abstract) relation algebra are not equivalent for general Kleene algebras.

B. Möller: Safer ways to pointer manipulation.
Institut für Informatik, Universität Augsburg, Report 2000-4.

We present a technique for passing in a safe way from high-level specifications of algorithms on pointer structures in a semi-functional style to efficient low-level implementations involving address calculations.

J. Desharnais, B. Möller, F. Tchier: Kleene under a demonic star.
Institut für Informatik, Universität Augsburg, Report 2000-3. Revised version in: T. Rus (ed.): Algebraic Methodology and Software Technology. Lecture Notes in Computer Sciecne 1816. Berlin: Springer 2000, 355-370.

In relational semantics, the input-output semantics of a program is a relation on its set of states. We generalize this in considering elements of Kleene algebras as semantical values. In a nondeterministic context, the demonic semantics is calculated by considering the worst behavior of the program. In this paper, we concentrate on while loops. Calculating the semantics of a loop is difficult, but showing the correctness of any candidate abstraction is much easier. For deterministic programs, Mills has described a checking method known as the while statement verification rule. A corresponding programming theorem for nondeterministic iterative constructs is proposed, proved and applied to an example. This theorem can be considered as a generalization of the while statement verification rule to nondeterministic loops.

B. Möller: Calculating with acyclic and cyclic lists.
Information Sciences - An International Journal. Special Issue on Relational Methods in Computer Science 119/3-4, 135-154 (1999)

We use a relational model of pointer structures to calculate a number of standard algorithms on singly linked lists, both acyclic and cyclic. This shows that our techniques are not just useful for tree-like structures, but apply to general pointer structures as well.

B. Möller: Typed Kleene algebras.
Institut für Informatik, Universität Augsburg, Report 1999-8

Kleene algebras provide a convenient and powerful algebraic axiomatisation of a complete lattice that is endowed with a sequential composition operation. Models include formal languages under concatenation, relations under standard composition, sets of graph paths under path concatenation and sets of streams under concatenation. The least and greatest fixpoint operators of a complete lattice allow definitions of the finite and infinite iteration operators * and omega-iteration, resp. The abstract setting of Kleene algebras was used by Brunn/Möller/Russling (LNCS 1422) for the schematic derivation of a class of algorithms that abstracts layer-oriented graph traversals such as breadth-first search. It was also shown that the standard efficiency improvement for such algorithms, viz. carrying along a set of already visited vertices, can completely be transferred to the abstract level. The set of already visited vertices is used to restrict the underlying graph appropriately. So we need abstract counterparts of the notions of (sub)sets and restriction. The former role is taken over by elements of the Kleene algebra that are called types, whereas restriction can be modeled, as in the case of relations, by composition with a type.

B. Möller: Algebraic structures for program calculation.
In: M. Broy, R. Steinbrüggen (eds.): Calculational system design. International Summer School Marktoberdorf, July 28 - August 9, 1998. NATO Advanced Science Institutes Series. Subseries F: Computer and Systems Sciences. Amsterdam: IOS Press 1999, 25-97

In calculational program design one derives implementations from specifications using semantics-preserving deduction rules. The aim of modern algebraic approaches is to make both specification and calculation more concise and perspicuous by compacting logic into algebra as much as possible. We present a collection of algebraic calculi that are useful in this activity. They are shown at work in a number of examples that range from graph algorithms over stream processing to hardware description.

B. Möller, J.V. Tucker (eds.): Prospects for hardware foundations.
Lecture Notes in Computer Science 1546. Berlin: Springer 1998

This volume is devoted to the theoretical foundations of hardware design. The 12  chapters presented are organized in sections on mathematical foundations of hardware modelling; models of hardware and dynamical systems; and verification and deductive design of systems. The book is a memoir documenting scientific work done by the NADA Working Group within ESPRIT Basic Research Action 8533. The chapters address theoretical topics including stream processing, spatially extended systems, hierarchical structures, and integration of digital analogue models. There are case studies of superscalar processors, the Java Virtual Machine, and biological excitable media; various design and verification techniques are presented.

B. Möller: An Algebraic Approach to Systolic Circuits.
Institut für Informatik, Universität Augsburg, Report 1998-1

The goal of deductive design is the systematic construction of a system implementation starting from its behavioural specification according to formal, provably correct rules. We use Gofer/Haskell to formulate a functional model of directional, synchronous and deterministic systems with discrete time. We develop an algebra of slowdown. The associated laws are then employed in deductive hardware design of two systolic circuits, a convolver and a recognizer for regular expressions. The strategy used is applicable to the derivation of other systolic circuits as well.

B. Möller: Ideal Stream Algebra.
Institut für Informatik, Universität Augsburg, Report 1997-10. Revised version in: B. Möller, J.V. Tucker (eds.): Prospects for hardware foundations. Lecture Notes in Computer Science 1546. Berlin: Springer 1998, 69-116

We provide some mathematical properties of behaviours of systems, where the individual elements of a behaviour are modeled by ideals of a suitable partial order. It is well-known that the associated ideal completion provides a simple way of constructing algebraic cpos. An ideal can be viewed as a set of consistent finite or compact approximations of an object which itself may even be infinite. A special case is the domain of streams where the finite approximations are the finite prefixes of a stream. We introduce a special way of characterising behaviours through sets of relevant approximations. This is a generalisation of the technique used earlier for the case of streams. Given a subset P of partially ordered set (M,<=), we define

ide P := { close(Q) : Q a directed subset of P }

B. Möller: Deductive Hardware Design: A Functional Approach.
Institut für Informatik, Universität Augsburg, Report 1997-9. Revised version in: B. Möller, J.V. Tucker (eds.): Prospects for hardware foundations. Lecture Notes in Computer Science 1546. Berlin: Springer 1998, 420-468

The goal of deductive design is the systematic construction of a system implementation starting from its behavioural specification according to formal, provably correct rules. We use Gofer/Haskell to formulate a functional model of directional, synchronous and deterministic systems with discrete time. The associated algebraic laws are then employed in deductive hardware design of basic combinational and sequential circuits as well as a brief account of pipelining. With this we tackle several of the IFIP WG 10.5 benchmark verification problems. Special emphasis is laid on parameterisation and re-usability aspects.

T. Brunn, B. Möller, M. Russling: Layered Graph Traversals and Hamiltonian Path Problems - An Algebraic Approach.
Institut für Informatik, Universität Augsburg, Report 1997-8. Revised version in: J. Jeuring (ed.): Mathematics of Program Construction. Lecture Notes in Computer Science 1422. Berlin: Springer 1998, 96-121

Using an algebra of paths we present abstract algebraic derivations for two problem classes concerning graphs, viz. layer oriented traversal and computing sets of Hamiltonian paths. In the first case, we are even able to abstract to the very general setting of Kleene algebras. Applications include reachability and a shortest path problem as well as topological sorting, cycle detection and finding maximum cardinality matchings.

B. Möller: Linked Lists Calculated.
Institut für Informatik, Universität Augsburg, Report 1997-7.

We use a relational calculus of pointer structures to calculate a number of standard algorithms on singly linked lists, both acyclic and cyclic. This shows that our techniques are not just useful for tree-like structures, but apply to general pointer structures as well. 

B. Möller: Calculating With Pointer Structures.
In: R. Bird, L. Meertens (eds.): Algorithmic languages and calculi. Proc. IFIP TC2/WG2.1 Working Conference, Le Bischenberg, Feb. 1997. Chapman&Hall 1997, 24-48

Based on the algebra of relations and maps we present some techniques for safe manipulation of pointer structures, with a special emphasis on tree-like structures. We investigate sufficient criteria for preservation of substructures under selective updating. The approach is illustrated with some simple examples. 

W. Dosch, B. Möller: Calculating a Module for Binary Search Trees.
In: W. Kluge (ed.): Implementation of Functional Languages. Selected Papers from the 8th International Workshop, Bad Godesberg, Germany, September 1996. Lecture Notes in Computer Science 1268. Berlin: Springer 1997, 267-284

We formally derive a functional module for binary search trees comprising search, insert, delete, minimum and maximum operations. The derivation starts with an extensional specification that refers only to the multiset of elements stored in the tree.

B. Möller: Assertions and Recursions.
In: G. Dowek, J. Heering, K. Meinke, B. Möller (eds.): Higher order algebra, logic and term rewriting. Second International Workshop, Paderborn, Sept. 21-22, 1995. Lecture Notes in Computer Science 1074. Berlin: Springer 1996, 163-184

We provide an algebraic description of subtypes and the way they propagate through recursive functions. By abstracting from the concrete domain of functions or relations we obtain a framework which is independent of strict or non-strict, deterministic or non-deterministic semantics. Applications include efficiency increasing simplification of recursions as well as proofs about recursions by noetherian induction, such as termination proofs.

B. Möller: Refining Ideal Behaviours.
Institut für Mathematik, Universität Augsburg, Report Nr. 345, 1995

We provide some mathematical properties of behaviours of systems, where the individual elements of a behaviour are modeled by ideals of a suitable partial order. It is well-known that the associated ideal completion provides a simple way of constructing algebraic cpos. An ideal can be viewed as a set of consistent finite or compact approximations of an object which itself may even be infinite. We introduce a special way of characterising behaviours through sets of relevant approximations. This is a generalisation of the technique used in the Ideal Streams paper for the case of streams. Given a subset P of partially ordered set (M,<=), we define

ide P := { close(Q) : Q a directed subset of P }

B. Möller, M. Russling: Shorter Paths to Graph Algorithms.
Science of Computer Programming 22, 157-180 (1994)

We illustrate the use of formal languages and relations in compact formal derivations of algorithms for computing the length of a shortest path between two graph vertices and for cycle detection.

B. Möller: Ordered and continuous models of higher-order specifications.
In: J. Heering, K. Meinke, B. Möller, T. Nipkow (eds.): Higher-Order algebra, logic and term rewriting. Lecture Notes in Computer Science 816. Berlin 1994, 223-255

We investigate the existence of continuous and fixpoint models of higher-order specifications. Particular attention is paid to the question of extensionality. We use ordered specifications, a particular case of Horn specifications. The main tool for obtaining continuous models is the ideal completion. Unfortunately, it may destroy extensionality. This problem is inherent: we show that there is no completion method which is guaranteed to preserve extensionality. To restore it, generally a quotient has to be taken. It is shown that under certain conditions this preserves the existence of least fixpoints. Examples of the specification method include the essential concepts of Backus's FP and Hoare's CSP.

B. Möller: Ideal Streams.
In: E.-R. Olderog (ed.): Programming Concepts, Methods and Calculi. IFIP Transactions A-56. Amsterdam: North-Holland 1994, 39-58

We introduce operators and laws of an algebra of formal languages, a subalgebra of which corresponds to the algebra of (multiary) relations. This algebra is then used to give a simplified semantics for finite and infinite streams, based on the ideal completion. We show how some essential operations on streams and notions concerning correctness are expressed and show the use of the underlying algebra in reasoning about streams. Moreover, we give a simple treatment of non-determinacy. The approach is illustrated with a formal description and correctness proof for the alternating bit protocol. This study is part of an attempt to single out a framework for program development at a very high level of discourse, close to informal reasoning but still with full formal precision.