Publications

Important Copyright Notice: This material is presented to ensure timely distribution of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders, such as publishers (Springer, Elsevier...). All persons copying this information are expected to adhere to the terms and constraints invoked by each copyright holder. In most cases, these works may not be reposted without explicit permission of the copyright holder.

Books

1. P. Höfner: Algebraic Calculi for Hybrid Systems. Books on Demand, 2009. (Phd Thesis) isbn: 9783839125106
   details | bibtex
   @Book{Hoefner2009-5,
       Author = {H{\"o}fner, P.},
       Title = {Algebraic Calculi for Hybrid Systems},
       Publisher = {Books on Demand},
       Year = {2009},
       Isbn = {9783839125106},
       Note ={(Phd Thesis)},
       Doi = {}
   }

Book Chapters

1. R. Bird, J. Gibbons, R. Hinze, P. Höfner, J. Jeuring, L. Meertens, B. Möller, C. Morgan, T. Schrijvers, W. Swierstra, N. Wu: Algorithmics. In Advancing Research in Information and Communication Technology, IFIP Advances in Information and Communication Technology 600:59-98, Springer, 2021.
   doi: 10.1007/978-3-030-81701-5_3
   abstract | pdf | bibtex

   Abstract:

   Algorithmics is the study and practice of taking a high-level description of a program's purpose and, from it, producing an executable program of acceptable efficiency. Each step in that process is justified by rigorous, careful reasoning at the moment it is taken; and the repertoire of steps allowed by that rigour, at each stage, guides the development of the algorithm itself. IFIP's Working Group 2.1 has always been concerned with Algorithmics: both the design of its notations and the laws that enable its calculations. Even ALGOL 60 showed that orthogonality, simplicity and rigour in a programming language improves the quality of its programs. Our Group's title ``Algorithmic Languages and Calculi'' describes our activities: the discovery of precise but more general rules of calculational reasoning for the many new styles of programming that have developed over the 60 years since IFIP’s founding. As our contribution to the birth- day celebrations, we outline how we have tried to contribute during those decades to the rigorous and reliable design of computer programs of all kinds -- to Algorithmics.
   @InBook{Hoefner2021-2,
       Author = {Bird, R. and Gibbons, J. and Hinze, R. and H{\"o}fner, P. and Jeuring, J. and Meertens, L. and M{\"o}ller, B. and Morgan, C. and Schrijvers, T. and Swierstra, W. and Wu, N.},
       Editor = {},
       Title = {Algorithmics},
       BookTitle = {Advancing Research in Information and Communication Technology},
       Series = {IFIP Advances in Information and Communication Technology},
       Volume = {600},
       Pages = {59-98},
       Publisher = {Springer},
       Year = {2021},
       Doi = {10.1007/978-3-030-81701-5_3}
   }
2. P. Höfner: Using Process Algebra to Design Better Protocols. In The Role and Importance of Mathematics in Innovation, Mathematics for Industry 25:87-101, Springer, 2016.
   doi: 10.1007/978-981-10-0962-4_8
   abstract | pdf | bibtex

   Abstract:

   Protocol design, development and standardisation still follow the lines of rough consensus and running code. This approach yields fast and impressive results in a sense that protocols are actually implemented and shipped, but comes at a price: protocol specifications, which are mainly written in natural languages without presenting a formal specification , are (excessively) long, ambiguous, underspecified and erroneous. These shortcomings are neither new nor surprising, and well documented. It is the purpose of this paper to provide further evidence that formal methods in general and process algebras in particular can overcome these problems. They provide powerful tools that help to analyse and evaluate protocols, already during the design phase. To illustrate this claim, I report how a combination of pen-and-paper analysis, model checking and interactive theorem proving has helped to perform a formal analysis of the Ad hoc On-Demand Vector (AODV) routing protocol.
   @InBook{Hoefner2016-11,
       Author = {H{\"o}fner, P.},
       Editor = {Anderssen, B. and Broadbridge, P. and Fukumoto, Y. and Kamiyama, N. and Mizoguchi, Y. and Polthier, K. and Saeki, O.},
       Title = {Using Process Algebra to Design Better Protocols},
       BookTitle = {The Role and Importance of Mathematics in Innovation},
       Series = {Mathematics for Industry},
       Volume = {25},
       Pages = {87-101},
       Publisher = {Springer},
       Year = {2016},
       Doi = {10.1007/978-981-10-0962-4_8}
   }

Articles in Journals

1. R. Berghammer, H. Hitoshi, W. Guttmann, P. Höfner: Relational Characterisations of Paths. In Journal of Logic and Algebraic Methods in Programming 117, Elsevier, 2020.
   arXiv: CoRR abs/1801.04026 | doi: 10.1016/j.jlamp.2020.100590
   abstract | pdf | bibtex

   Abstract:

   Binary relations are one of the standard ways to encode, characterise and reason about graphs. Relation algebras provide equational axioms for a large fragment of the calculus of binary relations. Although relations are standard tools in many areas of mathematics and computing, researchers usually fall back to point-wise reasoning when it comes to arguments about paths in a graph. We present a purely algebraic way to specify different kinds of paths in relation algebras. We study the relationship between paths with a designated root vertex and paths without such a vertex. Since we stay in first-order logic this development helps with mechanising proofs. To demonstrate the applicability of the algebraic framework we verify the correctness of three basic graph algorithms. All results of this paper are formally verified using Isabelle/HOL.
   @article{Hoefner2020-3,
       Author = {Berghammer, R. and Hitoshi, H. and Guttmann, W. and H{\"o}fner, P.},
       Title = {Relational Characterisations of Paths},
       Journal = {Journal of Logic and Algebraic Methods in Programming},
       Volume = {117},
       Year = {2020},
       Publisher = {Elsevier},
       Doi = {10.1016/j.jlamp.2020.100590}
   }
2. R.J. van Glabbeek, P. Höfner: Progress, Justness and Fairness. In ACM Computing Surveys 52(4):69:1-69:38, ACM, 2019.
   arXiv: CoRR abs/1810.07414 | doi: 10.1145/3329125
   abstract | pdf | bibtex

   Abstract:

   Fairness assumptions are a valuable tool when reasoning about systems. In this paper, we classify several fairness properties found in the literature and argue that most of them are too restrictive for many applications. As an alternative we introduce the concept of justness.
   @article{Hoefner2019-2,
       Author = {van Glabbeek, R.J. and H{\"o}fner, P.},
       Title = {Progress, Justness and Fairness},
       Journal = {ACM Computing Surveys},
       Number = {4},
       Volume = {52},
       Pages = {69:1-69:38},
       Year = {2019},
       Publisher = {ACM},
       Doi = {10.1145/3329125}
   }
3. R. Berghammer, N. Danilenko, P. Höfner, I. Stucke: Cardinality of Relations with Applications. In Discrete Mathematics 339(12):3089-3115, Elsevier, 2016.
   doi: 10.1016/j.disc.2016.06.019
   abstract | pdf | bibtex

   Abstract:

   Based on Y. Kawahara’s characterisation of the cardinality of relations we derive some fundamental properties of cardinalities concerning vectors, points and mapping-related relations. As applications of these results we verify some properties of linear orders and graphs in a calculational manner. These include the cardinalities of rooted trees and some estimates concerning graph parameters. We also calculationally prove the result of D. Kőnig that in bipartite graphs the matching number equals the vertex cover number.
   @article{Hoefner2016-9,
       Author = {Berghammer, R. and Danilenko, N. and H{\"o}fner, P. and Stucke, I.},
       Title = {Cardinality of Relations with Applications},
       Journal = {Discrete Mathematics},
       Number = {12},
       Volume = {339},
       Pages = {3089-3115},
       Year = {2016},
       Publisher = {Elsevier},
       Doi = {10.1016/j.disc.2016.06.019}
   }
4. T. Bourke, R.J. van Glabbeek, P. Höfner: Mechanizing a Process Algebra for Network Protocols. In Journal of Automated Reasoning 56(3):309-341, Springer, 2016.
   doi: 10.1007/s10817-015-9358-9
   abstract | pdf | bibtex

   Abstract:

   This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invariant properties. Mechanizing the core process algebra in Isabelle/HOL is relatively standard, but its layered structure necessitates special treatment. The control states of reactive processes, such as nodes in a network, are modelled by terms of the process algebra. We propose a technique based on these terms to streamline proofs of inductive invariance. This is not sufficient, however, to state and prove invariants that relate states across multiple processes (entire networks). To this end, we propose a novel compositional technique for lifting global invariants stated at the level of individual nodes to networks of nodes.
   @article{Hoefner2016-6,
       Author = {Bourke, T. and van Glabbeek, R.J. and H{\"o}fner, P.},
       Title = {Mechanizing a Process Algebra for Network Protocols},
       Journal = {Journal of Automated Reasoning},
       Number = {3},
       Volume = {56},
       Pages = {309-341},
       Year = {2016},
       Publisher = {Springer},
       Doi = {10.1007/s10817-015-9358-9}
   }
5. R.J. van Glabbeek, P. Höfner, M. Portmann, W.L. Tan: Modelling and Verifying the AODV Routing Protocol. In Distributed Computing 29(4):279-315, Springer, 2016.
   arXiv: CoRR abs/1512.08867 | doi: 10.1007/s00446-015-0262-7
   abstract | pdf | bibtex

   Abstract:

   This paper presents a formal specification of the Ad hoc On-Demand Distance Vector (AODV) routing protocol using AWN (Algebra for Wireless Networks), a recent process algebra which has been tailored for the modelling of Mobile Ad Hoc Networks and Wireless Mesh Network protocols. Our formalisation models the exact details of the core functionality of AODV, such as route discovery, route maintenance and error handling. We demonstrate how AWN can be used to reason about critical protocol properties by providing detailed proofs of loop freedom and route correctness.
   @article{Hoefner2016-3,
       Author = {van Glabbeek, R.J. and H{\"o}fner, P. and Portmann, M. and Tan, W.L.},
       Title = {Modelling and Verifying the {AODV} Routing Protocol},
       Journal = {Distributed Computing},
       Number = {4},
       Volume = {29},
       Pages = {279-315},
       Year = {2016},
       Publisher = {Springer},
       Doi = {10.1007/s00446-015-0262-7}
   }
6. P. Höfner, B. Möller: Extended Feature Algebra. In Journal of Logic and Algebraic Methods in Programming 85(5):952-971, Part 2, Elsevier, 2016.
   doi: 10.1016/j.jlamp.2015.12.002
   abstract | pdf | bibtex

   Abstract:

   Feature Algebra was introduced as an abstract framework for feature-oriented software development. One goal is to provide a common, clearly defined basis for the key ideas of feature-orientation. The algebra captures major aspects of feature-orientation, such as the hierarchical structure of features and feature composition. However, as we will show, it is not able to model aspects at the level of code, i.e., situations where code fragments of different features have to be merged. In other words, it does not reflect details of concrete implementations.
   In this paper we first present concrete models for the original axioms of Feature Algebra which represent the main concepts of feature-oriented programs. This shows that the abstract Feature Algebra can be interpreted in different ways. We then use these models to show that the axioms of Feature Algebra do not properly reflect all aspects of feature-orientation from the level of directory structures down to the level of actual code. This gives motivation to extend the abstract algebra, which is the second main contribution of the paper. We modify the axioms and introduce the concept of an Extended Feature Algebra. As third contribution, we introduce more operators to cover concepts like overriding in the abstract setting.
   @article{Hoefner2016-2,
       Author = {H{\"o}fner, P. and M{\"o}ller, B.},
       Title = {Extended Feature Algebra},
       Journal = {Journal of Logic and Algebraic Methods in Programming},
       Number = {5},
       Volume = {85},
       Pages = {952-971},
       Year = {2016},
       Publisher = {Elsevier},
       Doi = {10.1016/j.jlamp.2015.12.002}
   }
7. R. Berghammer, P. Höfner, I. Stucke: Cardinality of Relations and Relational Approximation Algorithms. In Journal of Logic and Algebraic Methods in Programming 85(2):269-286, Elsevier, 2016.
   doi: 10.1016/j.jlamp.2015.12.001
   abstract | pdf | bibtex

   Abstract:

   First, we discuss three specific classes of relations, which allow to model the essential constituents of graphs, such as vertices and (directed or undirected) edges. Based on Kawahara’s characterisation of the cardinality of relations we then derive fundamental properties on their cardinalities. As main applications of these results, we formally verify four relational programs, which implement approximation algorithms by using the assertion-based method and relation-algebraic calculations.
   @article{Hoefner2016-1,
       Author = {Berghammer, R. and H{\"o}fner, P. and Stucke, I.},
       Title = {Cardinality of Relations and Relational Approximation Algorithms},
       Journal = {Journal of Logic and Algebraic Methods in Programming},
       Number = {2},
       Volume = {85},
       Pages = {269-286},
       Year = {2016},
       Publisher = {Elsevier},
       Doi = {10.1016/j.jlamp.2015.12.001}
   }
8. R.J. van Glabbeek, P. Höfner: CCS: It's not Fair!—Fair Schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions. In Acta Informatica 52(2-3):175-205, Springer, 2015.
   arXiv: CoRR abs/1505.05964 | doi: 10.1007/s00236-015-0221-6
   abstract | pdf | bibtex

   Abstract:

   In the process algebra community it is sometimes suggested that, on some level of abstraction, any distributed system can be modelled in standard process-algebraic specification formalisms like CCS. This sentiment is strengthened by results testifying that CCS, like many similar formalisms, is Turing powerful and provides a mechanism for interaction. This paper counters that sentiment by presenting a simple fair scheduler—one that in suitable variations occurs in many distributed systems—of which no implementation can be expressed in CCS, unless CCS is enriched with a fairness assumption.
   Since Dekker's and Peterson's mutual exclusion protocols implement fair schedulers, it follows that these protocols cannot be rendered correctly in CCS without imposing a fairness assumption. Peterson expressed this algorithm correctly in pseudocode without resorting to a fairness assumption, so it furthermore follows that CCS lacks the expressive power to accurately capture such pseudocode.
   @article{Hoefner2015-2,
       Author = {van Glabbeek, R.J. and H{\"o}fner, P.},
       Title = {CCS: It's not Fair!---Fair Schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions},
       Journal = {Acta Informatica},
       Number = {2-3},
       Volume = {52},
       Pages = {175-205},
       Year = {2015},
       Publisher = {Springer},
       Doi = {10.1007/s00236-015-0221-6}
   }
9. D. Batory, P. Höfner, D. Köppl, B. Möller, A. Zelend: Structured Document Algebra in Action. In Software, Services and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Emeritation 8950:291-311, Springer, 2015.
   doi: 10.1007/978-3-319-15545-6_19
   abstract | pdf | bibtex

   Abstract:

   A Structured Document Algebra (SDA) defines modules with variation points and how such modules compose. The basic operations are module addition and replacement. Repeated addition can create nested module structures. SDA also allows the decomposition of mod- ules into smaller parts. In this paper we show how SDA modules can be used to deal algebraically with Software Product Lines (SPLs). In particular, we treat some fundamental concepts of SPLs, such as refine- ment and refactoring. This leads to mathematically precise formalization of fundamental concepts used in SPLs, which can be used for improved Feature-Oriented Software Development (FOSD) tooling.
   @article{Hoefner2015-1,
       Author = {Batory, D. and H{\"o}fner, P. and K{\"o}ppl, D. and M{\"o}ller, B. and Zelend, A.},
       Title = {Structured Document Algebra in Action},
       Journal = { Software, Services and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Emeritation},
       Volume = {8950},
       Pages = {291-311},
       Year = {2015},
       Publisher = {Springer},
       Doi = {10.1007/978-3-319-15545-6_19}
   }
10. P. Höfner, A. McIver: Hopscotch—Reaching the Target Hop by Hop. In Journal of Logic and Algebraic Methods in Programming 83(2):212-224, Elsevier, 2014.
    doi: 10.1016/j.jlap.2014.02.009
    abstract | pdf | bibtex

    Abstract:

    Concrete and abstract relation algebras have widespread applications in computer science. One of the most famous is graph theory. Classical relations, however, only reason about connectivity, not about the length of a path between nodes. Generalisations of relation algebra, such as the min-plus algebra, use numbers allowing the treatment of weighted graphs. In this way one can for example determine the length of shortest paths (e.g. Dijkstra's algorithm). In this paper we treat matrices that carry even more information, such as the \"next hop\" on a path towards a destination. In this way we can use algebra not only for determining the length of paths, but also the concrete path. We show how paths can be reconstructed from these matrices, hop by hop. We further sketch an application for message passing in wireless networks.
    @article{Hoefner2014-2,
        Author = {H{\"o}fner, P. and McIver, A.},
        Title = {Hopscotch---Reaching the Target Hop by Hop},
        Journal = {Journal of Logic and Algebraic Methods in Programming},
        Number = {2},
        Volume = {83},
        Pages = {212-224},
        Year = {2014},
        Publisher = {Elsevier},
        Doi = {10.1016/j.jlap.2014.02.009}
    }
11. P. Höfner, B. Möller: Dijkstra, Floyd and Warshall meet Kleene. In Formal Aspects of Computing 24(4-6):459-476, Springer, 2012.
    doi: 10.1007/s00165-012-0245-4
    abstract | pdf | bibtex

    Abstract:

    Around 1960, Dijkstra, Floyd and Warshall published papers on algorithms for solving single-source and all-sources shortest path problems, respectively. These algorithms, nowadays named after their inventors, are well known and well established. This paper sheds an algebraic light on these algorithms. We combine the shortest path problems with Kleene algebra, also known as Conway's regular algebra. This view yields a purely algebraic version of Dijkstra's shortest path algorithm and the one by Floyd/Warshall. Moreover, the algebraic abstraction yields applications of these algorithms to structures different from graphs and pinpoints the mathematical requirements on the underlying cost algebra that ensure their correctness.
    @article{Hoefner2012-4,
        Author = {H{\"o}fner, P. and M{\"o}ller, B.},
        Title = {{Dijkstra}, {Floyd} and {Warshall} meet {Kleene}},
        Journal = {Formal Aspects of Computing},
        Number = {4-6},
        Volume = {24},
        Pages = {459-476},
        Year = {2012},
        Publisher = {Springer},
        Doi = {10.1007/s00165-012-0245-4}
    }
12. P. Höfner, R.J. van Glabbeek, I.J. Hayes: Morgan: a suitable case for treatment (Preface). In Formal Aspects of Computing 24(4-6):417-422, Springer, 2012. (Festschrift in Honour of Carroll Morgan)
    doi: 10.1007/s00165-012-0257-0
    abstract | pdf | bibtex

    Abstract:

    The achievements of Professor Charles Carroll Morgan as a scientific expert and a computer scientist are discussed. Carroll, as a computer programmer at Ascomp, worked in 'Laws of Programming' after joining the Programming Research Group. He is also credited to describe large and complex static structures by combining building blocks known as schemas and proposing the notion of Dynamic-schemas, which are in line with the building blocks used for static properties, and developed a corresponding calculus. Carroll's book 'Programming from Specifications' is seen as the reference for the refinement calculus and provides a thorough treatment of elementary program constructs which were later incorporated as elements. In 2000 Carroll joined his Alma Mater UNSW as adjunct professor where he worked on operational interpretation of the quantitative μ-calculus qMμ as a turn-based game between two players.
    @article{Hoefner2012-3,
        Author = {H{\"o}fner, P. and van Glabbeek, R.J. and Hayes, I.J.},
        Title = {Morgan: a suitable case for treatment (Preface)},
        Journal = {Formal Aspects of Computing},
        Number = {4-6},
        Volume = {24},
        Pages = {417-422},
        Year = {2012},
        Publisher = {Springer},
        Doi = {10.1007/s00165-012-0257-0}
    }
13. P. Höfner, B. Möller: Fixing Zeno Gaps. In Theoretical Computer Science 412(28):3303-3322, Elsevier, 2011.
    doi: j.tcs.2011.03.018
    abstract | pdf | bibtex

    Abstract:

    In computer science fixpoints play a crucial role. Most often least and greatest fixpoints are sufficient. However there are situations where other ones are needed. In this paper we study, on an algebraic base, a special fixpoint of the function f(x) = a⋅x that describes infinite iteration of an element a. We show that the greatest fixpoint is too imprecise. Special problems arise if the iterated element contains the possibility of stepping on the spot (e.g. skip in a programming language) or if it allows Zeno behaviour. We present a construction for a fixpoint that captures these phenomena in a precise way. The theory is presented and motivated using an example from hybrid system analysis.
    @article{Hoefner2011-6,
        Author = {H{\"o}fner, P. and M{\"o}ller, B.},
        Title = {Fixing Zeno Gaps},
        Journal = {Theoretical Computer Science},
        Number = {28},
        Volume = {412},
        Pages = {3303-3322},
        Year = {2011},
        Publisher = {Elsevier},
        Doi = {j.tcs.2011.03.018}
    }
14. P. Höfner, R. Khedri, B. Möller: Supplementing Product Families with Behaviour. In International Journal of Software and Informatics 5(1-2):245-266, Part II, Institute of Software, Chinese Academy of Sciences, 2011.
    abstract | pdf | bibtex

    Abstract:

    A common approach to dealing with software requirements volatility is to define product families instead of single products. In earlier papers we have developed an algebra of such families that, roughly, consists in a more abstract view of FODA-like and/or trees of features. A product family is represented by an algebraic term over the feature names that can be manipulated using equational laws such as associativity or distributivity. Initially, only \"syntactic\" models of the algebra were considered, giving more or less just the names of the features used in the various products of a family and certain interrelations such as mandatory occurrence and implication between or mutual exclusion of features, without attaching any kind of \"meaning\" to the features. While this is interesting and useful for determining the variety and number of possible members of such a family, it is wholly insufficient when it comes to talking about the correctness of families in a semantic sense. In the present paper we define a class of \"semantic\" models of the general abstract product family algebra that allow treating very relevant additional questions. In these models, the features of a family are requirements scenarios formalised as pairs of relational specifications of a proposed system and its environment. However, the paper is just intended as a proof of feasibility; we are convinced that the approach can also be employed for different semantic models such as general denotational or stream-based semantics.
    @article{Hoefner2011-3,
        Author = {H{\"o}fner, P. and Khedri, R. and M{\"o}ller, B.},
        Title = {Supplementing Product Families with Behaviour},
        Journal = {International Journal of Software and Informatics},
        Number = {1-2},
        Volume = {5},
        Pages = {245-266},
        Year = {2011},
        Publisher = {Institute of Software, Chinese Academy of Sciences},
    }
15. H.H. Dang, P. Höfner, B. Möller: Algebraic Separation Logic. In Journal of Logic and Algebraic Programming 80(6):221-247, Elsevier, 2011.
    doi: 10.1016/j.jlap.2011.04.003
    abstract | pdf | bibtex

    Abstract:

    We present an algebraic approach to separation logic. In particular, we give an algebraic characterisation for assertions of separation logic, discuss different classes of assertions and prove abstract laws fully algebraically. After that, we use our algebraic framework to give a relational semantics of the commands of a simple programming language associated with separation logic. On this basis we prove the frame rule in an abstract and concise way, parametric in the operator of separating conjunction, of which two particular variants are discussed. In this we also show how to algebraically formulate the requirement that a command preserves certain variables. The algebraic view does not only yield new insights on separation logic but also shortens proofs due to a point free representation. It is largely first-order and hence enables the use of off-the-shelf automated theorem provers for verifying properties at an abstract level.
    @article{Hoefner2011-2,
        Author = {Dang, H.H. and H{\"o}fner, P. and M{\"o}ller, B.},
        Title = {Algebraic Separation Logic},
        Journal = {Journal of Logic and Algebraic Programming},
        Number = {6},
        Volume = {80},
        Pages = {221-247},
        Year = {2011},
        Publisher = {Elsevier},
        Doi = {10.1016/j.jlap.2011.04.003}
    }
16. P. Höfner, R. Khedri, B. Möller: An Algebra of Product Families. In Software & Systems Modeling 10(2):161-182, 2011.
    doi: 10.1007/s10270-009-0127-2
    abstract | pdf | bibtex

    Abstract:

    Experience from recent years has shown that it is often advantageous not to build a single product but rather a family of similar products that share at least one common functionality while having well-identified variabilities. Such product families are built from elementary features that reach from hardware parts to software artefacts such as requirements, architectural elements or patterns, components, middleware, or code. We use the well established mathematical structure of idempotent semirings as the basis for a product family algebra that allows a formal treatment of the above notions. A particular application of the algebra concerns the multi-view reconciliation problem that arises when complex systems are modelled. We use algebraic integration constraints linking features in one view to features in the same or a different view and show in several examples the suitability of this approach for a wide class of integration constraint formulations. Our approach is illustrated with a Haskell prototype implementation of one particular model of product family algebra.
    @article{Hoefner2011-1,
        Author = {H{\"o}fner, P. and Khedri, R. and M{\"o}ller, B.},
        Title = {An Algebra of Product Families},
        Journal = {Software & Systems Modeling},
        Number = {2},
        Volume = {10},
        Pages = {161-182},
        Year = {2011},
        Doi = {10.1007/s10270-009-0127-2}
    }
17. P. Höfner, G. Struth: Algebraic Notions of Nontermination: Omega and Divergence in Idempotent Semirings. In Journal of Logic and Algebraic Programming 79(8):794-811, Springer, 2010.
    doi: 10.1016/j.jlap.2010.07.016
    abstract | pdf | bibtex

    Abstract:

    Two notions of nontermination are studied and compared in the setting of idempotent semirings: Cohen's omega operator and a divergence operator. They are determined for various computational models, and conditions for their existence and their coincidence are given. It turns out that divergence yields a simple and natural way of modelling infinite behaviours of programs and discrete systems, whereas the omega operator shows some anomalies.
    @article{Hoefner2010-1,
        Author = {H{\"o}fner, P. and Struth, G.},
        Title = {Algebraic Notions of Nontermination: Omega and Divergence in Idempotent Semirings},
        Journal = {Journal of Logic and Algebraic Programming},
        Number = {8},
        Volume = {79},
        Pages = {794-811},
        Year = {2010},
        Publisher = {Springer},
        Doi = {10.1016/j.jlap.2010.07.016}
    }
18. P. Höfner, G. Struth, G. Sutcliffe: Automated Verification of Refinement Laws. In Annals of Mathematics and Artificial Intelligence 55(1-2):35-62, Springer, 2009.
    doi: 10.1007/s10472-009-9151-8
    abstract | pdf | bibtex

    Abstract:

    Demonic refinement algebras are variants of Kleene algebras. Introduced by von Wright as a light-weight variant of the refinement calculus, their intended semantics are positively disjunctive predicate transformers, and their calculus is entirely within first-order equational logic. So, for the first time, off-the-shelf automated theorem proving (ATP) becomes available for refinement proofs. We used ATP to verify a toolkit of basic refinement laws. Based on this toolkit, we then verified two classical complex refinement laws for action systems by ATP: a data refinement law and Back's atomicity refinement law. We also present a refinement law for infinite loops that has been discovered through automated analysis. Our proof experiments not only demonstrate that refinement can effectively be automated, they also compare eleven different ATP systems and suggest that program verification with variants of Kleene algebras yields interesting theorem proving benchmarks. Finally, we apply hypothesis learning techniques that seem indispensable for automating more complex proofs.
    @article{Hoefner2009-2,
        Author = {H{\"o}fner, P. and Struth, G. and Sutcliffe, G.},
        Title = {Automated Verification of Refinement Laws},
        Journal = {Annals of Mathematics and Artificial Intelligence},
        Number = {1-2},
        Volume = {55},
        Pages = {35-62},
        Year = {2009},
        Publisher = {Springer},
        Doi = {10.1007/s10472-009-9151-8}
    }
19. P. Höfner, B. Möller: An Algebra of Hybrid Systems. In Journal of Logic and Algebraic Programming 78(2):74-97, Springer, 2009.
    doi: 10.1016/j.jlap.2008.08.005
    abstract | pdf | bibtex

    Abstract:

    Hybrid systems are heterogeneous systems characterised by the interaction of discrete and continuous dynamics. We present a trajectory-based algebraic model for describing hybrid systems; the trajectories used are closely related to streams. The algebra is based on left quantales and left semirings and provides a new application for these algebraic structures. We show that hybrid automata, which are probably the standard tool for describing hybrid systems, can conveniently be embedded into our algebra. Moreover we point out some important advantages of the algebraic approach. In particular, we show how to handle Zeno effects, which are excluded by most other authors. The development of the theory is illustrated by a running example and a larger case study.
    @article{Hoefner2009-1,
        Author = {H{\"o}fner, P. and M{\"o}ller, B.},
        Title = {An Algebra of Hybrid Systems},
        Journal = {Journal of Logic and Algebraic Programming},
        Number = {2},
        Volume = {78},
        Pages = {74-97},
        Year = {2009},
        Publisher = {Springer},
        Doi = {10.1016/j.jlap.2008.08.005}
    }
20. P. Höfner, B. Möller: Algebraic Neighbourhood Logic. In Journal of Logic and Algebraic Programming 76(1):35-59, Springer, 2008.
    doi: 10.1016/j.jlap.2007.10.004
    abstract | pdf | bibtex

    Abstract:

    We present an algebraic embedding of Neighbourhood Logic (NL) into the framework of semirings which yields various simplifications. For example, some of the NL axioms can be dropped, since they are theorems in our framework, and Galois connections produce properties for free. A further simplification is achieved, since the semiring methods used are easy and fairly standard. Moreover, this embedding allows us to reuse knowledge from Neighbourhood Logic in other areas of Computer Science. Since in its original axiomatisation the logic cannot handle intervals of infinite length and therefore not fully model and specify reactive and hybrid systems, using lazy semirings we introduce an extension of NL to intervals of finite and infinite length. Furthermore, we discuss connections between the (extended) logic and other application areas, like Allen's thirteen relations between intervals, the branching time temporal logic CTL* and hybrid systems.
    @article{Hoefner2008-3,
        Author = {H{\"o}fner, P. and M{\"o}ller, B.},
        Title = {Algebraic Neighbourhood Logic},
        Journal = {Journal of Logic and Algebraic Programming},
        Number = {1},
        Volume = {76},
        Pages = {35-59},
        Year = {2008},
        Publisher = {Springer},
        Doi = {10.1016/j.jlap.2007.10.004}
    }
21. P. Höfner, G. Struth: Can Refinement be Automated?. In Electronic Notes in Theoretical Computer Science 201:197-222, Elsevier, 2008.
    doi: 10.1016/j.entcs.2008.02.021
    abstract | pdf | bibtex

    Abstract:

    We automatically verify Back's atomicity refinement law and a classical data refinement law for action systems. Our novel approach mechanises a refinement calculus based on Kleene algebras in an off the shelf resolution and paramodulation theorem prover and a counterexample checker with heuristics for hypothesis learning. The proofs are supported by a toolkit of meaningful refinement laws that has also been verified and that, for the first time, allows the refinement of programs and software systems, and the verification of further complex refinement laws, by automated deduction. This suggests that a substantial proportion of refinement could indeed be automated.
    @article{Hoefner2008-2,
        Author = {H{\"o}fner, P. and Struth, G.},
        Title = {Can Refinement be Automated?},
        Journal = {Electronic Notes in Theoretical Computer Science},
        Volume = {201},
        Pages = {197-222},
        Year = {2008},
        Publisher = {Elsevier},
        Doi = {10.1016/j.entcs.2008.02.021}
    }
22. P. Höfner, F. Lautenbacher: Algebraic Structure of Web Services. In Electronic Notes in Theoretical Computer Science 200(3):171-187, Elsevier, 2008.
    doi: 10.1016/j.entcs.2008.04.099
    abstract | pdf | bibtex

    Abstract:

    Web Services and Service-Oriented Architecture in general are promising concepts to overcome difficulties such as heterogeneity, scalability, etc. In this paper we present an algebraic structure of Web Services which assist users in Web Service composition and formal description of their services. Using relation algebra, tests and iteration offer the possibility of an automatic composition of Web Services based on a specified goal.
    @article{Hoefner2008-1,
        Author = {H{\"o}fner, P. and Lautenbacher, F.},
        Title = {Algebraic Structure of Web Services},
        Journal = {Electronic Notes in Theoretical Computer Science},
        Number = {3},
        Volume = {200},
        Pages = {171-187},
        Year = {2008},
        Publisher = {Elsevier},
        Doi = {10.1016/j.entcs.2008.04.099}
    }
23. P. Höfner: Semiring Neighbours: An Algebraic Embedding and Extension of Neighbourhood Logic. In Electronic Notes in Theoretical Computer Science 191:49-72, Elsevier, 2007.
    doi: 10.1016/j.entcs.2006.09.040
    abstract | pdf | bibtex

    Abstract:

    In 1996 Zhou and Hansen proposed a first-order interval logic called Neighbourhood Logic (NL) for specifying liveness and fairness of computing systems and defining notions of real analysis in terms of expanding modalities. After that, Roy and Zhou developed a sound and relatively complete Duration Calculus as an extension of NL. We present an embedding of NL into an idempotent semiring of intervals. This embedding allows us to extend NL from single intervals to sets of intervals as well as to extend the approach to arbitrary idempotent semirings. We show that most of the required properties follow directly from Galois connections, hence we get many properties for free. As one important result we obtain that some of the axioms which were postulated for NL can be dropped since they are theorems in our generalisation. Furthermore, we discuss other interval operations like Allen's 13 relations between intervals and their relationship to semiring neighbours. Then we present some possible interpretations for neighbours beyond interval settings. Here we discuss for example reachability in graphs and applications to hybrid systems. At the end of the paper we add finite and infinite iteration to NL and extend idempotent semirings to Kleene algebras and ω algebras. These extensions are useful for formulating properties of repetitive procedures like loops.
    @article{Hoefner2007-1,
        Author = {H{\"o}fner, P.},
        Title = {Semiring Neighbours: An Algebraic Embedding and Extension of Neighbourhood Logic},
        Journal = {Electronic Notes in Theoretical Computer Science},
        Volume = {191},
        Pages = {49-72},
        Year = {2007},
        Publisher = {Elsevier},
        Doi = {10.1016/j.entcs.2006.09.040}
    }

Papers in Conference and Workshop Proceedings

1. C. Bannister, P. Höfner, G. Struth: Effect Algebras, Girard Quantales and Complementation in Separation Logic. In U. Fahrenberg, M. Gehrke, L. Santocanale, M. Winter (eds.), elational and Algebraic Methods in Computer Science (RAMiCS 2021). Lecture Notes in Computer Science 13027, pp. 37-53, Springer, 2021.
   doi: 10.1007/978-3-030-88701-8_3
   abstract | pdf | bibtex

   Abstract:

   We study convolution and residual operations within convolution quantales of maps from partial abelian semigroups and effect algebras into value quantales, thus generalising separating conjunction and implication of separation logic to quantitative settings. We show that effect algebras lift to Girard convolution quantales, but not the standard partial abelian monoids used in separation logic. It follows that the standard assertion quantales of separation logic do not admit a linear negation relating convolution and its right adjoint. We consider alternative dualities for these operations on convolution quantales using boolean negations, some old, some new, relate them with properties of the underlying partial abelian semigroups and outline potential uses.
   @InProceedings{Hoefner2021-5,
       Author = {Bannister, C. and H{\"o}fner, P. and Struth, G.},
       Title = {Effect Algebras, Girard Quantales and Complementation in Separation Logic},
       BookTitle = {elational and Algebraic Methods in Computer Science (RAMiCS 2021)},
       Editor = {Fahrenberg, U. and Gehrke, M. and Santocanale, L. and Winter, M.},
       Series = {Lecture Notes in Computer Science},
       Volume = {13027},
       Pages = {37-53},
       Year = {2021},
       Publisher = {Springer},
       Doi = {10.1007/978-3-030-88701-8_3}
   }
2. R.J. van Glabbeek, P. Höfner, W. Wang: Enabling Preserving Bisimulation Equivalence. In Concurrency Theory (CONCUR 2021). LIPIcs 203, pp. 33:1-33:20, Schloss Dagstuhl -- Leibniz-Zentrum für Informatik, 2021.
   arXiv: CoRR abs/2108.00142 | doi: 10.4230/LIPIcs.CONCUR.2021.33
   abstract | pdf | bibtex

   Abstract:

   Most fairness assumptions used for verifying liveness properties are criticised for being too strong or unrealistic. On the other hand, justness, arguably the minimal fairness assumption required for the verification of liveness properties, is not preserved by classical semantic equivalences, such as strong bisimilarity. To overcome this deficiency, we introduce a finer alternative to strong bisimilarity, called enabling preserving bisimilarity. We prove that this equivalence is justness-preserving and a congruence for all standard operators, including parallel composition.
   @InProceedings{Hoefner2021-4,
       Author = {van Glabbeek, R.J. and H{\"o}fner, P. and Wang, W.},
       Title = {Enabling Preserving Bisimulation Equivalence},
       BookTitle = {Concurrency Theory (CONCUR 2021)},
       Editor = {},
       Series = {LIPIcs},
       Volume = {203},
       Pages = {33:1-33:20},
       Year = {2021},
       Publisher = {Schloss Dagstuhl -- Leibniz-Zentrum für Informatik},
       Doi = {10.4230/LIPIcs.CONCUR.2021.33}
   }
3. R.J. van Glabbeek, P. Höfner, R. Horne: Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom. In Logic in Computer Science (LICS 2021). pp. 1-13, IEEE, 2021.
   arXiv: CoRR abs/2104.14226 | doi: 10.1109/LICS52264.2021.9470531
   abstract | pdf | bibtex

   Abstract:

   We investigate how different fairness assumptions affect results concerning lock-freedom, a typical liveness property targeted by session type systems. We fix a minimal session calculus and systematically take into account all known fairness assumptions, thereby identifying precisely three interesting and semantically distinct notions of lock-freedom, all of which having a sound session type system. We then show that, by using a general merge operator in an otherwise standard approach to global session types, we obtain a session type system complete for the strongest amongst those notions of lock-freedom, which assumes only justness of execution paths, a minimal fairness assumption for concurrent systems.
   @InProceedings{Hoefner2021-3,
       Author = {van Glabbeek, R.J. and H{\"o}fner, P. and Horne, R.},
       Title = {Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom},
       BookTitle = {Logic in Computer Science (LICS 2021)},
       Editor = {},
       Series = {},
       Volume = {0},
       Pages = {1-13},
       Year = {2021},
       Publisher = {IEEE},
       Doi = {10.1109/LICS52264.2021.9470531}
   }
4. J. Drury, P. Höfner, W. Wang: Formal Models of the OSPF Routing Protocol. In A. Fehnker, H. Garaval (eds.), Models for Formal Analysis of Real Systems (MARS 2020). Electronic Proceedings in Theoretical Computer Science 316, pp. 72-120, Open Publishing Association, 2020.
   doi: 10.4204/EPTCS.316.4
   abstract | pdf | bibtex

   Abstract:

   We present three formal models of the OSPF routing protocol. The first two are formalised in the timed process algebra T-AWN, which is not only tailored for routing protocols, but also specifies protocols in pseudo-code that is easily readable. The difference between the two models lies in the level of detail (level of abstraction). From the more abstract model we then generate the third model. It is based on networks of timed automata and can be executed in the model checker Uppaal.
   @InProceedings{Hoefner2020-2,
       Author = {Drury, J. and H{\"o}fner, P. and Wang, W.},
       Title = {Formal Models of the {OSPF} Routing Protocol},
       BookTitle = {Models for Formal Analysis of Real Systems (MARS 2020)},
       Editor = {Fehnker, A. and Garaval, H.},
       Series = {Electronic Proceedings in Theoretical Computer Science},
       Volume = {316},
       Pages = {72-120},
       Year = {2020},
       Publisher = {Open Publishing Association},
       Doi = {10.4204/EPTCS.316.4}
   }
5. R. Barry, R.J. van Glabbeek, P. Höfner: Formalising the Optimised Link State Routing Protocol. In A. Fehnker, H. Garaval (eds.), Models for Formal Analysis of Real Systems (MARS 2020). Electronic Proceedings in Theoretical Computer Science 316, pp. 40-71, Open Publishing Association, 2020.
   doi: 10.4204/EPTCS.316.3
   abstract | pdf | bibtex

   Abstract:

   Routing protocol specifications are traditionally written in plain English. Often this yields ambiguities, inaccuracies or even contradictions. Formal methods techniques, such as process algebras, avoid these problems, thus leading to more precise and verifiable descriptions of protocols. In this paper we use the timed process algebra T-AWN for modelling the Optimised Link State Routing protocol (OLSR) version 2.
   @InProceedings{Hoefner2020-1,
       Author = {Barry, R. and van Glabbeek, R.J. and H{\"o}fner, P.},
       Title = {Formalising the Optimised Link State Routing Protocol},
       BookTitle = {Models for Formal Analysis of Real Systems (MARS 2020)},
       Editor = {Fehnker, A. and Garaval, H.},
       Series = {Electronic Proceedings in Theoretical Computer Science},
       Volume = {316},
       Pages = {40-71},
       Year = {2020},
       Publisher = {Open Publishing Association},
       Doi = {10.4204/EPTCS.316.3}
   }
6. R.J. van Glabbeek, P. Höfner, M. Markl: A Process Algebra for Link Layer Protocols. In L. Caires (ed.), Programming Languages and Systems (ESOP 2019). Lecture Notes in Computer Science 11423, pp. 668-693, Springer, 2019.
   arXiv: CoRR abs/1907.13329 | doi: 10.1007/978-3-030-17184-1_24
   abstract | pdf | bibtex

   Abstract:

   We propose a process algebra for link layer protocols, featuring a unique mechanism for modelling frame collisions. We also formalise suitable liveness properties for link layer protocols specified in this framework. To show applicability we model and analyse two versions of the Carrier-Sense Multiple Access with Collision Avoidance (CSMA/CA) protocol. Our analysis confirms the hidden station problem for the version without virtual carrier sensing. However, we show that the version with virtual carrier sensing not only overcomes this problem, but also the exposed station problem with probability 1. Yet the protocol cannot guarantee packet delivery, not even with probability 1.
   @InProceedings{Hoefner2019-3,
       Author = {van Glabbeek, R.J. and H{\"o}fner, P. and Markl, M.},
       Title = {A Process Algebra for Link Layer Protocols},
       BookTitle = {Programming Languages and Systems (ESOP 2019)},
       Editor = {Caires, L.},
       Series = {Lecture Notes in Computer Science},
       Volume = {11423},
       Pages = {668-693},
       Year = {2019},
       Publisher = {Springer},
       Doi = {10.1007/978-3-030-17184-1_24}
   }
7. C. Bannister, P. Höfner: False Failure: Creating Failure Models for Separation Logic. In J. Desharnais, W. Guttmann, S. Joosten (eds.), Relational and Algebraic Methods in Computer Science (RAMiCS 2018). Lecture Notes in Computer Science 11194, pp. 263-279, Springer, 2018.
   doi: 10.1007/978-3-030-02149-8_16
   abstract | pdf | bibtex

   Abstract:

   Separation logic, an extension of Floyd-Hoare logic, finds countless applications in areas of program verification, but does not allow forward reasoning in the setting of total or generalised correctness. To support forward reasoning, separation logic needs to be equiped with a failure element. We present several ways on how to add such an element. We show that none of the `obvious' extensions preserve all the algebraic properties desired. We develop more complicated models, satisfying the desired properties, and discuss their use for forward reasoning.
   @InProceedings{Hoefner2018-4,
       Author = {Bannister, C. and H{\"o}fner, P.},
       Title = {False Failure: Creating Failure Models for Separation Logic},
       BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2018)},
       Editor = {Desharnais, J. and Guttmann, W. and Joosten, S.},
       Series = {Lecture Notes in Computer Science},
       Volume = {11194},
       Pages = {263-279},
       Year = {2018},
       Publisher = {Springer},
       Doi = {10.1007/978-3-030-02149-8_16}
   }
8. R.J. van Glabbeek, P. Höfner, D. van der Wal: Analysing AWN-specifications using mCRL2 (extended abstract). In C.A. Furia, K. Winter (eds.), Integrated Formal Methods (iFM 2018). Lecture Notes in Computer Science 11023, pp. 398-418, Springer, 2018.
   doi: 10.1007/978-3-319-98938-9_23
   abstract | pdf | bibtex

   Abstract:

   We develop and implement a translation from the process Algebra for Wireless Networks (AWN) into the milli Common Representation Language (mCRL2). As a consequence of the translation, the sophisticated toolset of mCRL2 is now available for AWN-specifications. We show that the translation respects strong bisimilarity; hence all safety properties can be automatically checked using the toolset. To show usability of our translation we report on a case study.
   @InProceedings{Hoefner2018-3,
       Author = {van Glabbeek, R.J. and H{\"o}fner, P. and van der Wal, D.},
       Title = {Analysing {AWN}-specifications using {mCRL2} (extended abstract)},
       BookTitle = {Integrated Formal Methods (iFM 2018)},
       Editor = {Furia, C.A. and Winter, K.},
       Series = {Lecture Notes in Computer Science},
       Volume = {11023},
       Pages = {398-418},
       Year = {2018},
       Publisher = {Springer},
       Doi = {10.1007/978-3-319-98938-9_23}
   }
9. C. Bannister, P. Höfner, G. Klein: Backwards and Forwards with Separation Logic. In J. Avigad, A. Mahboubi (eds.), Interactive Theorem Proving (ITP 2018). Lecture Notes in Computer Science 10895, pp. 68-87, Springer, 2018.
   doi: 10.1007/978-3-319-94821-8_5
   abstract | pdf | bibtex

   Abstract:

   The use of Hoare logic in combination with weakest preconditions and strongest postconditions is a standard tool for program verification, known as backward and forward reasoning. In this paper we extend these techniques to allow backward and forward reasoning for separation logic. While the former is derived directly from the standard operators of separation logic, the latter uses a new one. We implement our framework in the interactive proof assistant Isabelle/HOL, and enable automation with several interactive proof tactics.
   @InProceedings{Hoefner2018-2,
       Author = {Bannister, C. and H{\"o}fner, P. and Klein, G.},
       Title = {Backwards and Forwards with Separation Logic},
       BookTitle = {Interactive Theorem Proving (ITP 2018)},
       Editor = {Avigad, J. and Mahboubi, A.},
       Series = {Lecture Notes in Computer Science},
       Volume = {10895},
       Pages = {68-87},
       Year = {2018},
       Publisher = {Springer},
       Doi = {10.1007/978-3-319-94821-8_5}
   }
10. V. Dyseryn, R.J. van Glabbeek, P. Höfner: Analysing Mutual Exclusion using Process Algebra with Signals. In K. Peters, T. Tini (eds.), Expressiveness in Concurrency and Structural Operational Semantics (EXPRESS/SOS 2017). Electronic Proceedings in Theoretical Computer Science 255, pp. 18-34, Open Publishing Association, 2017.
    doi: 10.4204/EPTCS.255.2
    abstract | pdf | bibtex

    Abstract:

    In contrast to common belief, the Calculus of Communicating Systems (CCS) and similar process algebras lack the expressive power to accurately capture mutual exclusion protocols without enriching the language with fairness assumptions. Adding a fairness assumption to implement a mutual exclusion protocol seems counter-intuitive. We employ a signalling operator, which can be combined with CCS, or other process calculi, and show that this minimal extension is expressive enough to model mutual exclusion: we confirm the correctness of Peterson's mutual exclusion algorithm for two processes, as well as Lamport's bakery algorithm, under reasonable assumptions on the underlying memory model. The correctness of Peterson's algorithm for more than two processes requires stronger, less realistic assumptions on the underlying memory model.
    @InProceedings{Hoefner2017-6,
        Author = {Dyseryn, V. and van Glabbeek, R.J. and H{\"o}fner, P.},
        Title = {Analysing Mutual Exclusion using Process Algebra with Signals},
        BookTitle = {Expressiveness in Concurrency and Structural Operational Semantics (EXPRESS/SOS 2017)},
        Editor = {Peters, K. and Tini, T.},
        Series = {Electronic Proceedings in Theoretical Computer Science},
        Volume = {255},
        Pages = {18-34},
        Year = {2017},
        Publisher = {Open Publishing Association},
        Doi = {10.4204/EPTCS.255.2}
    }
11. R.J. van Glabbeek, P. Höfner: Split, Send, Reassemble: A Formal Specification of a CAN Bus Protocol Stack. In Models for Formal Analysis of Real Systems (MARS 2017). Electronic Proceedings in Theoretical Computer Science 244, pp. 14-52, Open Publishing Association, 2017.
    doi: 10.4204/EPTCS.244.2
    abstract | pdf | bibtex

    Abstract:

    We present a formal model for a fragmentation and a reassembly protocol running on top of the standardised CAN bus, which is widely used in automotive and aerospace applications. Although the CAN bus comes with an in-built mechanism for prioritisation, we argue that this is not sufficient and provide another protocol to overcome this shortcoming.
    @InProceedings{Hoefner2017-3,
        Author = {van Glabbeek, R.J. and H{\"o}fner, P.},
        Title = {Split, Send, Reassemble: A Formal Specification of a {CAN} Bus Protocol Stack},
        BookTitle = {Models for Formal Analysis of Real Systems (MARS 2017)},
        Editor = {},
        Series = {Electronic Proceedings in Theoretical Computer Science},
        Volume = {244},
        Pages = {14-52},
        Year = {2017},
        Publisher = {Open Publishing Association},
        Doi = {10.4204/EPTCS.244.2}
    }
12. E. Bres, R.J. van Glabbeek, P. Höfner: A Timed Process Algebra for Wireless Networks with an Application in Routing (Extended Abstract). In Programming Languages and Systems (ESOP 2016). Lecture Notes in Computer Science 9632, pp. 95-122, Springer, 2016.
    doi: 10.1007/978-3-662-49498-1_5
    abstract | pdf | bibtex

    Abstract:

    This paper proposes a timed process algebra for wireless networks, an extension of the Algebra for Wireless Networks. It combines treatments of local broadcast, conditional unicast and data structures, which are essential features for the modelling of network protocols. In this framework we model and analyse the Ad hoc On-Demand Distance Vector routing protocol, and show that, contrary to claims in the literature, it fails to be loop free. We also present boundary conditions for a fix ensuring that the resulting protocol is indeed loop free.
    @InProceedings{Hoefner2016-7,
        Author = {Bres, E. and van Glabbeek, R.J. and H{\"o}fner, P.},
        Title = {A Timed Process Algebra for Wireless Networks with an Application in Routing (Extended Abstract)},
        BookTitle = {Programming Languages and Systems (ESOP 2016)},
        Editor = {},
        Series = {Lecture Notes in Computer Science},
        Volume = {9632},
        Pages = {95-122},
        Year = {2016},
        Publisher = {Springer},
        Doi = {10.1007/978-3-662-49498-1_5}
    }
13. P. Höfner: Using Process Algebra to Design Better Protocol (extended abstract); invited. In Forum "Math-for-Industry" 2015 - The Role and Importance of Mathematics in Innovation (FMI 2015). MI Lecture Notes 65, Kyushu University, 2015.
    pdf | bibtex

    Abstract:

    @InProceedings{Hoefner2015-8,
        Author = {H{\"o}fner, P.},
        Title = {Using Process Algebra to Design Better Protocol (extended abstract); invited},
        BookTitle = {Forum "Math-for-Industry" 2015 - The Role and Importance of Mathematics in Innovation (FMI 2015)},
        Editor = {},
        Series = {MI Lecture Notes},
        Volume = {65},
        Pages = {-},
        Year = {2015},
        Publisher = {Kyushu University},
        Doi = {}
    }
14. R. Berghammer, P. Höfner, I. Stucke: Tool-Based Verification of a Relational Vertex Coloring Program. In W. Kahl, J.N. Oliveira, M. Winter (eds.), Relational and Algebraic Methods in Computer Science (RAMiCS 2015). Lecture Notes in Computer Science 9348, pp. 275-292, Springer, 2015.
    doi: 10.1007/978-3-319-24704-5_17
    abstract | pdf | bibtex

    Abstract:

    We present different approaches of using a special purpose computer algebra system and theorem provers in software verification. To this end, we first develop a purely algebraic while-program for computing a vertex coloring of an undirected (loop-free) graph. For showing its correctness, we then combine the well-known assertion-based verification method with relation-algebraic calculations. Based on this, we show how automatically to test loop-invariants by means of the RelView tool and also compare the usage of three different theorem provers in respect to the verification of the proof obligations: the automated theorem prover Prover9 and the two proof assistants Coq and Isabelle/HOL. As a result, we illustrate that algebraic abstraction yields verification tasks that can easily be verified with off-the-shelf theorem provers, but also reveal some shortcomings and difficulties with theorem provers that are nowadays available.
    @InProceedings{Hoefner2015-6,
        Author = {Berghammer, R. and H{\"o}fner, P. and Stucke, I.},
        Title = {Tool-Based Verification of a Relational Vertex Coloring Program},
        BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2015)},
        Editor = {Kahl, W. and Oliveira, J.N. and Winter, M.},
        Series = {Lecture Notes in Computer Science},
        Volume = {9348},
        Pages = {275-292},
        Year = {2015},
        Publisher = {Springer},
        Doi = {10.1007/978-3-319-24704-5_17}
    }
15. M. Kamali, P. Höfner, M. Kamali, L. Petre: Formal Analysis of Proactive, Distributed Routing. In R. Calinescu, B. Rumpe (eds.), Software Engineering and Formal Methods (SEFM 2015). Lecture Notes in Computer Science 9276, pp. 175-189, Springer, 2015.
    doi: 10.1007/978-3-319-22969-0_13
    abstract | pdf | bibtex

    Abstract:

    As (network) software is such an omnipresent component of contemporary mission-critical systems, formal analysis is required to provide the necessary certification or at least assurance for these systems. In this paper we focus on modelling and analysing the Optimised Link State Routing (OLSR) protocol, a distributed, proactive routing protocol. It is recognised as one of the standard ad-hoc routing protocols for Wireless Mesh Networks (WMN). WMNs are instrumental in critical systems, such as emergency response networks and smart electrical grids. We use the model checker Uppaal for analysing safety properties of OLSR as well as to point out a case of OLSR malfunctioning.
    @InProceedings{Hoefner2015-5,
        Author = {Kamali, M. and H{\"o}fner, P. and Kamali, M. and Petre, L.},
        Title = {Formal Analysis of Proactive, Distributed Routing},
        BookTitle = {Software Engineering and Formal Methods (SEFM 2015)},
        Editor = {Calinescu, R. and Rumpe, B.},
        Series = {Lecture Notes in Computer Science},
        Volume = {9276},
        Pages = {175-189},
        Year = {2015},
        Publisher = {Springer},
        Doi = {10.1007/978-3-319-22969-0_13}
    }
16. T. Bourke, R.J. van Glabbeek, P. Höfner: A Mechanized Proof of Loop Freedom of the (Untimed) {AODV} Routing Protocol. In F. Cassez, J.-F. Raskin (eds.), Automated Technology for Verification and Analysis (ATVA 2014). Lecture Notes in Computer Science 8837, pp. 47-63, Springer, 2014.
    arXiv: CoRR abs/1505.05646 | doi: 10.1007/978-3-319-11936-6_5
    abstract | pdf | bibtex

    Abstract:

    The Ad hoc On-demand Distance Vector (AODV) routing protocol allows the nodes in a Mobile Ad hoc Network (MANET) or a Wireless Mesh Network (WMN) to know where to forward data packets. Such a protocol is `loop free' if it never leads to routing decisions that forward packets in circles. This paper describes the mechanization of an existing pen-and-paper proof of loop freedom of AODV in the interactive theorem prover Isabelle/HOL. The mechanization relies on a novel compositional approach for lifting invariants to networks of nodes. We exploit the mechanization to analyse several improvements of AODV and show that Isabelle/HOL can re-establish most proof obligations automatically and identify exactly the steps that are no longer valid.
    @InProceedings{Hoefner2014-5,
        Author = {Bourke, T. and van Glabbeek, R.J. and H{\"o}fner, P.},
        Title = {A Mechanized Proof of Loop Freedom of the (Untimed) {AODV} Routing Protocol},
        BookTitle = {Automated Technology for Verification and Analysis (ATVA 2014)},
        Editor = {Cassez, F. and Raskin, J.-F.},
        Series = {Lecture Notes in Computer Science},
        Volume = {8837},
        Pages = {47-63},
        Year = {2014},
        Publisher = {Springer},
        Doi = {10.1007/978-3-319-11936-6_5}
    }
17. T. Bourke, R.J. van Glabbeek, P. Höfner: Showing Invariance Compositionally for a Process Algebra of Network Protocols. In G. Klein, R. Gamboa (eds.), Interactive Theorem Proving (ITP 2014). Lecture Notes in Computer Science 8558, pp. 144-159, Springer, 2014.
    arXiv: CoRR abs/1407.3519 | doi: 10.1007/978-3-319-08970-6_10
    abstract | pdf | bibtex

    Abstract:

    This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invariant properties. Mechanizing the core process algebra in Isabelle/HOL is relatively standard, but its layered structure necessitates special treatment. The control states of reactive processes, for example nodes of a network, are modelled by terms of the process algebra. We propose a technique based on these terms to streamline proofs of inductive invariance. This is not sufficient, however, to state and prove invariants that relate states across multiple processes (entire networks). We propose a novel compositional technique for lifting properties from local states (individual nodes) to global states (networks of nodes).
    @InProceedings{Hoefner2014-3,
        Author = {Bourke, T. and van Glabbeek, R.J. and H{\"o}fner, P.},
        Title = {Showing Invariance Compositionally for a Process Algebra of Network Protocols},
        BookTitle = {Interactive Theorem Proving (ITP 2014)},
        Editor = {Klein, G. and Gamboa, R.},
        Series = {Lecture Notes in Computer Science},
        Volume = {8558},
        Pages = {144-159},
        Year = {2014},
        Publisher = {Springer},
        Doi = {10.1007/978-3-319-08970-6_10}
    }
18. R. Berghammer, P. Höfner, I. Stucke: Automated Verification of Relational While-Programs. In P. Höfner, P. Jipsen, W. Kahl, M.E. Müller (eds.), Relational and Algebraic Methods in Computer Science (RAMiCS 2014). Lecture Notes in Computer Science 8428, pp. 173-190, Springer, 2014.
    doi: 10.1007/978-3-319-06251-8_11
    abstract | pdf | bibtex

    Abstract:

    Software verification is essential for safety-critical systems. In this paper, we illustrate that some verification tasks can be done fully automatically. We show how to automatically verify imperative programs for relation-based discrete structures by combining relation algebra and the well-known assertion-based verification method with automated theorem proving. We present two examples in detail: a relational program for determining the reflexive-transitive closure and a topological sorting algorithm. We also treat the automatic verification of the equivalence of common-logical and relation-algebraic specifications.
    @InProceedings{Hoefner2014-1,
        Author = {Berghammer, R. and H{\"o}fner, P. and Stucke, I.},
        Title = {Automated Verification of Relational While-Programs},
        BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2014)},
        Editor = {H{\"o}fner, P. and Jipsen, P. and Kahl, W. and M{\"u}ller, M.E.},
        Series = {Lecture Notes in Computer Science},
        Volume = {8428},
        Pages = {173-190},
        Year = {2014},
        Publisher = {Springer},
        Doi = {10.1007/978-3-319-06251-8_11}
    }
19. D. Batory, P. Höfner, B. Möller, A. Zelend: Features, Modularity, and Variation Points. In Workshop on Feature-Oriented Software Development (FOSD 2013). pp. 9-16, ACM, 2013.
    doi: 10.1145/2528265.2528269
    abstract | pdf | bibtex

    Abstract:

    A feature interaction algebra (FIA) is an abstract model of features, feature interactions, and their compositions. A structured document algebra (SDA) defines modules with variation points and how such modules compose. We present both FIA and SDA in this paper, and homomorphisms that relate FIA expressions to SDA expressions. This leads to mathematically precise formalizations of fundamental concepts used in software product lines, which can be used for improved FOSD tooling and teaching material.
    @InProceedings{Hoefner2013-6,
        Author = {Batory, D. and H{\"o}fner, P. and M{\"o}ller, B. and Zelend, A.},
        Title = {Features, Modularity, and Variation Points},
        BookTitle = {Workshop on Feature-Oriented Software Development (FOSD 2013)},
        Editor = {},
        Series = {},
        Volume = {0},
        Pages = {9-16},
        Year = {2013},
        Publisher = {ACM},
        Doi = {10.1145/2528265.2528269}
    }
20. R.J. van Glabbeek, P. Höfner, M. Portmann, W.L. Tan: Sequence Numbers Do Not Guarantee Loop Freedom —AODV Can Yield Routing Loops—. In Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM 2013). pp. 91-100, ACM, 2013.
    arXiv: CoRR abs/1512.08891 | doi: 10.1145/2507924.2507943
    abstract | pdf | bibtex

    Abstract:

    In the area of mobile ad-hoc networks and wireless mesh networks, sequence numbers are often used in routing protocols to avoid routing loops. It is commonly stated in protocol specifications that sequence numbers are sufficient to guarantee loop freedom if they are monotonically increased over time. A classical example for the use of sequence numbers is the popular Ad hoc On-Demand Distance Vector (AODV) routing protocol. The loop freedom of AODV is not only a common belief, it has been claimed in the abstract of its RFC and at least two proofs have been proposed. AODV-based protocols such as AODVv2 (DYMO) and HWMP also claim loop freedom due to the same use of sequence numbers.
    In this paper we show that AODV is not a priori loop free; by this we counter the proposed proofs in the literature. In fact, loop freedom hinges on non-evident assumptions to be made when resolving ambiguities occurring in the RFC. Thus, monotonically increasing sequence numbers, by themselves, do not guarantee loop freedom.
    @InProceedings{Hoefner2013-5,
        Author = {van Glabbeek, R.J. and H{\"o}fner, P. and Portmann, M. and Tan, W.L.},
        Title = {Sequence Numbers Do Not Guarantee Loop Freedom ---AODV Can Yield Routing Loops---},
        BookTitle = {Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM 2013)},
        Editor = {},
        Series = {},
        Volume = {0},
        Pages = {91-100},
        Year = {2013},
        Publisher = {ACM},
        Doi = {10.1145/2507924.2507943}
    }
21. A. Fehnker, P. Höfner, M. Kamali, V. Mehta: Topology-based Mobility Models for Wireless Networks. In L. Alvisi, D. Giannakopoulou (eds.), Quantitative Evaluation of Systems (QEST 2013). Lecture Notes in Computer Science 8054, pp. 368-383, Springer, 2013.
    doi: 10.1007/978-3-642-40196-1_32
    abstract | pdf | bibtex

    Abstract:

    The performance and reliability of wireless network protocols heavily depend on the network and its environment. In wireless networks node mobility can affect the overall performance up to a point where, e.g. route discovery and route establishment fail. As a consequence any formal technique for performance analysis of wireless network protocols should take node mobility into account. In this paper we propose a topology-based mobility model, that abstracts from physical behaviour, and models mobility as probabilistic changes in the topology. We demonstrate how this model can be instantiated to cover the main aspects of the random walk and the random waypoint mobility model. The model is not a stand-alone model, but intended to be used in combination with protocol models. We illustrate this by two application examples: first we show a brief analysis of the Ad-hoc On demand Distance Vector (AODV) routing protocol, and second we combine the mobility model with the Lightweight Medium Access Control (LMAC).
    @InProceedings{Hoefner2013-3,
        Author = {Fehnker, A. and H{\"o}fner, P. and Kamali, M. and Mehta, V.},
        Title = {Topology-based Mobility Models for Wireless Networks},
        BookTitle = {Quantitative Evaluation of Systems (QEST 2013)},
        Editor = {Alvisi, L. and Giannakopoulou, D.},
        Series = {Lecture Notes in Computer Science},
        Volume = {8054},
        Pages = {368-383},
        Year = {2013},
        Publisher = {Springer},
        Doi = {10.1007/978-3-642-40196-1_32}
    }
22. P. Höfner, M. Kamali: Quantitative Analysis of AODV and its Variants on Dynamic Topologies using Statistical Model Checking. In V. Braberman, L. Fribourg (eds.), Formal Modelling and Analysis of Timed Systems (FORMATS 2013). Lecture Notes in Computer Science 8053, pp. 121-136, Springer, 2013.
    doi: 10.1007/978-3-642-40229-6_9
    abstract | pdf | bibtex

    Abstract:

    Wireless Mesh Networks (WMNs) are self-organising ad-hoc networks that support broadband communication. Due to changes in the topology, route discovery and maintenance play a crucial role in the reliability and the performance of such networks. Formal analysis of WMNs using exhaustive model checking techniques is often not feasible: network size (up to hundreds of nodes) and topology changes yield state- space explosion. Statistical Model Checking, however, can overcome this problem and allows a quantitative analysis.
    In this paper we illustrate this by a careful analysis of the Ad hoc On- demand Distance Vector (AODV) protocol. We show that some optional features of AODV are not useful, and that AODV shows unexpected behaviour, yielding a high probability of route discovery failure.
    @InProceedings{Hoefner2013-4,
        Author = {H{\"o}fner, P. and Kamali, M.},
        Title = {Quantitative Analysis of {AODV} and its Variants on Dynamic Topologies using Statistical Model Checking},
        BookTitle = {Formal Modelling and Analysis of Timed Systems (FORMATS 2013)},
        Editor = {Braberman, V. and Fribourg, L.},
        Series = {Lecture Notes in Computer Science},
        Volume = {8053},
        Pages = {121-136},
        Year = {2013},
        Publisher = {Springer},
        Doi = {10.1007/978-3-642-40229-6_9}
    }
23. P. Höfner, A. McIver: Statistical Model Checking of Wireless Mesh Routing Protocols. In G. Brat, N. Rungta, A. Venet (eds.), NASA Formal Methods Symposium (NFM 2013). Lecture Notes in Computer Science 7871, pp. 322-336, Springer, 2013.
    doi: 10.1007/978-3-642-38088-4_22
    abstract | pdf | bibtex

    Abstract:

    Several case studies indicate that model checking is limited in the analysis of mesh networks: state space explosion restricts applicability to at most 10 node networks, and quantitative reasoning, often sufficient for network evaluation, is not possible. Both deficiencies can be overcome to some extent by the use of statistical model checkers, such as SMC-Uppaal. In this paper we illustrate this by a quantitative analysis of two well-known routing protocols for wireless mesh networks, namely AODV and DYMO. Moreover, we push the limits and show that this technology is capable of analysing networks of up to 100 nodes.
    @InProceedings{Hoefner2013-2,
        Author = {H{\"o}fner, P. and McIver, A.},
        Title = {Statistical Model Checking of Wireless Mesh Routing Protocols},
        BookTitle = {NASA Formal Methods Symposium (NFM 2013)},
        Editor = {Brat, G. and Rungta, N. and Venet, A.},
        Series = {Lecture Notes in Computer Science},
        Volume = {7871},
        Pages = {322-336},
        Year = {2013},
        Publisher = {Springer},
        Doi = {10.1007/978-3-642-38088-4_22}
    }
24. S. Edenhofer, P. Höfner: Towards a Rigorous Analysis of AODVv2 (DYMO). In N. Foster, A. Gurney (eds.), Rigorous Protocol Engineering (WRiPE 2012). IEEE, 2012.
    doi: 10.1109/ICNP.2012.6459942
    abstract | pdf | bibtex

    Abstract:

    Dynamic MANET On-demand (AODVv2) routing, formerly known as DYMO, is a routing protocol especially designed for wireless, multi hop networks. AODVv2 determines routes in a network in an on-demand fashion.
    In this paper we present a formal model of AODVv2, using the process algebra AWN. The benefit of this is two-fold: (a) the given specification is definitely free of ambiguities; (b) a formal and rigorous analysis of the routing protocol is now feasible. To underpin the latter point we also present a first analysis of the AODVv2 routing protocol. On the one hand we show that some of the problems discovered in the AODV routing protocol, the predecessor of AODVv2, have been addressed and solved. On the other hand we show that other limitations still exist; an example is the establishment of non-optimal routes. Even worse, we locate shortcomings in the AODVv2 routing protocol that do not occur in AODV. This yields the conclusion that AODVv2 is not necessarily better than AODV.
    @InProceedings{Hoefner2012-5,
        Author = {Edenhofer, S. and H{\"o}fner, P.},
        Title = {Towards a Rigorous Analysis of {AODVv2} ({DYMO})},
        BookTitle = {Rigorous Protocol Engineering (WRiPE 2012)},
        Editor = {Foster, N. and Gurney, A.},
        Series = {},
        Volume = {0},
        Pages = {-},
        Year = {2012},
        Publisher = {IEEE},
        Doi = {10.1109/ICNP.2012.6459942}
    }
25. P. Höfner, R.J. van Glabbeek, W.L. Tan, M. Portmann, A. McIver, A. Fehnker: A Rigorous Analysis of AODV and its Variants. In Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM 2012). pp. 203-212, ACM, 2012. (nominated for best paper award)
    arXiv: CoRR abs/1512.08873 | doi: 10.1145/2387238.2387274
    abstract | pdf | bibtex

    Abstract:

    In this paper we present a rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol using a formal specification in AWN (Algebra for Wireless Net- works), a process algebra which has been specifically tailored for the modelling of Mobile Ad Hoc Networks and Wireless Mesh Network protocols. Our formalisation models the exact details of the core functionality of AODV, such as route discovery, route maintenance and error handling. We demonstrate how AWN can be used to reason about critical protocol correctness properties by providing a detailed proof of loop freedom. In contrast to evaluations using simulation or other formal methods such as model checking, our proof is generic and holds for any possible network scenario in terms of network topology, node mobility, traffic pattern, etc. A key contribution of this paper is the demonstration of how the reasoning and proofs can relatively easily be adapted to protocol variants.
    @InProceedings{Hoefner2012-7,
        Author = {H{\"o}fner, P. and van Glabbeek, R.J. and Tan, W.L. and Portmann, M. and McIver, A. and Fehnker, A.},
        Title = {A Rigorous Analysis of {AODV} and its Variants},
        BookTitle = {Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM 2012)},
        Editor = {},
        Series = {},
        Volume = {0},
        Pages = {203-212},
        Year = {2012},
        Publisher = {ACM},
        Doi = {10.1145/2387238.2387274}
    }
26. P. Höfner, B. Möller, A. Zelend: Foundations of Coloring Algebra with Consequences for Feature-oriented Programming. In W. Kahl, T. Griffin (eds.), Relational and Algebraic Methods in Computer Science (RAMiCS 2012). Lecture Notes in Computer Science 7560, pp. 33-49, Springer, 2012.
    doi: 10.1007/978-3-642-33314-9_3
    abstract | pdf | bibtex

    Abstract:

    In 2011, simple and concise axioms for feature compositions, interactions and products have been proposed by Batory et al. They were mainly inspired by Kästner's Colored IDE (CIDE) as well as by experience in feature oriented programming over the last decades. However, so far only axioms were proposed; consequences of these axioms such as variability in models have not been studied. In this paper we discuss the proposed axioms from a theoretical point of view, which yields a much better understanding of the proposed algebra and therefore of feature oriented programming. For example, we show that the axioms characterising feature composition are isomorphic to set-theoretic models.
    @InProceedings{Hoefner2012-6,
        Author = {H{\"o}fner, P. and M{\"o}ller, B. and Zelend, A.},
        Title = {Foundations of Coloring Algebra with Consequences for Feature-oriented Programming},
        BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2012)},
        Editor = {Kahl, W. and Griffin, T.},
        Series = {Lecture Notes in Computer Science},
        Volume = {7560},
        Pages = {33-49},
        Year = {2012},
        Publisher = {Springer},
        Doi = {10.1007/978-3-642-33314-9_3}
    }
27. A. Fehnker, R.J. van Glabbeek, P. Höfner, A. McIver, M. Portmann, W.L. Tan: A Process Algebra for Wireless Mesh Networks. In H. Seidl (ed.), Programming Languages and Systems (ESOP'12) (ESOP 2012). Lecture Notes in Computer Science 7211, pp. 295-315, Springer, 2012.
    doi: 10.1007/978-3-642-28869-2_15
    abstract | pdf | bibtex

    Abstract:

    We propose a process algebra for wireless mesh networks that combines novel treatments of local broadcast, conditional unicast and data structures. In this framework, we model the Ad-hoc On-Demand Distance Vector (AODV) routing protocol and (dis)prove crucial properties such as loop freedom and packet delivery.
    @InProceedings{Hoefner2012-2,
        Author = {Fehnker, A. and van Glabbeek, R.J. and H{\"o}fner, P. and McIver, A. and Portmann, M. and Tan, W.L.},
        Title = {A Process Algebra for Wireless Mesh Networks},
        BookTitle = {Programming Languages and Systems (ESOP'12) (ESOP 2012)},
        Editor = {Seidl, H.},
        Series = {Lecture Notes in Computer Science},
        Volume = {7211},
        Pages = {295-315},
        Year = {2012},
        Publisher = {Springer},
        Doi = {10.1007/978-3-642-28869-2_15}
    }
28. A. Fehnker, R.J. van Glabbeek, P. Höfner, A. McIver, M. Portmann, W.L. Tan: Automated Analysis of AODV using UPPAAL. In C. Flanagan, B. König (eds.), Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012). Lecture Notes in Computer Science 7214, pp. 173-187, Springer, 2012.
    arXiv: CoRR abs/1512.07352 | doi: 10.1007/978-3-642-28756-5_13
    abstract | pdf | bibtex

    Abstract:

    This paper describes an automated, formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in wireless mesh networks.
    We give a brief overview of a model of AODV implemented in the UPPAAL model checker. It is derived from a process-algebraic model which reflects precisely the intention of AODV and accurately captures the protocol specification. Furthermore, we describe experiments carried out to explore AODV's behaviour in all network topologies up to 5 nodes. We were able to automatically locate problematic and undesirable behaviours. This is in particular useful to discover protocol limitations and to develop improved variants. This use of model checking as a diagnostic tool complements other formal-methods-based protocol modelling and verification techniques, such as process algebra.
    @InProceedings{Hoefner2012-1,
        Author = {Fehnker, A. and van Glabbeek, R.J. and H{\"o}fner, P. and McIver, A. and Portmann, M. and Tan, W.L.},
        Title = {Automated Analysis of AODV using UPPAAL},
        BookTitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012)},
        Editor = {Flanagan, C. and K{\"o}nig, B.},
        Series = {Lecture Notes in Computer Science},
        Volume = {7214},
        Pages = {173-187},
        Year = {2012},
        Publisher = {Springer},
        Doi = {10.1007/978-3-642-28756-5_13}
    }
29. D. Batory, P. Höfner, J. Kim: Feature Interactions, Products, and Composition. In Generative Programming and Component Engineering (GPCE 2011). pp. 13-22, ACM, 2011.
    doi: 10.1145/2047862.2047867
    abstract | pdf | bibtex

    Abstract:

    The relationship between feature modules and feature interactions is not well-understood. To explain classic examples of feature interaction, we show that features are not only composed sequentially, but also by cross-product and interaction operations that heretofore were implicit in the literature. Using the Colored IDE (CIDE) tool as our starting point, we (a) present a formal model of these operations, (b) show how it connects and explains previously unrelated results in Feature Oriented Software Development (FOSD), and (c) describe a tool, based on our formalism, that demonstrates how changes in composed documents can be back-propagated to their original feature module definitions, thereby improving FOSD tooling.
    @InProceedings{Hoefner2011-8,
        Author = {Batory, D. and H{\"o}fner, P. and Kim, J.},
        Title = {Feature Interactions, Products, and Composition},
        BookTitle = {Generative Programming and Component Engineering (GPCE 2011)},
        Editor = {},
        Series = {},
        Volume = {0},
        Pages = {13-22},
        Year = {2011},
        Publisher = {ACM},
        Doi = {10.1145/2047862.2047867}
    }
30. A. Fehnker, R.J. van Glabbeek, P. Höfner, A. McIver, M. Portmann, W.L. Tan: Modelling and Analysis of AODV in UPPAAL. In Rigorous Protocol Engineering (WRiPE'11) (WRiPE 2011). 2011.
    abstract | pdf | bibtex

    Abstract:

    This paper describes work in progress towards an automated formal and rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol, a popular protocol used in ad hoc wireless networks.
    We give a brief overview of a model of AODV implemented in the UPPAAL model checker, and describe experiments carried out to explore AODV's behaviour in two network topologies. We were able to locate automatically and confirm some known problematic and undesirable behaviours. We believe this use of model checking as a diagnostic tool complements other formal methods based protocol modelling and verification techniques, such as process algebras. Model checking is in particular useful for the discovery of protocol limitations and in the development of improved variations.
    @InProceedings{Hoefner2011-7,
        Author = {Fehnker, A. and van Glabbeek, R.J. and H{\"o}fner, P. and McIver, A. and Portmann, M. and Tan, W.L.},
        Title = {Modelling and Analysis of {AODV} in {UPPAAL}},
        BookTitle = {Rigorous Protocol Engineering (WRiPE'11) (WRiPE 2011)},
        Editor = {},
        Series = {},
        Volume = {0},
        Pages = {-},
        Year = {2011},
        Publisher = {},
        Doi = {}
    }
31. P. Höfner, A. McIver: Towards an Algebra of Routing Tables. In H. de Swart (ed.), Relational and Algebraic Methods in Computer Science (RAMiCS 2011). Lecture Notes in Computer Science 6663, pp. 212-229, Springer, 2011.
    doi: 10.1007/978-3-642-21070-9_17
    abstract | pdf | bibtex

    Abstract:

    We use well-known algebraic concepts like semirings and matrices to model and argue about Wireless Mesh Networks. These networks are used in a wide range of application areas, including public safety and transportation. Formal reasoning therefore seems to be necessary to guarantee safety and security. In this paper, we model a simplified algebraic version of the AODV protocol and provide some basic properties. For example we show that each node knows a route to the originator of a message (if there is one).
    @InProceedings{Hoefner2011-5,
        Author = {H{\"o}fner, P. and McIver, A.},
        Title = {Towards an Algebra of Routing Tables},
        BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2011)},
        Editor = {de Swart, H.},
        Series = {Lecture Notes in Computer Science},
        Volume = {6663},
        Pages = {212-229},
        Year = {2011},
        Publisher = {Springer},
        Doi = {10.1007/978-3-642-21070-9_17}
    }
32. H.H. Dang, P. Höfner: Variable Side Conditions and Greatest Relations in Algebraic Separation Logic. In H. de Swart (ed.), Relational and Algebraic Methods in Computer Science (RAMiCS 2011). Lecture Notes in Computer Science 6663, pp. 125-140, Springer, 2011.
    doi: 10.1007/978-3-642-21070-9_11
    abstract | pdf | bibtex

    Abstract:

    When reasoning within separation logic, it is often necessary to provide side conditions for inference rules. These side conditions usually contain information about variables and their use, and are given within a meta-language, i.e., the side conditions cannot be encoded in separation logic itself. In this paper we discuss different possibilities how side conditions of variables—occurring e.g. in the ordinary or the hypothetical frame rule—can be characterised using algebraic separation logic. We also study greatest relations; a concept used in the soundness proof of the hypothetical frame rule. We provide one and only one level of abstraction for the logic, the side conditions and the greatest relations.
    @InProceedings{Hoefner2011-4,
        Author = {Dang, H.H. and H{\"o}fner, P.},
        Title = {Variable Side Conditions and Greatest Relations in Algebraic Separation Logic},
        BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 2011)},
        Editor = {de Swart, H.},
        Series = {Lecture Notes in Computer Science},
        Volume = {6663},
        Pages = {125-140},
        Year = {2011},
        Publisher = {Springer},
        Doi = {10.1007/978-3-642-21070-9_11}
    }
33. H.H. Dang, P. Höfner: Automated Higher-order Reasoning about Quantales. In B. Konev, R.A. Schmidt, S. Schulz (eds.), Workshop on Practical Aspects of Automated Reasoning (PAAR'10) (PAAR 2010"pages: "40-51). EasyChair Proceedings in Computing 9, EasyChair, 2010.
    abstract | pdf | bibtex

    Abstract:

    Originally developed as an algebraic characterisation for quantum mechanics, the al- gebraic structure of quantales nowadays finds widespread applications ranging from (non- commutative) logics to hybrid systems. We present an approach to bring reasoning about quantales into the realm of (fully) automated theorem proving. This will yield automation in various (new) fields of applications in the future. To achieve this goal and to receive a general approach (independent of any particular theorem prover), we use the TPTP Prob- lem Library for higher-order logic. In particular, we give an encoding of quantales in the typed higher-order form (THF) and present some theorems about quantales which can be proved fully automatically. We further present prospective applications for our approach and discuss practical experiences using THF.
    @InProceedings{Hoefner2010-2,
        Author = {Dang, H.H. and H{\"o}fner, P.},
        Title = {Automated Higher-order Reasoning about Quantales},
        BookTitle = {Workshop on Practical Aspects of Automated Reasoning (PAAR'10) (PAAR 2010"pages: "40-51)},
        Editor = {Konev, B. and Schmidt, R.A. and Schulz, S.},
        Series = {EasyChair Proceedings in Computing},
        Volume = {9},
        Pages = {-},
        Year = {2010},
        Publisher = {EasyChair},
        Doi = {}
    }
34. P. Höfner, B. Möller: An Extension of Feature Algebra [Extended Abstract]. In S. Apel, W.R. Cook, K. Czarnecki, C. Kästner, N. Loughran, O. Nierstrasz (eds.), Workshop on Feature-Oriented Software Development (FOSD'09). pp. 75-80, ACM, 2009.
    doi: 10.1145/1629716.1629731
    abstract | pdf | bibtex

    Abstract:

    Feature algebra was introduced as an abstract framework for feature oriented software development. One goal is to pro- vide a common, clearly defined basis for the key ideas of feature orientation. We first present concrete models for the original axioms of feature algebra which represent the main features of feature oriented programs. However, these mod- els show that the axioms of the feature algebra do not reflect some aspects of feature orientation properly. Hence we modify the axioms and introduce the concept of an extended feature algebra. Since the extension is also a generalisation, the original algebra can be retrieved by a single additional axiom. Last but not least we introduce more operators to cover concepts like overriding in the abstract setting.
    @InProceedings{Hoefner2009-4,
        Author = {H{\"o}fner, P. and M{\"o}ller, B.},
        Title = {An Extension of Feature Algebra [Extended Abstract]},
        BookTitle = {Workshop on Feature-Oriented Software Development (FOSD'09)},
        Editor = {Apel, S. and Cook, W.R. and Czarnecki, K. and K{\"a}stner, C. and Loughran, N. and Nierstrasz, O.},
        Series = {},
        Volume = {0},
        Pages = {75-80},
        Year = {2009},
        Publisher = {ACM},
        Doi = {10.1145/1629716.1629731}
    }
35. H.H. Dang, P. Höfner, B. Möller: Towards Algebraic Separation Logic. In R. Berghammer, A.M Jaoua, B. Möller (eds.), Relations and Kleene Algebra in Computer Science (RelmiCS/AKA'09). Lecture Notes in Computer Science 5827, pp. 59-72, Springer, 2009.
    doi: 10.1007/978-3-642-04639-1_5
    abstract | pdf | bibtex

    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.
    @InProceedings{Hoefner2009-3,
        Author = {Dang, H.H. and H{\"o}fner, P. and M{\"o}ller, B.},
        Title = {Towards Algebraic Separation Logic},
        BookTitle = {Relations and Kleene Algebra in Computer Science (RelmiCS/AKA'09)},
        Editor = {Berghammer, R. and Jaoua, A.M and M{\"o}ller, B.},
        Series = {Lecture Notes in Computer Science},
        Volume = {5827},
        Pages = {59-72},
        Year = {2009},
        Publisher = {Springer},
        Doi = {10.1007/978-3-642-04639-1_5}
    }
36. P. Höfner, R. Khedri, B. Möller: Algebraic View Reconciliation. In A. Cerone, S. Gruner (eds.), Software Engineering and Formal Methods (SEFM'08). pp. 85-94, IEEE, 2008.
    doi: 10.1109/SEFM.2008.36
    abstract | pdf | bibtex

    Abstract:

    Embedded systems such as automotive systems are very complex to specify. Since it is difficult to capture all their requirements or their design in one single model, approaches working with several system views are adopted. The main problem there is to keep these views coherent; the issue is known as view reconciliation. This paper proposes an algebraic solution. It uses sets of integration constraints that link (families of) system features in one view to other (families of) features in the same or a different view. Both, families and constraints, are formalised using a feature algebra. Besides presenting a constraint relation and its mathematical properties, the paper shows in several examples the suitability of this approach for a wide class of integration constraint formulations.
    @InProceedings{Hoefner2008-7,
        Author = {H{\"o}fner, P. and Khedri, R. and M{\"o}ller, B.},
        Title = {Algebraic View Reconciliation},
        BookTitle = {Software Engineering and Formal Methods (SEFM'08)},
        Editor = {Cerone, A. and Gruner, S.},
        Series = {},
        Volume = {0},
        Pages = {85-94},
        Year = {2008},
        Publisher = {IEEE},
        Doi = {10.1109/SEFM.2008.36}
    }
37. P. Höfner, G. Struth: On Automating the Calculus of Relations. In A. Armando, P. Baumgartner, G. Dowek (eds.), Automated Reasoning. Lecture Notes in Artificial Intelligence 5195, pp. 50-66, Springer, 2008.
    doi: 10.1007/978-3-540-71070-7_5
    abstract | pdf | bibtex

    Abstract:

    Relation algebras provide abstract equational axioms for the calculus of binary relations. They name an established area of mathematics and have found numerous applications in computing. We prove more than hundred theorems of relation algebras with off-the-shelf automated theorem provers. They form a basic calculus from which more advanced applications can be explored. We also present two automation experiments from the formal methods literature. Our results further demonstrate the feasibility of automated deduction with complex algebraic structures. They also open a new perspective for automated deduction in relational formal methods.
    @InProceedings{Hoefner2008-6,
        Author = {H{\"o}fner, P. and Struth, G.},
        Title = {On Automating the Calculus of Relations},
        BookTitle = {Automated Reasoning},
        Editor = {Armando, A. and Baumgartner, P. and Dowek, G.},
        Series = {Lecture Notes in Artificial Intelligence},
        Volume = {5195},
        Pages = {50-66},
        Year = {2008},
        Publisher = {Springer},
        Doi = {10.1007/978-3-540-71070-7_5}
    }
38. P. Höfner: Automated Reasoning for Hybrid Systems — Two Case Studies —. In R. Berghammer, B. Möller, G. Struth (eds.), Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'08). Lecture Notes in Computer Science 4988, pp. 191-205, Springer, 2008.
    doi: 10.1007/978-3-540-78913-0_15
    abstract | pdf | bibtex

    Abstract:

    At an abstract level hybrid systems are related to variants of Kleene algebra. Since it has recently been shown that Kleene algebras and their variants, like omega algebras, provide a reasonable base for automated reasoning, the aim of the present paper is to show that automated algebraic reasoning for hybrid system is feasible. We mainly focus on applications. In particular, we present case studies and proof experiments to show how concrete properties of hybrid systems, like safety and liveness, can be algebraically characterised and how off-the-shelf automated theorem provers can be used to verify them.
    @InProceedings{Hoefner2008-5,
        Author = {H{\"o}fner, P.},
        Title = {Automated Reasoning for Hybrid Systems --- Two Case Studies ---},
        BookTitle = {Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'08)},
        Editor = {Berghammer, R. and M{\"o}ller, B. and Struth, G.},
        Series = {Lecture Notes in Computer Science},
        Volume = {4988},
        Pages = {191-205},
        Year = {2008},
        Publisher = {Springer},
        Doi = {10.1007/978-3-540-78913-0_15}
    }
39. P. Höfner, G. Struth: Non-termination in Idempotent Semirings. In R. Berghammer, B. Möller, G. Struth (eds.), Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'08). Lecture Notes in Computer Science 4988, pp. 206-220, Springer, 2008.
    doi: 10.1007/978-3-540-78913-0_16
    abstract | pdf | bibtex

    Abstract:

    We study and compare two notions of non-termination on idempotent semirings: infinite iteration and divergence. We determine them in various models and develop conditions for their coincidence. It turns out that divergence yields a simple and natural way of modelling infinite behaviour, whereas infinite iteration shows some anomalies.
    @InProceedings{Hoefner2008-4,
        Author = {H{\"o}fner, P. and Struth, G.},
        Title = {Non-termination in Idempotent Semirings},
        BookTitle = {Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'08)},
        Editor = {Berghammer, R. and M{\"o}ller, B. and Struth, G.},
        Series = {Lecture Notes in Computer Science},
        Volume = {4988},
        Pages = {206-220},
        Year = {2008},
        Publisher = {Springer},
        Doi = {10.1007/978-3-540-78913-0_16}
    }
40. P. Höfner, G. Struth: Automated Reasoning in Kleene Algebra. In F. Pfenning (ed.), Automated Deduction (CADE21). Lecture Notes in Artificial Intelligence 4603, pp. 279-294, Springer, 2007.
    doi: 10.1007/978-3-540-73595-3_19
    abstract | pdf | bibtex

    Abstract:

    It has often been claimed that model checking, special purpose automated deduction or interactive theorem proving are needed for formal program development. We demonstrate that off-the-shelf automated proof and counterexample search is an interesting alternative if combined with the right domain model. We implement variants of Kleene algebras axiomatically in Prover9/Mace4 and perform proof experiments about Hoare, dynamic, temporal logics, concurrency control and termination analysis. They confirm that a simple automated analysis of some important program properties is possible. Particular benefits of this approach include \"soft\" model checking in a first-order setting, cross-theory reasoning between standard formalisms and full automation of some (co)inductive arguments. Kleene algebras might therefore provide light-weight formal methods with heavy-weight automation.
    @InProceedings{Hoefner2007-2,
        Author = {H{\"o}fner, P. and Struth, G.},
        Title = {Automated Reasoning in Kleene Algebra},
        BookTitle = {Automated Deduction (CADE21)},
        Editor = {Pfenning, F.},
        Series = {Lecture Notes in Artificial Intelligence},
        Volume = {4603},
        Pages = {279-294},
        Year = {2007},
        Publisher = {Springer},
        Doi = {10.1007/978-3-540-73595-3_19}
    }
41. P. Höfner, B. Möller: Lazy Semiring Neighbours and Some Applications. In R.A. Schmidt (ed.), Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'06). Lecture Notes in Computer Science 4136, pp. 207-221, Springer, 2006.
    doi: 10.1007/11828563_14
    abstract | pdf | bibtex

    Abstract:

    We extend an earlier algebraic approach to Neighbourhood Logic (NL) from domain semirings to lazy semi-rings yielding lazy semiring neighbours. Furthermore we show three important applications for these. The first one extends NL to intervals with infinite length. The second one applies lazy semiring neighbours in an algebraic semantics of the branching time temporal logic CTL*. The third one sets up a connection between hybrid systems and lazy semiring neighbours.
    @InProceedings{Hoefner2006-9,
        Author = {H{\"o}fner, P. and M{\"o}ller, B.},
        Title = {Lazy Semiring Neighbours and Some Applications},
        BookTitle = {Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'06)},
        Editor = {Schmidt, R.A.},
        Series = {Lecture Notes in Computer Science},
        Volume = {4136},
        Pages = {207-221},
        Year = {2006},
        Publisher = {Springer},
        Doi = {10.1007/11828563_14}
    }
42. P. Höfner, B. Möller, K. Solin: Omega Algebra, Demonic Refinement Algebra and Commands. In R.A. Schmidt (ed.), Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'06). Lecture Notes in Computer Science 4136, pp. 222-234, Springer, 2006.
    doi: 10.1007/11828563_15
    abstract | pdf | bibtex

    Abstract:

    Weak omega algebra and demonic refinement algebra are two ways of describing systems with finite and infinite iteration. We show that these independently introduced kinds of algebras can actually be defined in terms of each other. By defining modal operators on the underlying weak semiring, that result directly gives a demonic refinement algebra of commands. This yields models in which extensionality does not hold. Since in predicate-transformer models extensionality always holds, this means that the axioms of demonic refinement algebra do not characterise predicate-transformer models uniquely. The omega and the demonic refinement algebra of commands both utilise the convergence operator that is analogous to the halting predicate of modal μ-calculus. We show that the convergence operator can be defined explicitly in terms of infinite iteration and domain if and only if domain coinduction for infinite iteration holds.
    @InProceedings{Hoefner2006-8,
        Author = {H{\"o}fner, P. and M{\"o}ller, B. and Solin, K.},
        Title = {Omega Algebra, Demonic Refinement Algebra and Commands},
        BookTitle = {Relations and Kleene Algebra in Computer Science (RelMiCS/AKA'06)},
        Editor = {Schmidt, R.A.},
        Series = {Lecture Notes in Computer Science},
        Volume = {4136},
        Pages = {222-234},
        Year = {2006},
        Publisher = {Springer},
        Doi = {10.1007/11828563_15}
    }
43. P. Höfner, R. Khedri, B. Möller: Feature Algebra. In J. Misra, T. Nipkow, E. Sekerinski (eds.), Formal Methods (FM'06). Lecture Notes in Computer Science 4085, pp. 300-315, Springer, 2006.
    doi: 10.1007/11813040_21
    abstract | pdf | bibtex

    Abstract:

    Based on experience from the hardware industry, product families have entered the software development process as well, since software developers often prefer not to build a single product but rather a family of similar products that share at least one common functionality while having well-identified variabilities. Such shared commonalities, also called features, reach from common hardware parts to software artefacts such as requirements, architectural properties, components, middleware, or code. We use idempotent semirings as the basis for a feature algebra that allows a formal treatment of the above notions as well as calculations with them. In particular models of feature algebra the elements are sets of products, i.e. product families. We extend the algebra to cover product lines, refinement, product development and product classification. Finally we briefly describe a prototype implementation of one particular model.
    @InProceedings{Hoefner2006-5,
        Author = {H{\"o}fner, P. and Khedri, R. and M{\"o}ller, B.},
        Title = {Feature Algebra},
        BookTitle = {Formal Methods (FM'06)},
        Editor = {Misra, J. and Nipkow, T. and Sekerinski, E.},
        Series = {Lecture Notes in Computer Science},
        Volume = {4085},
        Pages = {300-315},
        Year = {2006},
        Publisher = {Springer},
        Doi = {10.1007/11813040_21}
    }
44. B. Möller, P. Höfner, G. Struth: Quantales and Temporal Logics. In M. Johnson, V. Vene (eds.), Algebraic Methodology and Software Technology (AMAST'06). Lecture Notes in Computer Science 4019, pp. 263-277, Springer, 2006.
    doi: 10.1007/11784180_21
    abstract | pdf | bibtex

    Abstract:

    We propose an algebraic semantics for the temporal logic CTL* and simplify it for its sublogics CTL and LTL. We abstractly represent state and path formulas over transition systems in Boolean left quantales. These are complete lattices with a multiplication that preserves arbitrary joins in its left argument and is isotone in its right argument. Over these quantales, the semantics of CTL* formulas can be encoded via finite and infinite iteration operators; the CTL and LTL operators can be related to domain operators. This yields interesting new connections between representations as known from the modal μ-calculus and Kleene/ω-algebra.
    @InProceedings{Hoefner2006-4,
        Author = {M{\"o}ller, B. and H{\"o}fner, P. and Struth, G.},
        Title = {Quantales and Temporal Logics},
        BookTitle = {Algebraic Methodology and Software Technology (AMAST'06)},
        Editor = {Johnson, M. and Vene, V.},
        Series = {Lecture Notes in Computer Science},
        Volume = {4019},
        Pages = {263-277},
        Year = {2006},
        Publisher = {Springer},
        Doi = {10.1007/11784180_21}
    }
45. P. Höfner, B. Möller: Towards an Algebra of Hybrid Systems. In W. MacCaull, M. Winter, I. Düntsch (eds.), Relational Methods in Computer Science (RelMiCS8/AKA3). Lecture Notes in Computer Science 3929, pp. 121-133, Springer, 2006.
    doi: 10.1007/11734673_10
    abstract | pdf | bibtex

    Abstract:

    We present a trajectory-based model for describing hybrid systems. For this we use left quantales and left semirings, thus providing a new application for these algebraic structures. Furthermore, we sketch a connection between game theory and hybrid systems.
    @InProceedings{Hoefner2006-2,
        Author = {H{\"o}fner, P. and M{\"o}ller, B.},
        Title = {Towards an Algebra of Hybrid Systems},
        BookTitle = {Relational Methods in Computer Science (RelMiCS8/AKA3)},
        Editor = {MacCaull, W. and Winter, M. and D{\"u}ntsch, I.},
        Series = {Lecture Notes in Computer Science},
        Volume = {3929},
        Pages = {121-133},
        Year = {2006},
        Publisher = {Springer},
        Doi = {10.1007/11734673_10}
    }
46. A. Huhn, P. Höfner, W. Kießling: Towards Evaluating the Impact of Ontologies on the Quality of a Digital Library Alerting System. In M. Winter, A. Rauber, S. Christodoulakis, A Min Tjoa (eds.), Research and Advanced Technology for Digital Libraries (ECDL'05). Lecture Notes in Computer Science 3652, pp. 498-499, Springer, 2005.
    doi: 10.1007/11551362_53
    abstract | pdf | bibtex

    Abstract:

    Advanced personalization techniques are required to cope with novel challenges posed by attribute-rich digital libraries. At the heart of our deeply personalized alerting system is one extensible preference model that serves all purposes in conjunction with our search technology Preference XPath and XML-based semantic annotations of digital library objects. In this paper we focus on the impact of automatic query expansion by ontologies. First results indicate that use of ontologies improves the quality of the result set and generates further results of higher quality.
    @InProceedings{Hoefner2005-3,
        Author = {Huhn, A. and H{\"o}fner, P. and Kie{\ss}ling, W.},
        Title = {Towards Evaluating the Impact of Ontologies on the Quality of a Digital Library Alerting System},
        BookTitle = {Research and Advanced Technology for Digital Libraries (ECDL'05)},
        Editor = {Winter, M. and Rauber, A. and Christodoulakis, S. and Tjoa, A Min},
        Series = {Lecture Notes in Computer Science},
        Volume = {3652},
        Pages = {498-499},
        Year = {2005},
        Publisher = {Springer},
        Doi = {10.1007/11551362_53}
    }

Editorials

1. Festschrift for Rob van Glabbeek. P. Höfner, C. Morgan, V. Pratt (eds.), Acta Informatica 57(3-5). Springer, 2020.
2. Special Issue on Relational and Algebraic Methods in Computer Science. P. Höfner, D. Pous, G. Struth (eds.), Journal of Logical and Algebraic Methods in Programming. Elsevier, 2019.
3. Relational and Algebraic Methods in Computer Science. P. Höfner, D. Pous, G. Struth (eds.), Lecture Notes in Computer Science 10226. Springer, 2017. doi: 10.1007/978-3-319-57418-9
4. 2nd Workshop on Models for Formal Analysis of Real Systems. H. Hermanns, P. Höfner (eds.), Electronic Proceedings in Theoretical Computer Science 244. Open Publishing Association, 2017. doi: 10.4204/EPTCS.244
5. Special Issue on Relational and Algebraic Methods in Computer Science (RAMiCS 2014). P. Höfner, P. Jipsen, W. Kahl, M.E. Müller (eds.), Journal of Logical and Algebraic Methods in Programming 85(2). Elsevier, 2016.
6. 1st Workshop on Models for Formal Analysis of Real Systems. R.J. van Glabbeek, J.F. Groote, P. Höfner (eds.), Electronic Proceedings in Theoretical Computer Science 196. Open Publishing Association, 2015.
7. 13th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2012). W. Kahl, T. Griffin, P. Höfner (eds.), Journal of Logical and Algebraic Methods in Programming 84(3). Elsevier, 2015.
8. Relational and Algebraic Methods in Computer Science. P. Höfner, P. Jipsen, W. Kahl, M.E. Müller (eds.), Lecture Notes in Computer Science 8428. Springer, 2014. doi: 10.1007/978-3-319-06251-8
9. Festschrift in honour of Carroll Morgan. P. Höfner, R.J. van Glabbeek, I.J. Hayes (eds.), Formal Aspects of Computing 24(4-6). Springer, 201.
10. ATx'12/WInG'12: Joint Proceedings of the Workshops on Automated Theory eXploration and on Invariant Generation. J. Fleuriot, P. Höfner, A. McIver, A. Smaill (eds.), EasyChair Proceedings: EPiC Series 17, 2012.
11. Proceedings of Workshop on Automated Theory Engineering (ATE 2011). P. Höfner, A. McIver, G. Struth (eds.), CEUR Proceedings Vol-760. 2011.

Archive of Formal Proofs

1. W. Guttmann, P. Höfner: Relational Characterisations of Paths. In Archive of Formal Proofs, 2020. link: www.isa-afp.org/entries/Relational_Paths.html
   abstract | bibtex

   Abstract:

   Binary relations are one of the standard ways to encode, characterise and reason about graphs. Relation algebras provide equational axioms for a large fragment of the calculus of binary relations. Although relations are standard tools in many areas of mathematics and computing, researchers usually fall back to point-wise reasoning when it comes to arguments about paths in a graph. We present a purely algebraic way to specify different kinds of paths in Kleene relation algebras, which are relation algebras equipped with an operation for reflexive transitive closure. We study the relationship between paths with a designated root vertex and paths without such a vertex. Since we stay in first-order logic this development helps with mechanising proofs. To demonstrate the applicability of the algebraic framework we verify the correctness of three basic graph algorithms.
   @article{Hoefner2020-6,
       Author = {Guttmann, W. and H{\"o}fner, P.},
       Title = {Relational Characterisations of Paths},
       Journal = {Archive of Formal Proofs},
       Year = {2020},
   }
2. V.B.F. Gomes, W. Guttmann, P. Höfner, G. Struth, T. Weber: Kleene Algebras with Domain. In Archive of Formal Proofs, 2016. link: www.isa-afp.org/entries/KAD.shtml
   abstract | bibtex

   Abstract:

   Kleene algebras with domain are Kleene algebras endowed with an operation that maps each element of the algebra to its domain of definition (or its complement) in abstract fashion. They form a simple algebraic basis for Hoare logics, dynamic logics or predicate transformer semantics. We formalise a modular hierarchy of algebras with domain and antidomain (domain complement) operations in Isabelle/HOL that ranges from domain and antidomain semigroups to modal Kleene algebras and divergence Kleene algebras. We link these algebras with models of binary relations and program traces. We include some examples from modal logics, termination and program analysis.
   @article{Hoefner2016-10,
       Author = {Gomes, V.B.F. and Guttmann, W. and H{\"o}fner, P. and Struth, G. and Weber, T.},
       Title = {Kleene Algebras with Domain},
       Journal = {Archive of Formal Proofs},
       Year = {2016},
   }
3. T. Bourke, P. Höfner: Loop Freedom of the (Untimed) AODV Routing Protocol. In Archive of Formal Proofs, 2014. link: www.isa-afp.org/entries/AODV.shtml
   abstract | bibtex

   Abstract:

   The Ad hoc On-demand Distance Vector (AODV) routing protocol allows the nodes in a Mobile Ad hoc Network (MANET) or a Wireless Mesh Network (WMN) to know where to forward data packets. Such a protocol is ‘loop free’ if it never leads to routing decisions that forward packets in circles.
   This development mechanises an existing pen-and-paper proof of loop freedom of AODV. The protocol is modelled in the Algebra of Wireless Networks (AWN), which is the subject of an earlier paper and AFP mechanization. The proof relies on a novel compositional approach for lifting invariants to networks of nodes.
   We exploit the mechanization to analyse several variants of AODV and show that Isabelle/HOL can re-establish most proof obligations automatically and identify exactly the steps that are no longer valid.
   @article{Hoefner2014-6,
       Author = {Bourke, T. and H{\"o}fner, P.},
       Title = {Loop Freedom of the (Untimed) {AODV} Routing Protocol},
       Journal = {Archive of Formal Proofs},
       Year = {2014},
   }

Technical Reports (incomplete)

1. P. Höfner, B. Möller: A New Correctness Proof for Prim's Algorithm. Technical Report 2019-02, Institute of Computer Science, University of Augsburg. 2019. direct link.
   abstract | pdf | bibtex

   Abstract:

   We present a new correctness proof for Prim's algorithm. The standard proof establishes the invariant that each iteration constructs a subtree of some minimal spanning tree, and heavily relies on the existence of a spanning tree of the overall graph, as well as an `edge exchange' property, which includes reasoning about graph cycles. We establish a stronger property showing that the algorithm builds a minimal spanning tree in each step, w.r.t. the vertices already covered. As a consequence, the proof neither uses the existence of a minimal spanning tree of the entire graph, nor the classical exchange property.
   @Techreport{Hoefner2019-5,
       Author = {H{\"o}fner, P. and M{\"o}ller, B.},
       Title = {A New Correctness Proof for Prim's Algorithm},
       Institution = {Institute of Computer Science, University of Augsburg},
       Number = {2019-02},
       Year = {2019},
       Url = {opus.bibliothek.uni-augsburg.de/opus4/57262}
   }
2. E. Bres, R.J. van Glabbeek, P. Höfner: A Timed Process Algebra for Wireless Networks with an Application in Routing. Technical Report 9145, NICTA. 2016. url: www.nicta.com.au/pub?doc=9145.
   arXiv: CoRR abs/1606.03663
   abstract | pdf | bibtex

   Abstract:

   This paper proposes a timed process algebra for wireless networks, an extension of the Algebra for Wireless Networks. It combines treatments of local broadcast, conditional unicast and data structures, which are essential features for the modelling of network protocols. In this framework we model and analyse the Ad hoc On-Demand Distance Vector routing protocol, and show that, contrary to claims in the literature, it fails to be loop free. We also present boundary conditions for a fix ensuring that the resulting protocol is indeed loop free.
   @Techreport{Hoefner2016-8,
       Author = {Bres, E. and van Glabbeek, R.J. and H{\"o}fner, P.},
       Title = {A Timed Process Algebra for Wireless Networks with an Application in Routing},
       Institution = {NICTA},
       Number = {9145},
       Year = {2016},
       Url = {www.nicta.com.au/pub?doc=9145}
   }
3. R.J. van Glabbeek, P. Höfner: Progress, Fairness and Justness in Process Algebra. Technical Report 8501, NICTA. 2015. url: www.nicta.com.au/pub?doc=8501.
   arXiv: CoRR abs/1501.03268
   abstract | pdf | bibtex

   Abstract:

   To prove liveness properties of concurrent systems, it is often necessary to postulate progress, fairness and justness properties. This paper investigates how the necessary progress, fairness and justness assumptions can be added to or incorporated in a standard process-algebraic specification formalism. We propose a formalisation that can be applied to a wide range of process algebras. The presented formalism is used to reason about route discovery and packet delivery in the setting of wireless networks.
   @Techreport{Hoefner2015-3,
       Author = {van Glabbeek, R.J. and H{\"o}fner, P.},
       Title = {Progress, Fairness and Justness in Process Algebra},
       Institution = {NICTA},
       Number = {8501},
       Year = {2015},
       Url = {www.nicta.com.au/pub?doc=8501}
   }
4. D. Batory, P. Höfner, B. Möller, A. Zelend: Features, Modularity, and Variation Points. Technical Report TR-2147, University of Texas at Austin. 2013. direct link.
   abstract | pdf | bibtex

   Abstract:

   A feature interaction algebra (FIA) is an abstract model of features, feature interactions, and their compositions. A structured document algebra (SDA) defines modules with variation points and how such modules compose. We present both FIA and SDA in this paper, and homomorphisms that relate FIA expressions to SDA expressions. Doing so separates fundamental concepts of Software Product Lines (SPLs) that have previously been conflated and misunderstood. Our work also justifies observations and relationships that have been used in prior work on feature-based SPLs.
   @Techreport{Hoefner2013-7,
       Author = {Batory, D. and H{\"o}fner, P. and M{\"o}ller, B. and Zelend, A.},
       Title = {Features, Modularity, and Variation Points},
       Institution = {University of Texas at Austin},
       Number = {TR-2147},
       Year = {2013},
       Url = {apps.cs.utexas.edu/tech_reports/reports/tr/TR-2147.pdf}
   }
5. A. Fehnker, R.J. van Glabbeek, P. Höfner, M. Portmann, A. McIver, W.L. Tan: A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing AODV. Technical Report 5513, NICTA. 2013. url: www.nicta.com.au/pub?doc=5513.
   arXiv: CoRR abs/1312.7645
   abstract | pdf | bibtex

   Abstract:

   We propose a process algebra for wireless mesh networks that combines novel treatments of local broadcast, conditional unicast and data structures. In this framework, we model the Ad-hoc On-Demand Distance Vector (AODV) routing protocol. We give a complete specification of this widely-used protocol, where only timing aspects are omitted. The process algebra allows us to state and (dis)prove crucial properties of mesh network routing protocols such as loop freedom and packet delivery.
   Based on the unambiguous specification, we locate some problems and limitations of AODV that could easily yield performance problems. Two examples are the non-optimal routes established by AODV and the fact that some routes are not found at all. These problems are then analysed and improvements are suggested. Since the improvements are formalised in the same process algebra, proofs of loop freedom etc. become simple.
   @Techreport{Hoefner2013-1,
       Author = {Fehnker, A. and van Glabbeek, R.J. and H{\"o}fner, P. and Portmann, M. and McIver, A. and Tan, W.L.},
       Title = {A Process Algebra for Wireless Mesh Networks used for Modelling, Verifying and Analysing {AODV}},
       Institution = {NICTA},
       Number = {5513},
       Year = {2013},
       Url = {www.nicta.com.au/pub?doc=5513}
   }
6. P. Höfner, B. Möller, A. Zelend: Foundations of Coloring Algebra with Consequences for Feature-Oriented Programming. Technical Report 2012-06, Institute of Computer Science, University of Augsburg. 2012. direct link.
   abstract | pdf | bibtex

   Abstract:

   In 2011, simple and concise axioms for feature compositions, interactions and products have been proposed by Batory et al. They were mainly inspired by Kästner's Colored IDE (CIDE) as well as by experience in feature oriented programming over the last decades. However, so far only axioms were proposed; consequences of these axioms such as variability in models have not been studied. In this paper we discuss the proposed axioms from a theoretical point of view, which yields a much better understanding of the proposed algebra and therefore of feature oriented programming. For example, we show that the axioms characterising feature composition are isomorphic to set-theoretic models.
   @Techreport{Hoefner2012-12,
       Author = {H{\"o}fner, P. and M{\"o}ller, B. and Zelend, A.},
       Title = {Foundations of Coloring Algebra with Consequences for Feature-Oriented Programming},
       Institution = {Institute of Computer Science, University of Augsburg},
       Number = {2012-06},
       Year = {2012},
       Url = {www.informatik.uni-augsburg.de/en/chairs/dbis/pmi/publications/all_pmi_tech-reports/tr-2012-06_hoe_moe_zel.html}
   }
7. P. Höfner, S. Mentl, B. Möller, W. Scholz: Requirements in Feature Algebra. Technical Report 2010-12, Institute of Computer Science, University of Augsburg. 2010. direct link.
   abstract | bibtex

   Abstract:

   Feature Algebra is intended to capture the commonalities of feature oriented software development (FOSD) such as introductions, refinements and quantification. It abstracts from differences of minor importance and focusses on most of the main aspects of FOSD. However, so far requirements have not been integrated into Feature Algebra. They arise within different aspects of feature orientation, like feature interaction, feature dependence, mutual exclusion and required features. In this paper we present a possibility how to integrate requirements into Feature Algebra.
   @Techreport{Hoefner2010-9,
       Author = {H{\"o}fner, P. and Mentl, S. and M{\"o}ller, B. and Scholz, W.},
       Title = {Requirements in Feature Algebra},
       Institution = {Institute of Computer Science, University of Augsburg},
       Number = {2010-12},
       Year = {2010},
       Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2010-12_hoe_men_moe_scholz/}
   }
8. P. Höfner, R. Khedri, B. Möller: Supplementing Product Families with Behaviour. Technical Report 2010-13, Institute of Computer Science, University of Augsburg. 2010. direct link.
   abstract | pdf | bibtex

   Abstract:

   A common approach to dealing with software requirements volatility is to define product families instead of single products. In earlier papers we have developed an algebra of such families that, roughly, consists in a more abstract view of and-or trees of features as used in Feature-Oriented Domain Analysis. A product family is represented by an algebraic term over the feature names; it can be manipulated using equational laws such as associativity or distributivity. Initially, only 'syntactic' models of the algebra were considered, giving more or less just the names of the features used in the various products of a family and certain interrelations such as mandatory occurrence and implication between or mutual exclusion of features, without attaching any kind of \"meaning\" to the features. While this is interesting and useful for determining the variety and number of possible members of such a family, it is wholly insufficient when it comes to talking about the correctness of families in a semantic manner. In the present paper we define a class of \"semantic\" models of the general abstract prod-uct family algebra that allows treating very relevant additional questions. In these models, the features of a family are requirements scenarios formalised as pairs of relational specifications of a proposed system and its environment. However, the paper is just intended as a proof of feasibility; we are convinced that the approach can also be employed for different semantic models such as general denotational or stream-based semantics.
   @Techreport{Hoefner2010-8,
       Author = {H{\"o}fner, P. and Khedri, R. and M{\"o}ller, B.},
       Title = {Supplementing Product Families with Behaviour},
       Institution = {Institute of Computer Science, University of Augsburg},
       Number = {2010-13},
       Year = {2010},
       Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2010-13_hoe_khe_moe/}
   }
9. P. Höfner, B. Möller: Fixing Zeno Gaps. Technical Report 2010-11, Institute of Computer Science, University of Augsburg. 2010. direct link.
   abstract | pdf | bibtex

   Abstract:

   In computer science fixpoints play a crucial role. Most often least and greatest fixpoints are sufficient. However there are situations where other ones are needed. In this paper we study, on an algebraic base, a special fixpoint of the function f(x) = a⋅x that describes infinite iteration of an element a. We show that the greatest fixpoint is too imprecise. Special problems arise if the iterated element contains the possibility of stepping on the spot (e.g. skip in a programming language) or if it allows Zeno behaviour. We present a construction for a fixpoint that captures these phenomena in a precise way. The theory is presented and motivated using an example from hybrid system analysis.
   @Techreport{Hoefner2010-7,
       Author = {H{\"o}fner, P. and M{\"o}ller, B.},
       Title = {Fixing Zeno Gaps},
       Institution = {Institute of Computer Science, University of Augsburg},
       Number = {2010-11},
       Year = {2010},
       Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2010-11_hoe_moe/}
   }
10. P. Höfner, M.E. Müller, S. Zeissler: ATPPortal: A User-friendly Webbased Interface for Automated Theorem Provers and for Automatically Generated Proofs. Technical Report 2010-10, Institute of Computer Science, University of Augsburg. 2010. direct link.
    abstract | pdf | bibtex

    Abstract:

    This report describes the design, the implementation and the usage of a system for managing different systems for automated theorem proving and automatically generated proofs. In particular, we focus on a user-friendly web-based interface and a structure for collecting and cataloguing proofs in a uniform way. The second point hopefully helps to understand the structure of automatically generated proofs and builds a starting point for new insights for strategies for proof planning.
    @Techreport{Hoefner2010-6,
        Author = {H{\"o}fner, P. and M{\"u}ller, M.E. and Zeissler, S.},
        Title = {{ATPPortal}: A User-friendly Webbased Interface for Automated Theorem Provers and for Automatically Generated Proofs},
        Institution = {Institute of Computer Science, University of Augsburg},
        Number = {2010-10},
        Year = {2010},
        Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2010-10_hoe_mue_zei/}
    }
11. P. Höfner, B. Möller: An Extension of Feature Algebra. Technical Report 2010-09, Institute of Computer Science, University of Augsburg. 2010. direct link.
    abstract | pdf | bibtex

    Abstract:

    Feature algebra was introduced as an abstract framework for feature oriented software development. One goal is to provide a common, clearly defined basis for the key ideas of feature orientation. So far, feature algebra captures major aspects of feature orientation, like the hierarchical structure of features and feature composition. However, as we will show, it is not able to model aspects at the level of code, i.e., situations where code fragments of different features have to be merged. With other words, it does not reflect details of concret implementations. In the paper we first present concrete models for the original axioms of feature algebra which represent the main concepts of feature oriented programs. This shows that the abstract feature algebra can be interpreted in different ways. We then use these models to show that the axioms of feature algebra do not reflect all aspects of feature orientation properly. This gives the motivation to extend the abstract algebra — which is the second main contribution of the paper. We modify the axioms and introduce the concept of an extended feature algebra. The original algebra can be retrieved by a single additional axiom. As third contribution we introduce more operators to coveer concepts like overriding in the abstract setting.
    @Techreport{Hoefner2010-5,
        Author = {H{\"o}fner, P. and M{\"o}ller, B.},
        Title = {An Extension of Feature Algebra},
        Institution = {Institute of Computer Science, University of Augsburg},
        Number = {2010-09},
        Year = {2010},
        Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2010-09_hoe_moe/}
    }
12. H.H. Dang, P. Höfner, B. Möller: Algebraic Separation Logic. Technical Report 2010-06, Institute of Computer Science, University of Augsburg. 2010. direct link.
    abstract | pdf | bibtex

    Abstract:

    We present an algebraic approach to separation logic. In particular, we give an algebraic characterisation for assertions of separation logic, discuss different classes of assertions and prove abstract laws fully algebraically. After that, we use our algebraic framework to give a relational semantics of the commands of the simple programming language associated with separation logic. On this basis we prove the frame rule in an abstract and concise way. We also propose a more general version of separating conjunction which leads to a frame rule that is easier to prove. In particular, we show how to algebraically formulate the requirement that a command does not change certain variables; this is also expressed more conveniently using the generalised separating conjunction. The algebraic view does not only yield new insights on separation logic but also shortens proofs due to a point free representation. It is largely first-order and hence enables the use of off-the-shelf automated theorem provers for verifying properties at a more abstract level.
    @Techreport{Hoefner2010-4,
        Author = {Dang, H.H. and H{\"o}fner, P. and M{\"o}ller, B.},
        Title = {Algebraic Separation Logic},
        Institution = {Institute of Computer Science, University of Augsburg},
        Number = {2010-06},
        Year = {2010},
        Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2010-06_dan_hoe_moe/}
    }
13. H.H. Dang, P. Höfner: Automated Higher-Order Reasoning in Quantales. Technical Report 2010-03, Institute of Computer Science, University of Augsburg. 2010. direct link.
    abstract | pdf | bibtex

    Abstract:

    Originally developed as an algebraic characterisation for quantum mechanics, the algebraic structure of quantales nowadays finds widespread applications ranging from (non-commutative) logics to hybrid systems. We present an approach to bring reasoning in quantales into the realm of (fully) automated theorem proving. Hence the paper paves the way for automatisation in various (new) fields of applications. To achieve this goal and to receive a general approach (independent of any particular theorem prover), we use the TPTP Problem Library for higher-order logic. In particular, we give an encoding of quantales in the typed higher-order form (THF) and present some theorems about quantales which can be proved fully automatically. We further present prospective applications for our approach and discuss practical experiences using THF.
    @Techreport{Hoefner2010-3,
        Author = {Dang, H.H. and H{\"o}fner, P.},
        Title = {Automated Higher-Order Reasoning in Quantales},
        Institution = {Institute of Computer Science, University of Augsburg},
        Number = {2010-03},
        Year = {2010},
        Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2010-03_dan_hoe/}
    }
14. H.H. Dang, P. Höfner, B. Möller: Towards Algebraic Separation Logic. Technical Report 2009-12, Institute of Computer Science, University of Augsburg. 2009. direct link.
    abstract | pdf | bibtex

    Abstract:

    We present an algebraic approach to separation logic. In particular, we give algebraic characterisations for all constructs of separation logic like assertions and commands. 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.
    @Techreport{Hoefner2009-6,
        Author = {Dang, H.H. and H{\"o}fner, P. and M{\"o}ller, B.},
        Title = {Towards Algebraic Separation Logic},
        Institution = {Institute of Computer Science, University of Augsburg},
        Number = {2009-12},
        Year = {2009},
        Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2009-12_dan_hoe_moe/}
    }
15. P. Höfner, G. Struth: On Automating the Calculus of Relations. Technical Report CS-08-05, Department of Computer Science, University of Sheffield. 2008.
    abstract | pdf | bibtex

    Abstract:

    Relation algebras provide abstract equational axioms for the calculus of binary relations. They name an established area of mathematics with various applications in computer science. We prove more than hundred theorems of relation algebras with off-the-shelf automated theorem provers. This yields a basic calculus from which more advance applications can be explored. Here, we present two examples from the formal methods literature. Our experiments not only further underline the feasibility of automated deduction in complex algebraic structures and provide theorem proving benchmarks, they also pave the way for lifting established formal methods such as B or Z to a new level of automation.
    @Techreport{Hoefner2008-10,
        Author = {H{\"o}fner, P. and Struth, G.},
        Title = {On Automating the Calculus of Relations},
        Institution = {Department of Computer Science, University of Sheffield},
        Number = {CS-08-05},
        Year = {2008},
        Url = {}
    }
16. P. Höfner, R. Khedri, B. Möller: Algebraic View Reconciliation. Technical Report 2007-13, Institute of Computer Science, University of Augsburg. 2007. direct link.
    abstract | bibtex

    Abstract:

    Embedded systems such as automotive systems are very complex to specify. Since it is difficult to capture all their requirements or their design in one single model, approaches working with several system views are adopted. The main problem there is to keep these views coherent; the issue is known as view reconciliation. This paper proposes an algebraic solution. It uses sets of integration constraints that link (families of) system features in one view to other (families of) features in the same or a different view. Both families and constraints are formalized using a feature algebra. Besides presenting a constraint relation and its mathematical properties, the paper shows in several examples the suitability of this approach for a wide class of integration constraint formulations
    @Techreport{Hoefner2007-8,
        Author = {H{\"o}fner, P. and Khedri, R. and M{\"o}ller, B.},
        Title = {Algebraic View Reconciliation},
        Institution = {Institute of Computer Science, University of Augsburg},
        Number = {2007-13},
        Year = {2007},
        Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2007-13_hoe_khe_moe/}
    }
17. P. Höfner, F. Lautenbacher: Algebraic Structure of Web Services. Technical Report 2007-12, Institute of Computer Science, University of Augsburg. 2007. direct link.
    abstract | pdf | bibtex

    Abstract:

    The Service-Oriented Architecture is gaining more and more attention and one way of realising it is the usage of Web Services. But which Web Services need to be invoked to reach a goal and which parameters are necessary at the beginning or are returned at the end? In this report we present an algebraic structure of Web Services in order to formally describe the Web Services and assist the users in Web Service composition. Hence, we apply relation algebra, tests, Kleene star and modal operators to characterise Web Services and Web Service Composition.
    @Techreport{Hoefner2007-7,
        Author = {H{\"o}fner, P. and Lautenbacher, F.},
        Title = {Algebraic Structure of Web Services},
        Institution = {Institute of Computer Science, University of Augsburg},
        Number = {2007-12},
        Year = {2007},
        Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2007-12_hoe_lau/}
    }
18. P. Höfner, B. Möller: An Algebra of Hybrid Systems. Technical Report 2007-08, Institute of Computer Science, University of Augsburg. 2007. direct link.
    abstract | pdf | bibtex

    Abstract:

    Hybrid systems are heterogeneous systems characterised by the interaction of discrete and continuous dynamics. We present a trajectory-based algebraic model for describing hybrid systems; the trajectories used are closely related to streams. The algebra is based on left quantales and left semirings and provides a new application for these algebraic structures. We show that hybrid automata, which are probably the standard tool for describing hybrid systems, can conveniently be embedded into our algebra. Moreover we point out some important advantages of the algebraic approach. In particular, we show how to handle Zeno effects, which are excluded by most other authors. The development of the theory is illustrated by a running example and a larger case study.
    @Techreport{Hoefner2007-5,
        Author = {H{\"o}fner, P. and M{\"o}ller, B.},
        Title = {An Algebra of Hybrid Systems},
        Institution = {Institute of Computer Science, University of Augsburg},
        Number = {2007-08},
        Year = {2007},
        Url = {www.informatik.uni-augsburg.de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2007-08_hoe_moe/}
    }
19. P. Höfner, G. Struth: Can Refinement be Automated?. Technical Report CS-07-08, Department of Computer Science, University of Sheffield. 2007. direct link.
    abstract | pdf | bibtex

    Abstract:

    Relation algebras provide abstract equational axioms for the calculus of binary relations. They name an established area of mathematics with various applications in computer science. We prove more than hundred theorems of relation algebras with off-the-shelf automated theorem provers. This yields a basic calculus from which more advance applications can be explored. Here, we present two examples from the formal methods literature. Our experiments not only further underline the feasibility of automated deduction in complex algebraic structures and provide theorem proving benchmarks, they also pave the way for lifting established formal methods such as B or Z to a new level of automation.
    @Techreport{Hoefner2007-4,
        Author = {H{\"o}fner, P. and Struth, G.},
        Title = {Can Refinement be Automated?},
        Institution = {Department of Computer Science, University of Sheffield},
        Number = {CS-07-08},
        Year = {2007},
        Url = {www.dcs.shef.ac.uk/intranet/research/public/resmes/CS0708.pdf}
    }
20. P. Höfner, G. Struth: Automated Reasoning in Kleene Algebra. Technical Report CS-07-04, Department of Computer Science, University of Sheffield. 2007.
    abstract | pdf | bibtex

    Abstract:

    It has often been claimed that model checking, special purpose automated deduction or interactive theorem proving are needed for formal program development. We demonstrate that off-the-shelf automated proof and counterexample search is an interesting alternative if combined with the right domain model. We implement variants of Kleene algebras axiomatically in Prover9/Mace4 and perform proof experiments about Hoare, dynamic, temporal logics, concurrency control and termination analysis. They confirm that a simple automated analysis of some important program properties is possible. Particular benefits of this approach include \"soft\" model checking in a first-order setting, cross-theory reasoning between standard formalisms and full automation of some (co)inductive arguments. Kleene algebras might therefore provide light-weight formal methods with heavy-weight automation.
    @Techreport{Hoefner2007-3,
        Author = {H{\"o}fner, P. and Struth, G.},
        Title = {Automated Reasoning in Kleene Algebra},
        Institution = {Department of Computer Science, University of Sheffield},
        Number = {CS-07-04},
        Year = {2007},
        Url = {}
    }
21. P. Höfner, G. Struth: Algebraic Notions of Non-Termination. Technical Report CS-06-12, Department of Computer Science, University of Sheffield. 2006. direct link.
    abstract | pdf | bibtex

    Abstract:

    We study and compare two notions of non-termination on idempotent semirings: infinite iteration and divergence. We determine them in various models and develop conditions for their coincidence. It turns out that divergence yields a simple and natural way of modelling infinite behaviour, whereas infinite iteration shows some anomalies.
    @Techreport{Hoefner2006-11,
        Author = {H{\"o}fner, P. and Struth, G.},
        Title = {Algebraic Notions of Non-Termination},
        Institution = {Department of Computer Science, University of Sheffield},
        Number = {CS-06-12},
        Year = {2006},
        Url = {www.dcs.shef.ac.uk/intranet/research/public/resmes/CS0612.pdf}
    }
22. P. Höfner, B. Möller, K. Solin: Omega Algebra, Demonic Refinement Algebra and Commands. Technical Report 2006-11, Institute of Computer Science, University of Augsburg. 2006. direct link.
    abstract | pdf | bibtex

    Abstract:

    Weak omega algebra and demonic refinement algebra are two ways of describing systems with finite and infinite iteration. We show that these independently introduced kinds of algebras can actually be defined in terms of each other. By defining modal operators on the underlying weak semiring, that result directly gives a demonic refinement algebra of commands. This yields models in which extensionality does not hold. Since in predicate-transformer models extensionality always holds, this means that the axioms of demonic refinement algebra do not characterise predicate-transformer models uniquely. The omega and the demonic refinement algebra of commands both utilise the convergence operator that is analogous to the halting predicate of modal μ-calculus. We show that the convergence operator can be defined explicitly in terms of infinite iteration and domain if and only if domain coinduction for infinite iteration holds.
    @Techreport{Hoefner2006-7,
        Author = {H{\"o}fner, P. and M{\"o}ller, B. and Solin, K.},
        Title = {Omega Algebra, Demonic Refinement Algebra and Commands},
        Institution = {Institute of Computer Science, University of Augsburg},
        Number = {2006-11},
        Year = {2006},
        Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2006-11_hoe_moe_sol/}
    }
23. P. Höfner, B. Möller: Lazy Semiring Neighbours and some Applications. Technical Report 2006-09, Institute of Computer Science, University of Augsburg. 2006. direct link.
    abstract | pdf | bibtex

    Abstract:

    We extend an earlier algebraic approach to Neighbourhood Logic (NL) from domain semirings to lazy semi-rings yielding lazy semiring neighbours. Furthermore we show three important applications for these. The first one extends NL to intervals with infinite length. The second one applies lazy semiring neighbours in an algebraic semantics of the branching time temporal logic CTL*. The third one sets up a connection between hybrid systems and lazy semiring neighbours.
    @Techreport{Hoefner2006-6,
        Author = {H{\"o}fner, P. and M{\"o}ller, B.},
        Title = {Lazy Semiring Neighbours and some Applications},
        Institution = {Institute of Computer Science, University of Augsburg},
        Number = {2006-09},
        Year = {2006},
        Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2006-9_hoe_moe/}
    }
24. B. Möller, P. Höfner, G. Struth: Quantales and Temporal Logics. Technical Report 2006-06, Institute of Computer Science, University of Augsburg. 2006. direct link.
    abstract | pdf | bibtex

    Abstract:

    We propose an algebraic semantics for the temporal logic CTL* and simplify it for its sublogics CTL and LTL. We abstractly represent state and path formulas over transition systems in Boolean left quantales. These are complete lattices with a multiplication that preserves arbitrary joins in its left argument and is isotone in its right argument. Over these quantales, the semantics of CTL* formulas can be encoded via finite and infinite iteration operators; the CTL and LTL operators can be related to domain operators. This yields interesting new connections between representations as known from the modal μ-calculus and Kleene/ω-algebra.
    @Techreport{Hoefner2006-3,
        Author = {M{\"o}ller, B. and H{\"o}fner, P. and Struth, G.},
        Title = {Quantales and Temporal Logics},
        Institution = {Institute of Computer Science, University of Augsburg},
        Number = {2006-06},
        Year = {2006},
        Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2006-6_moe_hoe_str/}
    }
25. P. Höfner, R. Khedri, B. Möller: Feature Algebra. Technical Report 2006-04, Institute of Computer Science, University of Augsburg. 2006. direct link.
    abstract | pdf | bibtex

    Abstract:

    Based on experience from the hardware industry, product families have entered the software development process as well, since software developers often prefer not to build a single product but rather a family of similar products that share at least one common functionality while having well-identified variabilities. Such shared commonalities, also called features, reach from common hardware parts to software artefacts such as requirements, architectural properties, components, middleware, or code. We use idempotent semirings as the basis for a feature algebra that allows a formal treatment of the above notions as well as calculations with them. In particular models of feature algebra the elements are sets of products, i.e. product families. We extend the algebra to cover product lines, refinement, product development and product classification. Finally we briefly describe a prototype implementation of one particular model.
    @Techreport{Hoefner2006-1,
        Author = {H{\"o}fner, P. and Khedri, R. and M{\"o}ller, B.},
        Title = {Feature Algebra},
        Institution = {Institute of Computer Science, University of Augsburg},
        Number = {2006-04},
        Year = {2006},
        Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2006-4_hoe_khe_moe/}
    }
26. P. Höfner: Semiring Neighbours. Technical Report 2005-19, Institute of Computer Science, University of Augsburg. 2005. direct link.
    abstract | pdf | bibtex

    Abstract:

    In 1996 Zhou and Hansen proposed a first-order interval logic called Neighbourhood Logic (NL) for specifying liveness and fairness of computing systems and also defining notions of real analysis in terms of expanding modalities. After that, Roy and Zhou presented a sound and relatively complete Duration Calculus as an extension of NL. We present an embedding of NL into an idempotent semiring of intervals. This embedding allows us to extend NL from single intervals to sets of intervals as well as to extend the approach to arbitrary idempotent semirings. We show that most of the required properties follow directly from Galois connections, hence we get the properties for free. As one important result we get that some of the axioms which were postulated for NL can be dropped since they are theorems in our generalisation. Furthermore, we present some possible interpretations for neighbours beyond intervals. Here we discuss for example reachability in graphs and applications to hybrid systems. At the end of the paper we add finite and infinite iteration to NL and extend idempotent semirigs to Kleene algebras and omega algebras. These extensions are useful for formulating repetitive properties and procedures like loops.
    @Techreport{Hoefner2005-5,
        Author = {H{\"o}fner, P.},
        Title = {Semiring Neighbours},
        Institution = {Institute of Computer Science, University of Augsburg},
        Number = {2005-19},
        Year = {2005},
        Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2005-19_hoe/}
    }
27. A. Huhn, P. Höfner, W. Kießling: Towards Evaluating the Impact of Ontologies on the Quality of a Digital Library Alerting System. Technical Report 2005-07, Institute of Computer Science, University of Augsburg. 2005. direct link.
    abstract | pdf | bibtex

    Abstract:

    Advanced personalization techniques are required to cope with novel challenges posed by attribute-rich digital libraries. At the heart of our deeply personalized alerting system is one extensible preference model that serves all purposes. In this paper we focus on ontology and quality assessment in con- junction with our search technology Preference XPath and XML-based seman- tic annotations of digital library multimedia objects. We evaluate the impacts of automatic query expansion by ontologies by embedding our alerting system P- News as a black box or a glass box in a test lab. It changes configuration pa- rameters on its own, feeds test cases to P-News, compares the results of differ- ent configurations, and stores the result set for further evaluations. The most important indications of this work in progress are: The use of ontologies im- proves the quality of the result set, generates further results of higher quality, and implies the use of knowledge to reduce a loss of focus.
    @Techreport{Hoefner2005-2,
        Author = {Huhn, A. and H{\"o}fner, P. and Kie{\ss}ling, W.},
        Title = {Towards Evaluating the Impact of Ontologies on the Quality of a Digital Library Alerting System},
        Institution = {Institute of Computer Science, University of Augsburg},
        Number = {2005-07},
        Year = {2005},
        Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/db/publications/all_db_tech-reports/tr-2005-7_huh_hoe_kie/}
    }
28. P. Höfner: From Sequential Algebra to Kleene Algebra: Interval Modalities and Duration Calculus. Technical Report 2005-05, Institute of Computer Science, University of Augsburg. 2005. direct link.
    abstract | pdf | bibtex

    Abstract:

    The duration calculus (DC) is a formal, algebraic system for specification and design of real- time systems, where real numbers are used to model time and (Boolean valued) functions to formulate requirements. Since its introduction in 1991 by Chaochen, Hoare and Ravn it has been applied to many case studies and has been extended into several directions. E.g., there is an extension for specifying liveness and safety requirements. This report presents the duration calculus on the basis of Kleene algebra. Doing this we will analyse the DC in a new view.
    @Techreport{Hoefner2005-1,
        Author = {H{\"o}fner, P.},
        Title = {From Sequential Algebra to Kleene Algebra: Interval Modalities and Duration Calculus},
        Institution = {Institute of Computer Science, University of Augsburg},
        Number = {2005-05},
        Year = {2005},
        Url = {www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-2005-5_hoe/}
    }

Miscellaneous (Abstracts, Theses, Prefaces, ...)

1. P. Höfner: Kleene Modules for Routing Procedures (Abstract). In Workshop on Lattices and Relations. 2012.
   abstract | pdf | bibtex

   Abstract:

   In the past, algebraic techniques based on semirings have been used describe shortest path algorithms and routing procedures. These approaches often use matrices over semirings/Kleene algebra, which form again a semiring/Kleene algebra. While these approaches work well for shortest paths algorithms, they fail when modelling timing aspects of routing algorithms. A major shortcoming is that at least one distributivity law has to be dropped on the level of semiring. This implies the loss of associativity on the matrix-level. In this talk I will present the shortcoming with the help of the Ad hoc On-Demand Distance Vector (AODV) routing protocol. AODV is a widely used and standardised routing protocol designed for wireless mesh networks (WMNs); AODV also forms the basis of new WMN routing protocols, such as the upcoming IEEE 802.11s wireless mesh network standard. I will argue that Kleene modules can help in this regard. I will show how crucial aspects of routing protocols in general, and AODV in particular, can be modelled using modules. The talk will be concluded with some discussion on on-going developments and future work.
   @misc{Hoefner2012-9,
       Author = {H{\"o}fner, Peter},
       Howpublished = {Workshop on Lattices and Relations (L&R 2012)},
       Note = {(Abstract)},
       Title = {Kleene Modules for Routing Procedures},
       Year = {2012}
   }
2. P. Höfner: Towards a Representation Theorem for Coloring Algebra (Abstract). In Workshop on Lattices and Relations. 2012.
   abstract | pdf | bibtex

   Abstract:

   Coloring algebra (CA) captures common ideas of feature oriented programming (FOP), a general programming paradigm that provides formalisms, methods, languages, and tools for building main- tainable, customisable, as well as extensible software. FOP has widespread applications from network protocols and data structures to software product lines. It arose from the idea of level-based designs, i.e., the idea that each program (design) can be successively built up by adding more and more levels (features). Later, this idea was generalised to the abstract concept of features. The algebra itself is based on rings and offers simple and concise axioms for feature composition and feature interaction. From these two operations algebraic laws describing products, product lines and other concepts of FOP can be derived. The talk will start with a brief introduction to coloring algebra. In particular I will discuss the interplay between feature composition and interaction. I will also present different models and discuss their relationship to and applicability for feature oriented programming. The examples will show that the choice for defining feature composition is limited. In fact, I will prove that the composition operator is always isomorphic to symmetric-difference in a set-theoretic model. The proof can easily be derived from Kronecker Basis Theorem. By this result we have 'half' a representation theorem for CA. A detailed understanding of feature interaction is missing for the characterisation and the proof of a full representation theorem. Therefore, I will conclude the talk with some observations and conjectures on the structure of coloring algebra, which hopefully helps to come up with a full representation theorem.
   @misc{Hoefner2012-8,
       Author = {H{\"o}fner, Peter},
       Howpublished = {Workshop on Lattices and Relations (L&R 2012)},
       Note = {(Abstract)},
       Title = {Towards a Representation Theorem for Coloring Algebra},
       Year = {2012}
   }
3. H.H. Dang, P. Höfner: First-Order Theorem Prover Evaluation w.r.t. Relation- and Kleene Algebra. In R. Berghammer, B. Möller, G. Struth (eds.), Relations and Kleene algebra in Computer Science — PhD Programme. Technical Report 2008-04, Institute of Computer Science, University of Augsburg, 48-52, 2008.
   abstract | pdf | bibtex

   Abstract:

   Recently it has been shown that off-the-shelf first-order automated theorem provers can successfully verify statements of substantial complexity in relation and Kleene algebras. Until now most of our proof automation had been done using McCune's theorem prover Prover9, while others like SPASS and Vampire were not used extensively. In this paper we use more than $500$ theorems to compare and evaluate 13 first-order theorem provers.
   @misc{Hoefner2008-9,
       Author = {Dang, Han Hing and H{\"o}fner, Peter},
       Title = {First-Order Theorem Prover Evaluation w.r.t. Relation- and {K}leene Algebra},
       Editor = {Berghammer, Rudolf and M{\"o}ller, Bernhard and Struth, Georg},
       BookTitle = {Relations and Kleene algebra in Computer Science (RelMiCS10/AKA5) — PhD Programme},
       Series = {Technical Report 2008-04, Institute of Computer Science, University of Augsburg},
       Pages = {48-52},
       Year = {2008}
   }
4. F. Lautenbacher, P. Höfner: Towards an Algebraic Composition of Semantic Web Services. In R. Berghammer, B. Möller, G. Struth (eds.), Relations and Kleene algebra in Computer Science — PhD Programme. Technical Report 2008-04, Institute of Computer Science, University of Augsburg, 68-72, 2008.
   abstract | pdf | bibtex

   Abstract:

   To realise a software that needs to interact with other com- puters, service-oriented architecture and especially Web Services are gain- ing more and more attention. Existing components need to be composed in order to reach a predefined goal. For Web Services this can be realised using data defined in WSDL or using semantic Web Services such as SAWSDL. We apply relation algebra to describe Web Services as well as the composition of existing semantic Web Services.
   @misc{Hoefner2008-8,
       Author = {Lautenbacher, Florian and H{\"o}fner, Peter},
       Title = {Towards an Algebraic Composition of Semantic Web Services},
       Editor = {Berghammer, Rudolf and M{\"o}ller, Bernhard and Struth, Georg},
       BookTitle = {Relations and Kleene algebra in Computer Science (RelMiCS10/AKA5) — PhD Programme},
       Series = {Technical Report 2008-04, Institute of Computer Science, University of Augsburg},
       Pages = {68-72},
       Year = {2008}
   }
5. P. Höfner: Proof Automation in Kleene Algebra. In W. Dosch, C. Grelck, A. Stümpel (eds.), 14. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS'07). Technical Report A-07-07, Schriftenreihe A, Institutes for Computer Science and Mathematics, University of Lübeck, 87-92, 2007.
   abstract | pdf | bibtex

   Abstract:

   It has often been claimed that model checking, special purpose automated deduction or interactive theorem proving are needed for formal program development. Recently, it has been demonstrated that off-the-shelf automated proof and counterexample search is an interesting alternative if combined with the right domain model. Furthermore it has been shown that variants of Kleene algebra might provide light-weight formal methods with heavy-weight automation. In this paper we give a brief overview of a number of program analysis and computer mathematics tasks where (variants of) Kleene algebra combined with automated theorem provers are already applied.
   @misc{Hoefner2007-6,
       Author = {Dang, Han Hing and H{\"o}fner, Peter},
       Title = {First-Order Theorem Prover Evaluation w.r.t. Relation- and {K}leene Algebra},
       Editor = {Berghammer, Rudolf and M{\"o}ller, Bernhard and Struth, Georg},
       BookTitle = {Relations and Kleene algebra in Computer Science (RelMiCS10/AKA5) — PhD Programme},
       Series = {Technical Report 2008-04, Institute of Computer Science, University of Augsburg},
       Pages = {48-52},
       Year = {2008}
   }
6. P. Höfner: f-Generated Kleene Algebra. In R.A. Schmidt, G. Struth (eds.), Relations and Kleene algebra in Computer Science — PhD Programme. Technical Report CS-06-09, University of Sheffield, 55-59, 2006.
   abstract | pdf | bibtex

   Abstract:

   When describing iterations or loops it is well known and common to use the Kleene star. We first show an example for iteration, where the star operation is not adequate, since it just iterate and do not modify the iterated element. Therefore we introduce, as a generalisation of Kleene algebra, the structure of f-generated Kleene algebra, that have an iteration operation which depends on a function f and modify the iterated element in each step.
   @misc{Hoefner2006-10,
       Author = {H{\"o}fner, Peter},
       Title = {$f$-Generated Kleene Algebra},
       Editor = {Schmidt, Renate and Struth, Georg},
       BookTitle = {Relations and Kleene algebra in Computer Science (RelMiCS/AKA 2006) — PhD Programme},
       Series = {Technical Report CS-06-09, Department of Computer Science, University of Sheffield},
       Pages = {55-59},
       Year = {2006}
   }
7. P. Höfner: Semiring Neighbours: An Algebraic Embedding and Extension of Neighbourhood Logic. In J. Romijn, G. Smith, J. van de Pol (eds.), IFM2005—Doctoral Symposium on Integrated Formal Methods. Computer Science Reports 05-29, TU/e technische universiteit eindhoven, 6-13, 2005.
   abstract | pdf | bibtex

   Abstract:

   In 1996 Zhou and Hansen proposed a first-order interval logic called Neighbourhood Logic (NL) for specifying liveness and fairness of computing systems and also defining notions of real analysis in terms of expanding modalities. After that, Roy and Zhou presented a sound and relatively complete Duration Calculus as an extension of NL.
   We present an embedding of NL into an idempotent semiring of intervals. This embedding allows us to extend NL from single intervals to sets of intervals as well as to extend the approach to arbitrary idempotent semirings. We show that most of the required properties follow directly from Galois connections, hence we get the properties for free. As one important result we get that some of the axioms which were postulated for NL can be dropped since they are theorems in our generalisation. At the end of the paper we shortly present some possible applications for neighbours beyond intervals. Here we discuss for example reachability in graphs and applications for hybrid systems.
   @misc{Hoefner2005-6,
       Author = {H{\"o}fner, Peter},
       Title = {Semiring Neighbours: An Algebraic Embedding and Extension of {Neighbourhood Logic}},
       Editor = {Romijn, Judi and Smith, Graeme and van~de~Pol, Jaco},
       BookTitle = {IFM2005—Doctoral Symposium on Integrated Formal Methods},
       Series = {Computer Science Reports 05-29, TU/e technische universiteit eindhoven},
       Pages = {6-13},
       Year = {2005}
   }
8. P. Höfner: An Algebraic Semantics for Duration Calculus. In J. Gervain (ed.), Tenth ESSLLI Student Session. 99-110, 2005.
   abstract | pdf | bibtex

   Abstract:

   We present an algebraic semantics for Duration Calculus based on semirings and quantales. Duration Calculus was originally introduced in 1991 as a powerful logic for specifying the safety of real-time systems. We embed the Duration Calculus into the theory of Boolean semirings and extendpand them to Kleene algebra and ω-algebra, respectively, to express finite and infinite iteration. This allows us to calculate easily with the safety requirements and to see special results of the Duration Calculus in a more general context. When formulating an algebraic semantics we also generalise parts of von Karger's work about reactive systems, especially, the engineer's induction.
   @misc{Hoefner2005-4,
       Author = {H{\"o}fner, Peter},
       Title = {An Algebraic Semantics for {Duration Calculus}},
       Editor = {Gervain, Judit},
       BookTitle = {Tenth ESSLLI Student Session},
       Pages = {1-10},
       Year = {2005}
   }
9. P. Höfner: Von sequentieller Algebra zu Kleene-Algebra: Intervalloperatoren and Zeitdauer-Kalkül. Master's Thesis (Diplomarbeit), Universität Augsburg, 2003.
   abstract | pdf | bibtex

   Abstract:

   Der Zeitdauer-Kalkül (Duration Calculus, DC) ist ein formales, algebraisches System für die Spezifikation und das Design eines Echtzeit-Sicherheitssystems. Seit seiner ersten Erwähnung im Jahr 1991 durch Z. Chaochen, C.A.R. Hoare und A.P. Ravn wurde er mehrfach unter verschiedensten Aspekten betrachtet. In der ursprünglichen Version gingen die Autoren von temporaler Logik aus und stellten durch den Zeitdauer-Kalkül eine Verknüpfung zu Sicherheitssystemen und Intervallen her. M.R. Hansen und Z. Chaochen zeigten 1997, dass der Zeitdauer-Kalkül die Intervall-Logik (IL) in gewisser Weise erweitert. Auch wurde häufig der Zusammenhang zwischen DC und linearer temporaler Logik (Linear Temporal Logic, LTL) betrachtet. In den meisten dieser Schriften wird das Beispiel der Gasleitung mit einem Leck (gas burner example) dargestellt. Es beruht ebenfalls auf dem Artikel von Z. Chaochen et al. B. von Karger betrachtet den Zeitdauer-Kalkül unter dem Aspekt der Einbettung in sequentielle Algebren. Er führt zudem erstmalig den Begriff der Ingenieurs-Induktion (Engeneer's induction) ein. Unabhängig hiervon existiert die algebraische Struktur der Kleene-Algebra (KA). Diese erweitert Halbringe um einen weiteren unären Operator, den Kleene-Stern. Kleene-Algebren wurden schon auf vielfältigste Weise untersucht. So bewies beispielsweise D. Kozen viele ihrer grundlegenden Eigenschaften. Auch B. Möller und J. Desharnais lieferten viele Resultate über Kleene-Algebren, ihre Eigenschaften und Algorithmen auf ihnen. Einen ersten Schritt zur Verknüpfung dieser beiden Ideen (KA und DC) lieferte im Jahr 2000 C. Dima. Er entwickelte hierzu eine Kleene-Algebra über der Potenzmenge der positiven reellen Zahlen. (Die dort dargestellte Kleene-Algebra unterscheidet sich gegenüber der von D. Kozen vorgestellten Definition in der Art, dass diese Struktur nicht additiv idempotent ist.). Weiterhin zeigte er, dass die reellen Zahlen bei zeit-theoretischen Überlegungen, wie sie für den Zeitdauer-Kalkül benötigt werden, eine zentrale Rolle spielen. Ziel dieser Arbeit soll es sein, den Zeitdauer-Kalkül auf der Grundlage von Kleene-Algebren zu analysieren und zu präsentieren.
   @misc{Hoefner2003-1,
       Author = {H{\"o}fner, Peter},
       Title = {{Von sequentieller Algebra zu Kleene-Algebra: Intervalloperatoren und Zeitdauer-Kalk\"ul}},
       School = {Universit\"at Augsburg},
       Year = {2003},
       Address = {Universit\"at Augsburg, Institut f\"ur Informatik}
   }