Publications
Below is a complete listing of all publications of Peter Höfner.
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

P. Höfner:
Algebraic Calculi for Hybrid Systems. Books on Demand, 2009. isbn: 9783839125106 (Phd Thesis)
details
 bibtex
@Book{Hoefner20095,
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

P. Höfner:
Using Process Algebra to Design Better Protocols. In The Role and Importance of Mathematics in Innovation, Mathematics for Industry 25:87101, Springer, 2016.
doi: 10.1007/9789811009624_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 penandpaper analysis, model checking and interactive theorem proving has helped to perform a formal analysis of the Ad hoc OnDemand Vector (AODV) routing protocol.
@InBook{Hoefner201611,
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 = {87101},
Publisher = {Springer},
Year = {2016},
Doi = {10.1007/9789811009624_8}
}
Articles in Journals

R.J. van Glabbeek, P. Höfner:
Progress, Justness and Fairness. In ACM Computing Surveys, ACM, 2019. (accepted)
arXiv: CoRR abs/1810.07414
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{Hoefner20192,
Author = {van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {Progress, Justness and Fairness},
Journal = {ACM Computing Surveys},
Year = {2019},
Publisher = {ACM},
}

R. Berghammer, N. Danilenko, P. Höfner, I. Stucke:
Cardinality of Relations with Applications. In Discrete Mathematics 339(12):30893115, 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 mappingrelated 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{Hoefner20169,
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 = {30893115},
Year = {2016},
Publisher = {Elsevier},
Doi = {10.1016/j.disc.2016.06.019}
}

T. Bourke, R.J. van Glabbeek, P. Höfner:
Mechanizing a Process Algebra for Network Protocols. In Journal of Automated Reasoning 56(3):309341, Springer, 2016.
doi: 10.1007/s1081701593589
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{Hoefner20166,
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 = {309341},
Year = {2016},
Publisher = {Springer},
Doi = {10.1007/s1081701593589}
}

R.J. van Glabbeek, P. Höfner, M. Portmann, W.L. Tan:
Modelling and Verifying the AODV Routing Protocol. In Distributed Computing 29(4):279315, Springer, 2016.
arXiv: CoRR abs/1512.08867  doi: 10.1007/s0044601502627
abstract  pdf  bibtex
Abstract:
This paper presents a formal specification of the Ad hoc OnDemand 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{Hoefner20163,
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 = {279315},
Year = {2016},
Publisher = {Springer},
Doi = {10.1007/s0044601502627}
}

P. Höfner, B. Möller:
Extended Feature Algebra. In Journal of Logic and Algebraic Methods in Programming 85(5):952971, 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 featureoriented software development. One goal is to provide a common, clearly defined basis for the key ideas of featureorientation. The algebra captures major aspects of featureorientation, 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 featureoriented 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 featureorientation 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{Hoefner20162,
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 = {952971},
Year = {2016},
Publisher = {Elsevier},
Doi = {10.1016/j.jlamp.2015.12.002}
}

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):269286, 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 assertionbased method and relationalgebraic calculations.
@article{Hoefner20161,
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 = {269286},
Year = {2016},
Publisher = {Elsevier},
Doi = {10.1016/j.jlamp.2015.12.001}
}

R.J. van Glabbeek, P. Höfner:
CCS: It's not Fair!—Fair Schedulers cannot be implemented in CCSlike languages even under progress and certain fairness assumptions. In Acta Informatica 52(23):175205, Springer, 2015.
arXiv: CoRR abs/1505.05964  doi: 10.1007/s0023601502216
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 processalgebraic 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{Hoefner20152,
Author = {van Glabbeek, R.J. and H{\"o}fner, P.},
Title = {CCS: It's not Fair!Fair Schedulers cannot be implemented in CCSlike languages even under progress and certain fairness assumptions},
Journal = {Acta Informatica},
Number = {23},
Volume = {52},
Pages = {175205},
Year = {2015},
Publisher = {Springer},
Doi = {10.1007/s0023601502216}
}

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:291311, Springer, 2015.
doi: 10.1007/9783319155456_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 FeatureOriented Software Development (FOSD) tooling.
@article{Hoefner20151,
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 = {291311},
Year = {2015},
Publisher = {Springer},
Doi = {10.1007/9783319155456_19}
}

P. Höfner, A. McIver:
Hopscotch—Reaching the Target Hop by Hop. In Journal of Logic and Algebraic Methods in Programming 83(2):212224, 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 minplus 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{Hoefner20142,
Author = {H{\"o}fner, P. and McIver, A.},
Title = {HopscotchReaching the Target Hop by Hop},
Journal = {Journal of Logic and Algebraic Methods in Programming},
Number = {2},
Volume = {83},
Pages = {212224},
Year = {2014},
Publisher = {Elsevier},
Doi = {10.1016/j.jlap.2014.02.009}
}

P. Höfner, B. Möller:
Dijkstra, Floyd and Warshall meet Kleene. In Formal Aspects of Computing 24(46):459476, Springer, 2012.
doi: 10.1007/s0016501202454
abstract  pdf  bibtex
Abstract:
Around 1960, Dijkstra, Floyd and Warshall published papers on algorithms for solving singlesource and allsources 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{Hoefner20124,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {Dijkstra, Floyd and Warshall meet Kleene},
Journal = {Formal Aspects of Computing},
Number = {46},
Volume = {24},
Pages = {459476},
Year = {2012},
Publisher = {Springer},
Doi = {10.1007/s0016501202454}
}

P. Höfner, R.J. van Glabbeek, I.J. Hayes:
Morgan: a suitable case for treatment (Preface). In Formal Aspects of Computing 24(46):417422, Springer, 2012. (Festschrift in Honour of Carroll Morgan)
doi: 10.1007/s0016501202570
abstract  pdf  bibtex
Abstract:
This triple issue of Formal Aspects of Computing constitutes a Festschrift dedicated to Professor Charles Carroll Morgan, on the occasion of his sixtieth birthday. The Festschrift consists of an invited paper and 23 scientific research papers, all related to Carroll's own research interests. Three of these papers could not be included in these issues due to space limitations. They are available hard copy in a later issue of the journal.
@article{Hoefner20123,
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 = {46},
Volume = {24},
Pages = {417422},
Year = {2012},
Publisher = {Springer},
Doi = {10.1007/s0016501202570}
}

P. Höfner, B. Möller:
Fixing Zeno Gaps. In Theoretical Computer Science 412(28):33033322, 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{Hoefner20116,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {Fixing Zeno Gaps},
Journal = {Theoretical Computer Science},
Number = {28},
Volume = {412},
Pages = {33033322},
Year = {2011},
Publisher = {Elsevier},
Doi = {j.tcs.2011.03.018}
}

P. Höfner, R. Khedri, B. Möller:
Supplementing Product Families with Behaviour. In International Journal of Software and Informatics 5(12):245266, 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 FODAlike 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 streambased semantics.
@article{Hoefner20113,
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 = {12},
Volume = {5},
Pages = {245266},
Year = {2011},
Publisher = {Institute of Software, Chinese Academy of Sciences},
}

H.H. Dang, P. Höfner, B. Möller:
Algebraic Separation Logic. In Journal of Logic and Algebraic Programming 80(6):221247, 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 firstorder and hence enables the use of offtheshelf automated theorem provers for verifying properties at an abstract level.
@article{Hoefner20112,
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 = {221247},
Year = {2011},
Publisher = {Elsevier},
Doi = {10.1016/j.jlap.2011.04.003}
}

P. Höfner, R. Khedri, B. Möller:
An Algebra of Product Families. In Software & Systems Modeling 10(2):161182, Springer, 2011.
doi: 10.1007/s1027000901272
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 wellidentified 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 multiview 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{Hoefner20111,
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 = {161182},
Year = {2011},
Publisher = {Springer},
Doi = {10.1007/s1027000901272}
}

P. Höfner, G. Struth:
Algebraic Notions of Nontermination: Omega and Divergence in Idempotent Semirings. In Journal of Logic and Algebraic Programming 79(8):794811, 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{Hoefner20101,
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 = {794811},
Year = {2010},
Publisher = {Springer},
Doi = {10.1016/j.jlap.2010.07.016}
}

P. Höfner, G. Struth, G. Sutcliffe:
Automated Verification of Refinement Laws. In Annals of Mathematics and Artificial Intelligence 55(12):3562, Springer, 2009.
doi: 10.1007/s1047200991518
abstract  pdf  bibtex
Abstract:
Demonic refinement algebras are variants of Kleene algebras. Introduced by von Wright as a lightweight variant of the refinement calculus, their intended semantics are positively disjunctive predicate transformers, and their calculus is entirely within firstorder equational logic. So, for the first time, offtheshelf 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{Hoefner20092,
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 = {12},
Volume = {55},
Pages = {3562},
Year = {2009},
Publisher = {Springer},
Doi = {10.1007/s1047200991518}
}

P. Höfner, B. Möller:
An Algebra of Hybrid Systems. In Journal of Logic and Algebraic Programming 78(2):7497, 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 trajectorybased 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{Hoefner20091,
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 = {7497},
Year = {2009},
Publisher = {Springer},
Doi = {10.1016/j.jlap.2008.08.005}
}

P. Höfner, B. Möller:
Algebraic Neighbourhood Logic. In Journal of Logic and Algebraic Programming 76(1):3559, 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{Hoefner20083,
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 = {3559},
Year = {2008},
Publisher = {Springer},
Doi = {10.1016/j.jlap.2007.10.004}
}

P. Höfner, G. Struth:
Can Refinement be Automated?. In Electronic Notes in Theoretical Computer Science 201:197222, 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{Hoefner20082,
Author = {H{\"o}fner, P. and Struth, G.},
Title = {Can Refinement be Automated?},
Journal = {Electronic Notes in Theoretical Computer Science},
Volume = {201},
Pages = {197222},
Year = {2008},
Publisher = {Elsevier},
Doi = {10.1016/j.entcs.2008.02.021}
}

P. Höfner, F. Lautenbacher:
Algebraic Structure of Web Services. In Electronic Notes in Theoretical Computer Science 200(3):171187, Elsevier, 2008.
doi: 10.1016/j.entcs.2008.04.099
abstract  pdf  bibtex
Abstract:
Web Services and ServiceOriented 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{Hoefner20081,
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 = {171187},
Year = {2008},
Publisher = {Elsevier},
Doi = {10.1016/j.entcs.2008.04.099}
}

P. Höfner:
Semiring Neighbours: An Algebraic Embedding and Extension of Neighbourhood Logic. In Electronic Notes in Theoretical Computer Science 191:4972, Elsevier, 2007.
doi: 10.1016/j.entcs.2006.09.040
abstract  pdf  bibtex
Abstract:
In 1996 Zhou and Hansen proposed a firstorder 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{Hoefner20071,
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 = {4972},
Year = {2007},
Publisher = {Elsevier},
Doi = {10.1016/j.entcs.2006.09.040}
}
Papers in Conference and Workshop Proceedings

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'19). Lecture Notes in Computer Science 11423, Springer, 2019.
doi: 10.1007/9783030171841_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 CarrierSense 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{Hoefner20193,
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'19)},
Editor = {Caires, L.},
Series = {Lecture Notes in Computer Science},
Volume = {11423},
Pages = {00},
Year = {2019},
Publisher = {Springer},
Doi = {10.1007/9783030171841_24}
}

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 '18). Lecture Notes in Computer Science 11194, pp. 263279, Springer, 2018.
doi: 10.1007/9783030021498_16
abstract  pdf  bibtex
Abstract:
Separation logic, an extension of FloydHoare 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{Hoefner20184,
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 '18)},
Editor = {Desharnais, J. and Guttmann, W. and Joosten, S.},
Series = {Lecture Notes in Computer Science},
Volume = {11194},
Pages = {263279},
Year = {2018},
Publisher = {Springer},
Doi = {10.1007/9783030021498_16}
}

R.J. van Glabbeek, P. Höfner, D. van der Wal:
Analysing AWNspecifications using mCRL2 (extended abstract). In C.A. Furia, K. Winter (eds.), Integrated Formal Methods (iFM 2018). Lecture Notes in Computer Science 11023, pp. 398418, Springer, 2018.
doi: 10.1007/9783319989389_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 AWNspecifications. 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{Hoefner20183,
Author = {van Glabbeek, R.J. and H{\"o}fner, P. and van der Wal, D.},
Title = {Analysing AWNspecifications 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 = {398418},
Year = {2018},
Publisher = {Springer},
Doi = {10.1007/9783319989389_23}
}

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. 6887, Springer, 2018.
doi: 10.1007/9783319948218_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{Hoefner20182,
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 = {6887},
Year = {2018},
Publisher = {Springer},
Doi = {10.1007/9783319948218_5}
}

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, 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 counterintuitive. 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{Hoefner20176,
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 = {00},
Year = {2017},
Publisher = {Open Publishing Association},
Doi = {10.4204/EPTCS.255.2}
}

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. 1452, 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 inbuilt mechanism for prioritisation, we argue that this is not sufficient and provide another protocol to overcome this shortcoming.
@InProceedings{Hoefner20173,
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 = {1452},
Year = {2017},
Publisher = {Open Publishing Association},
Doi = {10.4204/EPTCS.244.2}
}

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'16). Lecture Notes in Computer Science 9632, pp. 95122, Springer, 2016.
doi: 10.1007/9783662494981_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 OnDemand 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{Hoefner20167,
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'16)},
Editor = {},
Series = {Lecture Notes in Computer Science},
Volume = {9632},
Pages = {95122},
Year = {2016},
Publisher = {Springer},
Doi = {10.1007/9783662494981_5}
}

P. Höfner:
Using Process Algebra to Design Better Protocol (extended abstract); invited. In Forum "MathforIndustry" 2015  The Role and Importance of Mathematics in Innovation (FMI '15). MI Lecture Notes 65, Kyushu University, 2015.
pdf  bibtex
Abstract:
@InProceedings{Hoefner20158,
Author = {H{\"o}fner, P.},
Title = {Using Process Algebra to Design Better Protocol (extended abstract); invited},
BookTitle = {Forum "MathforIndustry" 2015  The Role and Importance of Mathematics in Innovation (FMI '15)},
Editor = {},
Series = {MI Lecture Notes},
Volume = {65},
Pages = {00},
Year = {2015},
Publisher = {Kyushu University},
Doi = {}
}

R. Berghammer, P. Höfner, I. Stucke:
ToolBased Verification of a Relational Vertex Coloring Program. In W. Kahl, J.N. Oliveira, M. Winter (eds.), Relational and Algebraic Methods in Computer Science (RAMiCS '15). Lecture Notes in Computer Science 9348, pp. 275292, Springer, 2015.
doi: 10.1007/9783319247045_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 whileprogram for computing a vertex coloring of an undirected (loopfree) graph. For showing its correctness, we then combine the wellknown assertionbased verification method with relationalgebraic calculations. Based on this, we show how automatically to test loopinvariants 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 offtheshelf theorem provers, but also reveal some shortcomings and difficulties with theorem provers that are nowadays available.
@InProceedings{Hoefner20156,
Author = {Berghammer, R. and H{\"o}fner, P. and Stucke, I.},
Title = {ToolBased Verification of a Relational Vertex Coloring Program},
BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS '15)},
Editor = {Kahl, W. and Oliveira, J.N. and Winter, M.},
Series = {Lecture Notes in Computer Science},
Volume = {9348},
Pages = {275292},
Year = {2015},
Publisher = {Springer},
Doi = {10.1007/9783319247045_17}
}

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. 175189, Springer, 2015.
doi: 10.1007/9783319229690_13
abstract  pdf  bibtex
Abstract:
As (network) software is such an omnipresent component of contemporary missioncritical 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 adhoc 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{Hoefner20155,
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 = {175189},
Year = {2015},
Publisher = {Springer},
Doi = {10.1007/9783319229690_13}
}

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 '14). Lecture Notes in Computer Science 8837, pp. 4763, Springer, 2014.
arXiv: CoRR abs/1505.05646  doi: 10.1007/9783319119366_5
abstract  pdf  bibtex
Abstract:
The Ad hoc Ondemand 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 penandpaper 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 reestablish most proof obligations automatically and identify exactly the steps that are no longer valid.
@InProceedings{Hoefner20145,
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 '14)},
Editor = {Cassez, F. and Raskin, J.F.},
Series = {Lecture Notes in Computer Science},
Volume = {8837},
Pages = {4763},
Year = {2014},
Publisher = {Springer},
Doi = {10.1007/9783319119366_5}
}

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 '14). Lecture Notes in Computer Science 8558, pp. 144159, Springer, 2014.
arXiv: CoRR abs/1407.3519  doi: 10.1007/9783319089706_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{Hoefner20143,
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 '14)},
Editor = {Klein, G. and Gamboa, R.},
Series = {Lecture Notes in Computer Science},
Volume = {8558},
Pages = {144159},
Year = {2014},
Publisher = {Springer},
Doi = {10.1007/9783319089706_10}
}

R. Berghammer, P. Höfner, I. Stucke:
Automated Verification of Relational WhilePrograms. In P. Höfner, P. Jipsen, W. Kahl, M.E. Müller (eds.), Relational and Algebraic Methods in Computer Science (RAMiCS '14). Lecture Notes in Computer Science 8428, pp. 173190, Springer, 2014.
doi: 10.1007/9783319062518_11
abstract  pdf  bibtex
Abstract:
Software verification is essential for safetycritical systems. In this paper, we illustrate that some verification tasks can be done fully automatically. We show how to automatically verify imperative programs for relationbased discrete structures by combining relation algebra and the wellknown assertionbased verification method with automated the orem proving. We present two examples in detail: a relational program for determining the reflexivetransitive closure and a topological sorting algorithm. We also treat the automatic verification of the equivalence of commonlogical and relationalgebraic specifications.
@InProceedings{Hoefner20141,
Author = {Berghammer, R. and H{\"o}fner, P. and Stucke, I.},
Title = {Automated Verification of Relational WhilePrograms},
BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS '14)},
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 = {173190},
Year = {2014},
Publisher = {Springer},
Doi = {10.1007/9783319062518_11}
}

D. Batory, P. Höfner, B. Möller, A. Zelend:
Features, Modularity, and Variation Points. In Workshop on FeatureOriented Software Development (FOSD'13). pp. 916, 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{Hoefner20136,
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 FeatureOriented Software Development (FOSD'13)},
Editor = {},
Series = {},
Volume = {0},
Pages = {916},
Year = {2013},
Publisher = {ACM},
Doi = {10.1145/2528265.2528269}
}

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'13). pp. 91100, ACM, 2013.
arXiv: CoRR abs/1512.08891  doi: 10.1145/2507924.2507943
abstract  pdf  bibtex
Abstract:
In the area of mobile adhoc 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 OnDemand 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. AODVbased 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 nonevident assumptions to be made when resolving ambiguities occurring in the RFC. Thus, monotonically increasing sequence numbers, by themselves, do not guarantee loop freedom.
@InProceedings{Hoefner20135,
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'13)},
Editor = {},
Series = {},
Volume = {0},
Pages = {91100},
Year = {2013},
Publisher = {ACM},
Doi = {10.1145/2507924.2507943}
}

A. Fehnker, P. Höfner, M. Kamali, V. Mehta:
Topologybased Mobility Models for Wireless Networks. In L. Alvisi, D. Giannakopoulou (eds.), Quantitative Evaluation of Systems (QEST'13). Lecture Notes in Computer Science 8054, pp. 368383, Springer, 2013.
doi: 10.1007/9783642401961_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 topologybased 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 standalone 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 Adhoc On demand Distance Vector (AODV) routing protocol, and second we combine the mobility model with the Lightweight Medium Access Control (LMAC).
@InProceedings{Hoefner20133,
Author = {Fehnker, A. and H{\"o}fner, P. and Kamali, M. and Mehta, V.},
Title = {Topologybased Mobility Models for Wireless Networks},
BookTitle = {Quantitative Evaluation of Systems (QEST'13)},
Editor = {Alvisi, L. and Giannakopoulou, D.},
Series = {Lecture Notes in Computer Science},
Volume = {8054},
Pages = {368383},
Year = {2013},
Publisher = {Springer},
Doi = {10.1007/9783642401961_32}
}

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'13). Lecture Notes in Computer Science 8053, pp. 121136, Springer, 2013.
doi: 10.1007/9783642402296_9
abstract  pdf  bibtex
Abstract:
Wireless Mesh Networks (WMNs) are selforganising adhoc 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{Hoefner20134,
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'13)},
Editor = {Braberman, V. and Fribourg, L.},
Series = {Lecture Notes in Computer Science},
Volume = {8053},
Pages = {121136},
Year = {2013},
Publisher = {Springer},
Doi = {10.1007/9783642402296_9}
}

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'13). Lecture Notes in Computer Science 7871, pp. 322336, Springer, 2013.
doi: 10.1007/9783642380884_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 SMCUppaal. In this paper we illustrate this by a quantitative analysis of two wellknown 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{Hoefner20132,
Author = {H{\"o}fner, P. and McIver, A.},
Title = {Statistical Model Checking of Wireless Mesh Routing Protocols},
BookTitle = {NASA Formal Methods Symposium (NFM'13)},
Editor = {Brat, G. and Rungta, N. and Venet, A.},
Series = {Lecture Notes in Computer Science},
Volume = {7871},
Pages = {322336},
Year = {2013},
Publisher = {Springer},
Doi = {10.1007/9783642380884_22}
}

S. Edenhofer, P. Höfner:
Towards a Rigorous Analysis of AODVv2 (DYMO). In N. Foster, A. Gurney (eds.), Rigorous Protocol Engineering (WRiPE'12). IEEE, 2012.
doi: 10.1109/ICNP.2012.6459942
abstract  pdf  bibtex
Abstract:
Dynamic MANET Ondemand (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 ondemand fashion.
In this paper we present a formal model of AODVv2, using the process algebra AWN. The benefit of this is twofold: (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 nonoptimal 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{Hoefner20125,
Author = {Edenhofer, S. and H{\"o}fner, P.},
Title = {Towards a Rigorous Analysis of AODVv2 (DYMO)},
BookTitle = {Rigorous Protocol Engineering (WRiPE'12)},
Editor = {Foster, N. and Gurney, A.},
Series = {},
Volume = {0},
Pages = {00},
Year = {2012},
Publisher = {IEEE},
Doi = {10.1109/ICNP.2012.6459942}
}

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'12). pp. 203212, 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 OnDemand 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{Hoefner20127,
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'12)},
Editor = {},
Series = {},
Volume = {0},
Pages = {203212},
Year = {2012},
Publisher = {ACM},
Doi = {10.1145/2387238.2387274}
}

P. Höfner, B. Möller, A. Zelend:
Foundations of Coloring Algebra with Consequences for Featureoriented Programming. In W. Kahl, T. Griffin (eds.), Relational and Algebraic Methods in Computer Science (RAMiCS 12). Lecture Notes in Computer Science 7560, pp. 3349, Springer, 2012.
doi: 10.1007/9783642333149_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 settheoretic models.
@InProceedings{Hoefner20126,
Author = {H{\"o}fner, P. and M{\"o}ller, B. and Zelend, A.},
Title = {Foundations of Coloring Algebra with Consequences for Featureoriented Programming},
BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 12)},
Editor = {Kahl, W. and Griffin, T.},
Series = {Lecture Notes in Computer Science},
Volume = {7560},
Pages = {3349},
Year = {2012},
Publisher = {Springer},
Doi = {10.1007/9783642333149_3}
}

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). Lecture Notes in Computer Science 7211, pp. 295315, Springer, 2012.
doi: 10.1007/9783642288692_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 Adhoc OnDemand Distance Vector (AODV) routing protocol and (dis)prove crucial properties such as loop freedom and packet delivery.
@InProceedings{Hoefner20122,
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)},
Editor = {Seidl, H.},
Series = {Lecture Notes in Computer Science},
Volume = {7211},
Pages = {295315},
Year = {2012},
Publisher = {Springer},
Doi = {10.1007/9783642288692_15}
}

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'12). Lecture Notes in Computer Science 7214, pp. 173187, Springer, 2012.
arXiv: CoRR abs/1512.07352  doi: 10.1007/9783642287565_13
abstract  pdf  bibtex
Abstract:
This paper describes an automated, formal and rigorous analysis of the Ad hoc OnDemand 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 processalgebraic 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 formalmethodsbased protocol modelling and verification techniques, such as process algebra.
@InProceedings{Hoefner20121,
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'12)},
Editor = {Flanagan, C. and K{\"o}nig, B.},
Series = {Lecture Notes in Computer Science},
Volume = {7214},
Pages = {173187},
Year = {2012},
Publisher = {Springer},
Doi = {10.1007/9783642287565_13}
}

D. Batory, P. Höfner, J. Kim:
Feature Interactions, Products, and Composition. In Generative Programming and Component Engineering (GPCE'11). pp. 1322, ACM, 2011.
doi: 10.1145/2047862.2047867
abstract  pdf  bibtex
Abstract:
The relationship between feature modules and feature interactions is not wellunderstood. To explain classic examples of feature interaction, we show that features are not only composed sequentially, but also by crossproduct 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 backpropagated to their original feature module definitions, thereby improving FOSD tooling.
@InProceedings{Hoefner20118,
Author = {Batory, D. and H{\"o}fner, P. and Kim, J.},
Title = {Feature Interactions, Products, and Composition},
BookTitle = {Generative Programming and Component Engineering (GPCE'11)},
Editor = {},
Series = {},
Volume = {0},
Pages = {1322},
Year = {2011},
Publisher = {ACM},
Doi = {10.1145/2047862.2047867}
}

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). 2011.
abstract  pdf  bibtex
Abstract:
This paper describes work in progress towards an automated formal and rigorous analysis of the Ad hoc OnDemand 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{Hoefner20117,
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)},
Editor = {},
Series = {},
Volume = {0},
Pages = {00},
Year = {2011},
Publisher = {},
Doi = {}
}

P. Höfner, A. McIver:
Towards an Algebra of Routing Tables. In H. de Swart (ed.), Relational and Algebraic Methods in Computer Science (RAMiCS 11). Lecture Notes in Computer Science 6663, pp. 212229, Springer, 2011.
doi: 10.1007/9783642210709_17
abstract  pdf  bibtex
Abstract:
We use wellknown 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{Hoefner20115,
Author = {H{\"o}fner, P. and McIver, A.},
Title = {Towards an Algebra of Routing Tables},
BookTitle = {Relational and Algebraic Methods in Computer Science (RAMiCS 11)},
Editor = {de Swart, H.},
Series = {Lecture Notes in Computer Science},
Volume = {6663},
Pages = {212229},
Year = {2011},
Publisher = {Springer},
Doi = {10.1007/9783642210709_17}
}

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 11). Lecture Notes in Computer Science 6663, pp. 125140, Springer, 2011.
doi: 10.1007/9783642210709_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 metalanguage, 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{Hoefner20114,
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 11)},
Editor = {de Swart, H.},
Series = {Lecture Notes in Computer Science},
Volume = {6663},
Pages = {125140},
Year = {2011},
Publisher = {Springer},
Doi = {10.1007/9783642210709_11}
}

H.H. Dang, P. Höfner:
Automated Higherorder Reasoning about Quantales. In B. Konev, R.A. Schmidt, S. Schulz (eds.), Workshop on Practical Aspects of Automated Reasoning (PAAR'10). EasyChair Proceedings in Computing 9, pp. 4051, 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 higherorder logic. In particular, we give an encoding of quantales in the typed higherorder 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{Hoefner20102,
Author = {Dang, H.H. and H{\"o}fner, P.},
Title = {Automated Higherorder Reasoning about Quantales},
BookTitle = {Workshop on Practical Aspects of Automated Reasoning (PAAR'10)},
Editor = {Konev, B. and Schmidt, R.A. and Schulz, S.},
Series = {EasyChair Proceedings in Computing},
Volume = {9},
Pages = {4051},
Year = {2010},
Publisher = {EasyChair},
Doi = {}
}

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 FeatureOriented Software Development (FOSD'09). pp. 7580, 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{Hoefner20094,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {An Extension of Feature Algebra [Extended Abstract]},
BookTitle = {Workshop on FeatureOriented 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 = {7580},
Year = {2009},
Publisher = {ACM},
Doi = {10.1145/1629716.1629731}
}

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. 5972, Springer, 2009.
doi: 10.1007/9783642046391_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{Hoefner20093,
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 = {5972},
Year = {2009},
Publisher = {Springer},
Doi = {10.1007/9783642046391_5}
}

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. 8594, 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{Hoefner20087,
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 = {8594},
Year = {2008},
Publisher = {IEEE},
Doi = {10.1109/SEFM.2008.36}
}

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. 5066, Springer, 2008.
doi: 10.1007/9783540710707_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 offtheshelf 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{Hoefner20086,
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 = {5066},
Year = {2008},
Publisher = {Springer},
Doi = {10.1007/9783540710707_5}
}

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. 191205, Springer, 2008.
doi: 10.1007/9783540789130_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 offtheshelf automated theorem provers can be used to verify them.
@InProceedings{Hoefner20085,
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 = {191205},
Year = {2008},
Publisher = {Springer},
Doi = {10.1007/9783540789130_15}
}

P. Höfner, G. Struth:
Nontermination 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. 206220, Springer, 2008.
doi: 10.1007/9783540789130_16
abstract  pdf  bibtex
Abstract:
We study and compare two notions of nontermination 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{Hoefner20084,
Author = {H{\"o}fner, P. and Struth, G.},
Title = {Nontermination 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 = {206220},
Year = {2008},
Publisher = {Springer},
Doi = {10.1007/9783540789130_16}
}

P. Höfner, G. Struth:
Automated Reasoning in Kleene Algebra. In F. Pfenning (ed.), Automated Deduction (CADE21). Lecture Notes in Artificial Intelligence 4603, pp. 279294, Springer, 2007.
doi: 10.1007/9783540735953_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 offtheshelf 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 firstorder setting, crosstheory reasoning between standard formalisms and full automation of some (co)inductive arguments. Kleene algebras might therefore provide lightweight formal methods with heavyweight automation.
@InProceedings{Hoefner20072,
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 = {279294},
Year = {2007},
Publisher = {Springer},
Doi = {10.1007/9783540735953_19}
}

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. 207221, 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 semirings 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{Hoefner20069,
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 = {207221},
Year = {2006},
Publisher = {Springer},
Doi = {10.1007/11828563_14}
}

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. 222234, 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 predicatetransformer models extensionality always holds, this means that the axioms of demonic refinement algebra do not characterise predicatetransformer 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{Hoefner20068,
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 = {222234},
Year = {2006},
Publisher = {Springer},
Doi = {10.1007/11828563_15}
}

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. 300315, 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 wellidentified 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{Hoefner20065,
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 = {300315},
Year = {2006},
Publisher = {Springer},
Doi = {10.1007/11813040_21}
}

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. 263277, 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{Hoefner20064,
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 = {263277},
Year = {2006},
Publisher = {Springer},
Doi = {10.1007/11784180_21}
}

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. 121133, Springer, 2006.
doi: 10.1007/11734673_10
abstract  pdf  bibtex
Abstract:
We present a trajectorybased 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{Hoefner20062,
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 = {121133},
Year = {2006},
Publisher = {Springer},
Doi = {10.1007/11734673_10}
}

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. 498499, Springer, 2005.
doi: 10.1007/11551362_53
abstract  pdf  bibtex
Abstract:
Advanced personalization techniques are required to cope with novel challenges posed by attributerich 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 XMLbased 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{Hoefner20053,
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 = {498499},
Year = {2005},
Publisher = {Springer},
Doi = {10.1007/11551362_53}
}
Editorials

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. (in preparation)

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/9783319574189

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

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.

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.

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.

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/9783319062518

Festschrift in honour of Carroll Morgan. P. Höfner, R.J. van Glabbeek, I.J. Hayes (eds.), Formal Aspects of Computing 24(46). Springer, 2012.

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.

Proceedings of Workshop on Automated Theory Engineering (ATE 2011). P. Höfner, A. McIver, G. Struth (eds.), CEUR Proceedings Vol760. 2011.
Archive of Formal Proofs

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.isaafp.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{Hoefner201610,
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},
}

T. Bourke, P. Höfner:
Loop Freedom of the (Untimed) AODV Routing Protocol. In Archive of Formal Proofs, 2014. link: www.isaafp.org/entries/AODV.shtml
abstract  bibtex
Abstract:
The Ad hoc Ondemand 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 penandpaper 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 reestablish most proof obligations automatically and identify exactly the steps that are no longer valid.
@article{Hoefner20146,
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)

R. Berghammer, H. Hitoshi, W. Guttmann, P. Höfner:
Relational Characterisations of Paths. Technical Report. 2018.
arXiv: CoRR abs/1801.04026
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 pointwise 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 firstorder 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.
@Techreport{Hoefner20181,
Author = {Berghammer, R. and Hitoshi, H. and Guttmann, W. and H{\"o}fner, P.},
Title = {Relational Characterisations of Paths},
Institution = {},
Number = {},
Year = {2018},
Url = {}
}

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 OnDemand 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{Hoefner20168,
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}
}

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 processalgebraic 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{Hoefner20153,
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}
}

D. Batory, P. Höfner, B. Möller, A. Zelend:
Features, Modularity, and Variation Points. Technical Report TR2147, 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 featurebased SPLs.
@Techreport{Hoefner20137,
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 = {TR2147},
Year = {2013},
Url = {apps.cs.utexas.edu/tech_reports/reports/tr/TR2147.pdf}
}

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 Adhoc OnDemand Distance Vector (AODV) routing protocol. We give a complete specification of this widelyused 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 nonoptimal 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{Hoefner20131,
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}
}

P. Höfner, B. Möller, A. Zelend:
Foundations of Coloring Algebra with Consequences for FeatureOriented Programming. Technical Report 201206, 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 settheoretic models.
@Techreport{Hoefner201212,
Author = {H{\"o}fner, P. and M{\"o}ller, B. and Zelend, A.},
Title = {Foundations of Coloring Algebra with Consequences for FeatureOriented Programming},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {201206},
Year = {2012},
Url = {www.informatik.uniaugsburg.de/en/chairs/dbis/pmi/publications/all_pmi_techreports/tr201206_hoe_moe_zel.html}
}

P. Höfner, S. Mentl, B. Möller, W. Scholz:
Requirements in Feature Algebra. Technical Report 201012, Institute of Computer Science, University of Augsburg. 2010. direct link.
abstract  pdf  bibtex
Abstract:
eature 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{Hoefner20109,
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 = {201012},
Year = {2010},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr201012_hoe_men_moe_scholz/}
}

P. Höfner, R. Khedri, B. Möller:
Supplementing Product Families with Behaviour. Technical Report 201013, 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 andor trees of features as used in FeatureOriented 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 product 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 streambased semantics.
@Techreport{Hoefner20108,
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 = {201013},
Year = {2010},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr201013_hoe_khe_moe/}
}

P. Höfner, B. Möller:
Fixing Zeno Gaps. Technical Report 201011, 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{Hoefner20107,
Author = {H{\"o}fner, P. and M{\"o}ller, B.},
Title = {Fixing Zeno Gaps},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {201011},
Year = {2010},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr201011_hoe_moe/}
}

P. Höfner, M.E. Müller, S. Zeissler:
ATPPortal: A Userfriendly Webbased Interface for Automated Theorem Provers and for Automatically Generated Proofs. Technical Report 201010, 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 userfriendly webbased 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{Hoefner20106,
Author = {H{\"o}fner, P. and M{\"u}ller, M.E. and Zeissler, S.},
Title = {ATPPortal: A Userfriendly Webbased Interface for Automated Theorem Provers and for Automatically Generated Proofs},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {201010},
Year = {2010},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr201010_hoe_mue_zei/}
}

P. Höfner, B. Möller:
An Extension of Feature Algebra. Technical Report 201009, 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{Hoefner20105,
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 = {201009},
Year = {2010},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr201009_hoe_moe/}
}

H.H. Dang, P. Höfner, B. Möller:
Algebraic Separation Logic. Technical Report 201006, 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 firstorder and hence enables the use of offtheshelf automated theorem provers for verifying properties at a more abstract level.
@Techreport{Hoefner20104,
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 = {201006},
Year = {2010},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr201006_dan_hoe_moe/}
}

H.H. Dang, P. Höfner:
Automated HigherOrder Reasoning in Quantales. Technical Report 201003, 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 (noncommutative) 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 higherorder logic. In particular, we give an encoding of quantales in the typed higherorder 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{Hoefner20103,
Author = {Dang, H.H. and H{\"o}fner, P.},
Title = {Automated HigherOrder Reasoning in Quantales},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {201003},
Year = {2010},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr201003_dan_hoe/}
}

H.H. Dang, P. Höfner, B. Möller:
Towards Algebraic Separation Logic. Technical Report 200912, 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{Hoefner20096,
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 = {200912},
Year = {2009},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr200912_dan_hoe_moe/}
}

P. Höfner, G. Struth:
On Automating the Calculus of Relations. Technical Report CS0805, Department of Computer Science, University of Sheffield. 2008. 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 offtheshelf 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{Hoefner200810,
Author = {H{\"o}fner, P. and Struth, G.},
Title = {On Automating the Calculus of Relations},
Institution = {Department of Computer Science, University of Sheffield},
Number = {CS0805},
Year = {2008},
Url = {www.dcs.shef.ac.uk/intranet/research/public/resmes/CS0805.pdf}
}

P. Höfner, R. Khedri, B. Möller:
Algebraic View Reconciliation. Technical Report 200713, 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{Hoefner20078,
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 = {200713},
Year = {2007},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr200713_hoe_khe_moe/}
}

P. Höfner, F. Lautenbacher:
Algebraic Structure of Web Services. Technical Report 200712, Institute of Computer Science, University of Augsburg. 2007. direct link.
abstract  pdf  bibtex
Abstract:
The ServiceOriented 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{Hoefner20077,
Author = {H{\"o}fner, P. and Lautenbacher, F.},
Title = {Algebraic Structure of Web Services},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {200712},
Year = {2007},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr200712_hoe_lau/}
}

P. Höfner, B. Möller:
An Algebra of Hybrid Systems. Technical Report 200708, 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 trajectorybased 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{Hoefner20075,
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 = {200708},
Year = {2007},
Url = {www.informatik.uniaugsburg.de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr200708_hoe_moe/}
}

P. Höfner, G. Struth:
Can Refinement be Automated?. Technical Report CS0708, 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 offtheshelf 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{Hoefner20074,
Author = {H{\"o}fner, P. and Struth, G.},
Title = {Can Refinement be Automated?},
Institution = {Department of Computer Science, University of Sheffield},
Number = {CS0708},
Year = {2007},
Url = {www.dcs.shef.ac.uk/intranet/research/public/resmes/CS0708.pdf}
}

P. Höfner, G. Struth:
Automated Reasoning in Kleene Algebra. Technical Report CS0704, Department of Computer Science, University of Sheffield. 2007. direct link.
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 offtheshelf 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 firstorder setting, crosstheory reasoning between standard formalisms and full automation of some (co)inductive arguments. Kleene algebras might therefore provide lightweight formal methods with heavyweight automation.
@Techreport{Hoefner20073,
Author = {H{\"o}fner, P. and Struth, G.},
Title = {Automated Reasoning in Kleene Algebra},
Institution = {Department of Computer Science, University of Sheffield},
Number = {CS0704},
Year = {2007},
Url = {www.dcs.shef.ac.uk/intranet/research/public/resmes/CS0704.pdf}
}

P. Höfner, G. Struth:
Algebraic Notions of NonTermination. Technical Report CS0612, Department of Computer Science, University of Sheffield. 2006. direct link.
abstract  pdf  bibtex
Abstract:
We study and compare two notions of nontermination 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{Hoefner200611,
Author = {H{\"o}fner, P. and Struth, G.},
Title = {Algebraic Notions of NonTermination},
Institution = {Department of Computer Science, University of Sheffield},
Number = {CS0612},
Year = {2006},
Url = {www.dcs.shef.ac.uk/intranet/research/public/resmes/CS0612.pdf}
}

P. Höfner, B. Möller, K. Solin:
Omega Algebra, Demonic Refinement Algebra and Commands. Technical Report 200611, 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 predicatetransformer models extensionality always holds, this means that the axioms of demonic refinement algebra do not characterise predicatetransformer 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{Hoefner20067,
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 = {200611},
Year = {2006},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr200611_hoe_moe_sol/}
}

P. Höfner, B. Möller:
Lazy Semiring Neighbours and some Applications. Technical Report 200609, 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 semirings 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{Hoefner20066,
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 = {200609},
Year = {2006},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr20069_hoe_moe/}
}

B. Möller, P. Höfner, G. Struth:
Quantales and Temporal Logics. Technical Report 200606, 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{Hoefner20063,
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 = {200606},
Year = {2006},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr20066_moe_hoe_str/}
}

P. Höfner, R. Khedri, B. Möller:
Feature Algebra. Technical Report 200604, 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 wellidentified 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{Hoefner20061,
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 = {200604},
Year = {2006},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr20064_hoe_khe_moe/}
}

P. Höfner:
Semiring Neighbours. Technical Report 200519, Institute of Computer Science, University of Augsburg. 2005. direct link.
abstract  pdf  bibtex
Abstract:
In 1996 Zhou and Hansen proposed a firstorder 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{Hoefner20055,
Author = {H{\"o}fner, P.},
Title = {Semiring Neighbours},
Institution = {Institute of Computer Science, University of Augsburg},
Number = {200519},
Year = {2005},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr200519_hoe/}
}

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 200507, 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 attributerich 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 XMLbased 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 PNews, 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{Hoefner20052,
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 = {200507},
Year = {2005},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/db/publications/all_db_techreports/tr20057_huh_hoe_kie/}
}

P. Höfner:
From Sequential Algebra to Kleene Algebra: Interval Modalities and Duration Calculus. Technical Report 200505, 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{Hoefner20051,
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 = {200505},
Year = {2005},
Url = {www.informatik.uniaugsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_techreports/tr20055_hoe/}
}
Miscellaneous (Abstracts, Theses, Prefaces, ...)

P. Höfner:
Kleene Modules for Routing Procedures (Abstract). In Workshop on Lattices and Relations (L&R 2012). 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 matrixlevel. In this talk I will present the shortcoming with the help of the Ad hoc OnDemand 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 ongoing developments and future work.
@misc{hoefner20128,
Author = {H{\"o}fner, Peter},
Howpublished = {Workshop on Lattices and Relations (L\&R 2012)},
Note = {(Abstract)},
Title = {Kleene Modules for Routing Procedures},
Year = {2012}
}

P. Höfner:
Towards a Representation Theorem for Coloring Algebra (Abstract). In Workshop on Lattices and Relations (L&R 2012). 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 levelbased 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 symmetricdifference in a settheoretic 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{hoefner20128,
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}
}

H.H. Dang, P. Höfner:
FirstOrder 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 200804, Institute of Computer Science, University of Augsburg, 4852, 2008.
abstract  pdf  bibtex
Abstract:
Recently it has been shown that offtheshelf firstorder 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 firstorder theorem provers.
@misc{hoefner20089,
Author = {Dang, Han Hing and H{\"o}fner, Peter},
Title = {FirstOrder 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 200804, Institute of Computer Science, University of Augsburg},
Pages = {4852},
Year = {2008}
}

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 200804, Institute of Computer Science, University of Augsburg, 6872, 2008.
abstract  pdf  bibtex
Abstract:
To realise a software that needs to interact with other com puters, serviceoriented 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{hoefner20088,
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 200804, Institute of Computer Science, University of Augsburg},
Pages = {6872},
Year = {2008}
}

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 A0707, Schriftenreihe A, Institutes for Computer Science and Mathematics, University of Lübeck, 8792, 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 offtheshelf 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 lightweight formal methods with heavyweight 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{hoefner20089,
Author = {Dang, Han Hing and H{\"o}fner, Peter},
Title = {FirstOrder 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 200804, Institute of Computer Science, University of Augsburg},
Pages = {4852},
Year = {2008}
}

P. Höfner:
fGenerated Kleene Algebra. In R.A. Schmidt, G. Struth (eds.), Relations and Kleene algebra in Computer Science — PhD Programme. Technical Report CS0609, University of Sheffield, 5559, 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 fgenerated Kleene algebra, that have an iteration operation which depends on a function f and modify the iterated element in each step.
@misc{hoefner20066,
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 CS0609, Department of Computer Science, University of Sheffield},
Pages = {5559},
Year = {2006}
}

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 0529, TU/e technische universiteit eindhoven, 613, 2005.
abstract  pdf  bibtex
Abstract:
In 1996 Zhou and Hansen proposed a firstorder 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{hoefner20053,
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 0529, TU/e technische universiteit eindhoven},
Pages = {613},
Year = {2005}
}

P. Höfner:
An Algebraic Semantics for Duration Calculus. In J. Gervain (ed.), Tenth ESSLLI Student Session. 99110, 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 realtime 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{hoefner20052,
Author = {H{\"o}fner, Peter},
Title = {An Algebraic Semantics for {Duration Calculus}},
Editor = {Gervain, Judit},
BookTitle = {Tenth ESSLLI Student Session},
Pages = {110},
Year = {2005}
}

P. Höfner:
Von sequentieller Algebra zu KleeneAlgebra: Intervalloperatoren and ZeitdauerKalkül. Master's Thesis (Diplomarbeit), Universität Augsburg, 2003.
abstract  pdf  bibtex
Abstract:
Der ZeitdauerKalkül (Duration Calculus, DC) ist ein formales, algebraisches System für die Spezifikation und das Design eines EchtzeitSicherheitssystems. 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 ZeitdauerKalkül eine Verknüpfung zu Sicherheitssystemen und Intervallen her. M.R. Hansen und Z. Chaochen zeigten 1997, dass der ZeitdauerKalkül die IntervallLogik (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 ZeitdauerKalkül unter dem Aspekt der Einbettung in sequentielle Algebren. Er führt zudem erstmalig den Begriff der IngenieursInduktion (Engeneer's induction) ein. Unabhängig hiervon existiert die algebraische Struktur der KleeneAlgebra (KA). Diese erweitert Halbringe um einen weiteren unären Operator, den KleeneStern. KleeneAlgebren 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 KleeneAlgebren, 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 KleeneAlgebra über der Potenzmenge der positiven reellen Zahlen. (Die dort dargestellte KleeneAlgebra 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 zeittheoretischen Überlegungen, wie sie für den ZeitdauerKalkül benötigt werden, eine zentrale Rolle spielen. Ziel dieser Arbeit soll es sein, den ZeitdauerKalkül auf der Grundlage von KleeneAlgebren zu analysieren und zu präsentieren.
@misc{hoefner20031,
Author = {H{\"o}fner, Peter},
Title = {{Von sequentieller Algebra zu KleeneAlgebra: Intervalloperatoren und ZeitdauerKalk\"ul}},
School = {Universit\"at Augsburg},,
Year = {2003},,
Address = {Universit\"at Augsburg, Institut f\"urInformatik},
}
Last update: Apr 02, 2019