Presentations
Below is a nearly complete list of all presentions of Peter Höfner. (no teaching)
2019

Justness: when progress is too weak and fairness it too strong.
IFIP WG 2.3, York, UK. February 2019. pdf
Abstract:

False Failure: Creating Failure Models for Separation Logic.
17th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS'18), Groningen, The Netherlands. October 2019. abstract
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
2018

Next Generation Smart Systems (Panel Discussion).
23rd International Conference on Formal Methods for Industrial Critical Systems (FMICS), Maynooth, Ireland. September 2018.
Abstract:

Analysing AWNspecifications using mCRL2 (extended abstract).
14th International Conference on integrated Formal Methods (iFM), Maynooth, Ireland. Sep 2018.
Abstract:

Failure Models for Separation Algebra.
IFIP WG 2.1, Brandenburg a.d. Havel, Germany. July 2018.
Abstract:

Using Process Algebra to Design Better Protocols.
University of Queensland, Brisbane, Australia. June 2018. abstract  pdf
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 talk 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.

Forwards and Backwards in Separation Algebra.
IFIP WG 2.3, Providence, Rhode Island. May 2018. abstract  pdf
Abstract:
In this talk I present a framework that allows backward reasoning using weakest preconditions, and forward reasoning using strongest postconditions for separation logic. While the former is derived directly from the standard operators of separation logic, the latter uses a new operator, which I introduce. We implemented the framework in the interactive theorem prover Isabelle/HOL, and enable automation with several interactive proof tactics. I will end the presentation with a couple of open problems we are working on right now.
2017

Using Process Algebra to Design Better Protocols.
Lero, Limerick, Ireland. November 2017. abstract  pdf
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 talk 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.

Forwards and Backwards in Separation Algebra.
IFIP WG 2.1, Lesbos, Greece. October 2017. abstract  pdf
Abstract:
In this talk I present a framework that allows backward reasoning using weakest preconditions, and forward reasoning using strongest postconditions for separation logic. While the former is derived directly from the standard operators of separation logic, the latter uses a new operator, which I introduce. We implemented the framework in the interactive theorem prover Isabelle/HOL, and enable automation with several interactive proof tactics. I will end the presentation with a couple of open problems we are working on right now.

Verifying Liveness Properties: Assumptions and Problems.
IFIP WG 2.3, Mooloolaba, Australia. July 2017. pdf
Abstract:

Forwards and Backwards in Separation Algebra.
University of Queensland, Brisbane, Australia. June 2017. abstract  pdf
Abstract:
Separation algebra is a formal and abstract algebraic framework to describe separation logic. So far separation algebra was mainly used as an abstract base to reason about heaps. I will present an algebraic framework that allows backward reasoning using weakest preconditions, and forward reasoning using strongest postconditions for separation algebra; and hence also for separation logic. While the former is well understood, the later requires the introduction of a new operator. Since this is work in progress I will point at some surprising algebraic problems that need to be solved within the setting of forward reasoning.

Split, Send, Reassemble: A Formal Specification of a CAN bus Protocol Stack"location: "Uppsala, Sweden.
2nd Workshop on Models for Formal Analysis of Real Systems (MARS 2017), April 2017. abstract  pdf
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.

Using Process Algebra to Design Better Protocols.
University of Twente, The Netherlands. February 2017. abstract  pdf
Abstract:
"Despite the maturity of formal description languages and formal methods for analyzing them, the description of real protocols is still overwhelmingly informal. The consequences of informal protocol description drag down industrial productivity and impede research progress" Pamela Zave\n This talk advocates formal methods in general, and process algebra in particular, as an alternative methodology for specifying, analysing and verifying protocols.\n After a short introduction of “failures” in specifying protocols, I will give a brief overview of our work in this area, which includes the development of a process algebra for wireless protocols, and its application to prove loop freedom of the AODV routing protocol, one of the major protocols in the area of wireless mesh networks. The latter required some adaptations to the specification, as the original specification protocol was not loop free.\n I will show that our modular proof strategy makes it easy to check that crucial correctness properties, such as loop freedom, are preserved under changes in the specification. Through automatic translation from processalgebraic specifications into the input language of model checkers, such as UPPAAL, proposed specifications can be tested on the fly modelchecking techniques.

Using Process Algebra to Design Better Protocols.
Vrije Universiteit Amsterdam, The Netherlands. January 2017. abstract  pdf
Abstract:
"Despite the maturity of formal description languages and formal methods for analyzing them, the description of real protocols is still overwhelmingly informal. The consequences of informal protocol description drag down industrial productivity and impede research progress" Pamela Zave\n This talk advocates formal methods in general, and process algebra in particular, as an alternative methodology for specifying, analysing and verifying protocols.\n After a short introduction of “failures” in specifying protocols, I will give a brief overview of our work in this area, which includes the development of a process algebra for wireless protocols, and its application to prove loop freedom of the AODV routing protocol, one of the major protocols in the area of wireless mesh networks. The latter required some adaptations to the specification, as the original specification protocol was not loop free.\n I will show that our modular proof strategy makes it easy to check that crucial correctness properties, such as loop freedom, are preserved under changes in the specification. Through automatic translation from processalgebraic specifications into the input language of model checkers, such as UPPAAL, proposed specifications can be tested on the fly modelchecking techniques.
2016

How to Review a Paper.
PhD Bootcamp Trustworthy Systems Group, Sydney, Australia. July 2016.
Abstract:

System Verified  Can we go to the Beach now?.
University of Augsburg, Augsburg, Germany. April 2016.
Abstract:

Was ist Informatik.
Anna Gymnasium, Sydney, Australia  Sometimes it's Rocket Science. April 2016.
Abstract:

A (Timed) Process Algebra for Wireless Mesh Networks.
Saarland University, Saarbücken, Germany. April 2016. abstract
Abstract:
Wireless Mesh Networks have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially selforganising wireless adhoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and lowcost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and testbed experiments. The key limitations of these approaches are that they are very expensive, time consuming and nonexhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the "timetomarket" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks. In this talk I present a process algebra for wireless mesh networks that combines novel treatments of broadcast, prioritised unicast, data structures and time. In this framework, we modelled the widelyused Adhoc OnDemand Distance Vector (AODV) routing protocol and (dis)proved crucial properties such as loop freedom.

A Timed Process Algebra for Wireless Networks with an Application in Routing (Extended Abstract).
19th European Joint Conferences on Theory and Practice of Software (ETAPS), Eindhoven, The Netherlands. April 2016. abstract  pdf
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.
2015

Verification of Relational Programs and Approximation Algorithms.
14th Logic and Computation Seminar, Kyushu University, Fukuoka, Japan. November 2015. abstract  pdf
Abstract:
Over the last decades relation algebra has shown its strength in many areas of mathematics and computer science: applications reach from data bases, graphs and preference modelling, via modal reasoning to linguistics and hardware verification.
In this talk I show how relation algebra in combination with Hoare logic can yield automation in verification tasks. I will illustrate the use of relation algebra in verification and show that (automated) theorem provers can help to verify relational while programs such as the calculation of the reflexivetransitive closure or an algorithm for topological sorting.
Based on this, I will then extend this work to cardinalities of relations, which allows the formal verification of approximation algorithms. This work is influenced and based on a characterisation of cardinalities for relation algebra developed by Prof. Kawahara.

Using Process Algebra to Design Better Protocols.
Forum "MathforIndustry" 2015, Fukuoka, Japan. October 2015. (invited) pdf
Abstract:

Shapes.
73rd meeting of IFIP Working Group 2.1 on Algorithmic Languages and Calculi, Lökeberg, Sweden. August 2015.
Abstract:

Formal Specification of Protocols for Internal HighAssurance Networks.
NICTA, Sydney, Australia. August 2015.
Abstract:
2014

A Mechanized Proof of Loop Freedom of the (Untimed) AODV Routing Protocol.
Symposium on Automated Technology for Verification and Analysis (ATVA'14), Sydney, Australia. November 2014. abstract  pdf
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.

Algebraic (Software) Verification.
Doha, Qatar. July 2014. (invited) abstract
Abstract:
It is well known that software verification is essential for safetycritical systems. Usually verification requires expert knowledge, and it is time consuming. Both aspects make software verification expensive (although it is still unclear how much more a customer has to pay for verified software). As a consequence, automation in software verification is crucial. In case theorem provers are used, a proof script also acts as a ``certificate'' and increase the confidence in the result.\\In this talk I will give an overview over verification tasks I have work on during the last couple of years. Applications range from hybrid systems to protocol analysis. A particular focus of this talk will be on software that can support verification techniques. I will show how\\(a) automated theorem provers, e.g. Prover9,\\(b) interactive theorem provers, e.g. Isabelle/HOL,\\(c) model checkers, e.g. Uppaal, and\\(d) specialpurpose tools, e.g. RelView, can be applied for verification tasks.

Algebras for (automatic) Verification of Graph Algorithms.
71st meeting of IFIP Working Group 2.1 on Algorithmic Languages and Calculi, Zeegse, The Netherlands. March 2014. pdf
Abstract:
2013

Statistical Model Checking with Uppaal.
NICTA, Sydney, Australia. December 2013. abstract  pdf
Abstract:
This talk is a continuation of Franck's talk. Model Checking was successfully applied to countless (industrial) case studies, as Franck pointed out. However, several case studies indicate that model checking is limited in some scenarios: state space explosion restricts applicability to large distributed systems, and quantitative reasoning, often sufficient for applications, is not possible. Both deficiencies can be overcome to some extent by the use of statistical model checkers, such as SMCUppaal. In this talk I will give a short introduction to statistical model checking and illustrate its usefulness by a quantitative analysis of two wellknown routing protocols for wireless mesh networks, namely AODV and DYMO. Moreover, I will report on experiments where we pushed the limits of statistical modelchecking and showed that this technology is capable of analysing networks of up to 100 nodes.

Formal Methods for Wireless Mesh Networks.
Argentina. August 2013. abstract  pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially selforganising wireless adhoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and lowcost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and testbed experiments. The key limitations of these approaches are that they are very expensive, time consuming and nonexhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the 'timetomarket' for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WMNs and present how formal methods can be applied. In particular I will presents techniques used for modelling, analysing and verifying the Adhoc on Demand Distance Vector (AODV) routing protocol, one of the leading protocols for WMNs. The techniques includes a formal model using process algebra, fully automation by a matrix model and the use of (statistical) model checkers.

Topologybased Mobility Models for Wireless Networks.
Quantitative Evaluation of Systems (QEST'13), Buenos Aires, Argentina. August 2013. abstract  pdf
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).

Statistical Model Checking of Wireless Mesh Routing Protocols.
University of Augsburg, Germany. July 2013. abstract  pdf
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 talk I will illustrate this by a quantitative analysis of two wellknown routing protocols for wireless mesh networks, namely AODV and DYMO. Among others I will show that some optional features of AODV are not useful, and that AODV shows unexpected behaviouryielding a high chance of route discovery failure.
Last, but not least, I will report on experiments set up in a way to find the benefits and the limits of statistical model checking. In particular I will discuss a result that verifies that this technology is capable of analysing networks of up to 100 nodes.

Ad hoc Routing in Mesh Networks using Algebra.
70th meeting of IFIP Working Group 2.1 on Algorithmic Languages and Calculi, Schloss Reisensburg, Germany. July 2013. abstract  pdf
Abstract:
At the meeting in Rome I gave an overview of formal modelling and analysis of routing protocols for wireless mesh networks (WMNs). Afterwards I was asked to present details about the methods used. This talk presents some more details about the algebra used to model main aspect of routing protocols.

Analyse drahtloser Netzwerke mittels Formaler Methoden.
ChristianAbrechtsUniversität zu Kiel, Germany. June 2013. abstract  pdf
Abstract:
Wireless Mesh Netzwerke (WMNe), auch drahtlose, gemaschte Netzwerke genannt, werden heutzutage in einer Vielzahl von Gebieten eingesetzt: Anwendungen reichen von Sicherstellung der öffentlichen Sicherheit, über intelligente Transportsysteme bis hin zu Videoüberwachung. Durch das Fehlen von Kabeln bieten diese Netzwerke eine kostengünstige Alternative zu klassischen Netzwerken und bringen zusätzlich den Vorteil mit sich, dass die Installation einfach und schnell verläuft. Um Daten über solche Netzwerke zu schicken, spielen RoutingProtokolle (Pfadfindung) eine zentrale Rolle; sie müssen insbesondere Besonderheiten von WMNen, wie etwa eine dynamische Topologie oder unzuverlässige Knotenverbindungen berücksichtigen.
Im alltäglichen Einsatz treten massive Probleme in der Performanz und der Zuverlässigkeit dieser Netzwerke auf. Klassische Analysetechniken, wie Simulation und TestbettEvaluation, konnten diese Probleme bisher nicht lösen, da sie viel Zeit beanspruchen und auch nicht alle Eventualitäten in Betracht ziehen. Eine Folge ist, dass selbst nach Jahren noch Fehler in Routingprotokollen gefunden werden.
Formale Methoden haben das Potenzial, Routing Protokolle präzise zu beschreiben und zu analysieren. In dem Vortrag wird, nach einem kurzen Überblick über WMNe, eines der StandardRoutingprotokolle, das \"Adhoc on Demand Distance Vector (AODV) routing protocol\" vorgestellt. Anschliessend wird ein Überblick über formale Methoden präsentiert, die bei NICTA erfolgreich zur Modellierung, Analyse und Verifikation des AODV Protokolls eingesetzt wurden. Behandelt werden ein prozessalgebraischer Ansatz, welcher alle Details von AODV abdeckt, ein Ansatz mittels Linearer Algebra, welcher den Einsatz von automatischen Theorembeweisern ermöglicht, und die Verwendung von Model Checkern.

Statistical Model Checking of Wireless Mesh Routing Protocols.
5th NASA Formal Methods Symposium (NFM'13), Mountain View, CA, USA. May 2013. abstract  pdf
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.

Formal Verification of Networks—Description Language—.
NICTA, Sydney, Australia. April 2013. abstract  pdf
Abstract:
Formal Verification of Networks can only be achieved when the specification (written in English prose) comes along with a formal description of the system. In this talk I will present a description language developed at NICTA to model network protocols for (wireless networks). The language covers main primitives of protocols, such as message passing, and is easy to use.The talk will not only cover details of the language (syntax), but also parts of the underlying semantics. The semantics is given in form of a structural operational semantics which immediately yields an underlying process algebra and allows formal reasoning.
The formal description language builds the base of many useful verification techniques; for example, proof mechanisation using Isabelle/HOL or (statistical) model checking using Uppaal. (these techniques are not part of this talk; but may be part of forthcoming talks)
2012

Past and Future of Formal Methods for Wireless Mesh Networks.
Quantitative Methods in Security and Safety Critical Applications, Shonan Village, Japan. November 2012. abstract  pdf
Abstract:
Wireless Mesh Networks (WMNs) are a promising technology that is currently being used in a wide range of application areas, including Public Safety, Transportation, Mining, etc. Typically, these networks do not have a central component (router), but each node in the network acts as an independent router, regardless of whether it is connected to another node or not. They allow reconfiguration around broken or blocked paths by \"hopping\" from node to node until the destination is reached. Unfortunately, the performance of current systems often does not live up to the expectations of end users in terms of performance and reliability, as well as ease of deployment and management.
The presentation will start with an overview of the (formal) methods for WMNs developed over the last two years. In particular, I will focus on a processalgebraic approach, which turned out to be very useful and powerful, and which can be complemented by model checking. Usability of our approach is illustrated by the analysis of the Adhoc Ondemand Distance Vector (AODV) routing protocol, a popular routing protocol designed for WMNs, and one of the four protocols currently standardised by the IETF MANET working group.
The talk will then discuss possible directions for future work. In particular, the talk will discuss two topics. (a) the extension of the processalgebraic approach by probabilities to model packet loss and to allow quantitative reasoning (b) the quest of protocol comparison, i.e., under which circumstances is one protocol better than another. Here new formalisms need to be created and evaluated.

Towards a Rigorous Analysis of AODVv2 (DYMO).
2nd International Workshop on Rigorous Protocol Engineering, UAustin, TX, USA. October 2012. abstract  pdf
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.

A Rigorous Analysis of AODV and its Variants.
15th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWIM'12), Paphos, Cyprus. October 2012. abstract  pdf
Abstract:
In this talk 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.

Kleene Modules for Routing Procedures.
Workshop on Lattices and Relations, Amsterdam, The Netherlands. September 2012. abstract  pdf
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.

Towards a Representation Theorem for Coloring Algebra.
Workshop on Lattices and Relations, Amsterdam, The Netherlands. September 2012. abstract  pdf
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.

Morgan: A Suitable Case for Treatment.
Carroll Morgan—Birthday Seminar, University of New South Wales, Sydney, Australia. July 2012. pdf
Abstract:

Formal Methods for Wireless (Mesh) Protocols.
NICTA, Sydney, Australia. April 2012. pdf
Abstract:

A Process Algebra for Wireless Mesh Networks.
21st European Symposium on Programming (ESOP'12), Tallinn, Estonia. March 2012. abstract  pdf
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.

Automated Analysis of AODV using UPPAAL.
18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), Tallinn, Estonia. March 2012. abstract  pdf
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.

Formal Methods for Wireless Mesh Networks.
National University Singapore, Singapore. February 2012. abstract  pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially selforganising wireless adhoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and lowcost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and testbed experiments. The key limitations of these approaches are that they are very expensive, time consuming and nonexhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"timetomarket\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WMNs and present one of the leading protocols: the Adhoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV. This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work.

Formal Methods for Wireless Mesh Networks.
TU München, Germany. February 2012. abstract  pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially selforganising wireless adhoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and lowcost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and testbed experiments. The key limitations of these approaches are that they are very expensive, time consuming and nonexhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"timetomarket\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WMNs and present one of the leading protocols: the Adhoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV. This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work. The latter includes a formal model of process algebra in Isabelle/HOL.

Formal Methods for Wireless Mesh Networks.
RWTH Aachen, Germany. February 2012. abstract  pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially selforganising wireless adhoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and lowcost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and testbed experiments. The key limitations of these approaches are that they are very expensive, time consuming and nonexhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"timetomarket\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WMNs and present one of the leading protocols: the Adhoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV. This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work.

Formal Methods for Wireless Mesh Networks.
IFIP WG 2.1, Rome, Italy. February 2012. pdf
Abstract:

Formal Methods for Wireless Mesh Networks.
University of Pisa, Italy. February 2012. abstract  pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially selforganising wireless adhoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and lowcost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and testbed experiments. The key limitations of these approaches are that they are very expensive, time consuming and nonexhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"timetomarket\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WMNs and present one of the leading protocols: the Adhoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV. This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work.

Formal Methods for Wireless Mesh Networks.
University of Bologna, Italy. January 2012. abstract  pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially selforganising wireless adhoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and lowcost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and testbed experiments. The key limitations of these approaches are that they are very expensive, time consuming and nonexhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"timetomarket\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WMNs and present one of the leading protocols: the Adhoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV. This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work.

Formal Methods for Mesh Protocols.
NICTA, Sydney, Australia. January 2012. pdf
Abstract:
2011

Formal Methods for Wireless Mesh Networks.
University of Adelaide, Adelaide, Australia. December 2011. abstract  pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially selforganising wireless adhoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and lowcost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and testbed experiments. The key limitations of these approaches are that they are very expensive, time consuming and nonexhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"timetomarket\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WMNs and present one of the leading protocols: the Adhoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV. This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work.

Modelling and Analysis of AODV in UPPAAL.
1st International Workshop on Rigorous Protocol Engineering, colocated with ICNP 2011, Vancouver, Canada. October 2011. abstract  pdf
Abstract:
This talk 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.

A Process Algebra for Wireless Mesh Networks.
University of Augsburg, Augsburg, Germany. June 2011. abstract  pdf
Abstract:
Wireless Mesh Networks have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially selforganising wireless adhoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and lowcost network deployment.
Traditionally, the main tools for evaluating and validating network protocol are simulation and testbed experiments. The key limitations of these approaches are that they are very expensive, time consuming and nonexhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"timetomarket\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I propose a process algebra for wireless mesh networks that combines novel treatments of broadcast, prioritised unicast and data structures. In this framework, we modelled the widelyused Adhoc OnDemand Distance Vector (AODV) routing protocol and prove crucial properties such as loop freedom.

Formal Methods for Wireless Mesh Networks.
University of Augsburg, Augsburg, Germany. June 2011. abstract  pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially selforganising wireless adhoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and lowcost network deployment.
Traditionally, the main tools for evaluating and validating network protocol are simulation and testbed experiments. The key limitations of these approaches are that they are very expensive, time consuming and nonexhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation.
Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"timetomarket\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks.
In this talk I describe the importance of WMNs and present one of the leading protocols: the Adhoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV. This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work.

Towards an Algebra of Routing Tables.
12th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS'12), Rotterdam, The Netherlands. June 2011. abstract  pdf
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).

Formal Methods for Wireless Mesh Networks.
University of Cambridge, Cambridge, UK. May 2011. abstract  pdf
Abstract:
Wireless Mesh Networks (WMNs) have recently gained considerable popularity and are increasingly deployed in a wide range of application scenarios, including emergency response communication, intelligent transportation systems, mining, video surveillance, etc. WMNs are essentially selforganising wireless adhoc networks that can provide broadband communication without relying on a wired backhaul infrastructure. This has the benefit of rapid and lowcost network deployment. Traditionally, the main tools for evaluating and validating network protocol are simulation and testbed experiments. The key limitations of these approaches are that they are very expensive, time consuming and nonexhaustive. As a result, protocol errors and limitations are still found many years after the definition and standardisation. Formal methods have a great potential in helping to address this problem, and can provide valuable tools for the design, evaluation and verification of WMN routing protocols. The overall goal is to reduce the \"timetomarket\" for better (new or modified) WMN protocols, and to increase the reliability and performance of the corresponding networks. In this talk I describe the importance of WMNs and present one of the leading protocols: the Adhoc on Demand Distance Vector (AODV) routing protocol. Moreover, I give an overview over formal methods used so far to model, analyse and verify AODV . This includes a formal model using process algebra, fully automation by a matrix model and the use of model checkers. In an outlook I present some problems we are faced and discuss ongoing and future work.

An Algebra for Routing Protocols.
University of Sheffield, Sheffield, UK. May 2011. pdf
Abstract:
2009

How to find Algebraic Semantics for Modal and Temporal Logics.
10th International Conference on Relational Methods in Computer Science, 5th International Conference on Applications of Kleene Algebra, Doha, Qatar. October 2009. (Tutorial) pdf
Abstract:

An Extention of Feature Algebra.
1st Workshop on FeatureOriented Software Development (FOSD'09), Denver, USA. Oct 2009. abstract  pdf
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.

An Algebra of Product Families.
McMaster University, Hamilton, Canada. August 2009. (invited) abstract  pdf
Abstract:
Experience from recent years has shown that it is often advantageousnot to build a single product but rather a family of similar productsthat share at least one common functionality while havingwellidentified variabilities. Such product families are built fromelementary features that reach from hardware parts to softwareartefacts such as requirements, architectural elements or patterns,components, middleware, or code. We use the well establishedmathematical structure of idempotent semirings as the basis for aproduct family algebra that allows a formal treatment of the abovenotions. A particular application of the algebra concerns themultiview reconciliation problem that arises when complex systems aremodelled. We use algebraic integration constraints linking features inone view to features in the same or a different view and show inseveral examples the suitability of this approach for a wide class ofintegration constraint formulations.

Algebraic Calculi for Hybrid Systems.
McMaster University, Hamilton, Canada. August 2009. (invited) abstract  pdf
Abstract:
Hybrid systems are heterogeneous systems characterised by the interaction of discrete and continuous dynamics. They have many applications, such as automated highway systems, airtraffic control, automotive controllers, robotics, chemical and biological processes. Hybrid automata are widely popular for designing and modelling hybrid systems. Nevertheless, they are quite unhandy in calculations concerning liveness and safety properties.
The first part of the talk gives a short introduction to hybrid systems and hybrid automata. Furthermore it presents a trajectorybased model for describing hybrid systems. This approach uses a weak Kleene algebra, a relaxed version of Kleene algebra. It will be shown that hybrid automata can conveniently be embedded into the algebra. Moreover some important advantages of the algebraic approach are discussed. The second part will be a longer discussion about what we have done in the area of hybrid systems, what we do at the moment and what we are planning to do.

Featuritis.
Doktoranden und Diplomandenseminar, Lehrstuhl Datenbanken, Universität Augsburg, Sion, Switzerland. July 2009. (in German) pdf
Abstract:

Algebraische Kalküle für Hybride Systeme.
Rigorosum, Universität Augsburg, Augsburg, Germany. July 2009. (in German) pdf
Abstract:
2008

Algebraische Kalküle für hybride Systeme.
Winterakademie Elitenetzwerk Bayern, Kloster Irsee, Germany. December 2008. (in German) application  pdf
Abstract:

An Algebra of Hybrid Systems.
The University of Queensland, Brisbane, Australia. August 2008. (invited) abstract  pdf
Abstract:
Hybrid systems are heterogeneous systems characterised by the interaction of discrete and continuous dynamics. They have many applications, such as automated highway systems, airtraffic control, automotive controllers, robotics, chemical and biological processes. Hybrid automata are widely popular for designing and modelling hybrid systems. Nevertheless, they are quite unhandy in calculations concerning liveness and safety properties.
The first part of the talk gives a short introduction to hybrid systems and hybrid automata. Furthermore it presents a trajectorybased model for describing hybrid systems. This approach uses a weak Kleene algebra, a relaxed version of Kleene algebra. It will be shown that hybrid automata can conveniently be embedded into the algebra. Moreover some important advantages of the algebraic approach are discussed. The second part will be a longer discussion about what we have done in the area of hybrid systems, what we do at the moment and what we are planning to do.

On Automating the Calculus of Relations.
4th International Joint Conference on Automated Reasoning, Sydney, Australia. August 2008. abstract  pdf
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.

Von temporaler Intervalllogik zu Nachbarschaftslogik.
Doktoranden und Diplomandenseminar, Lehrstuhl Datenbanken, Universität Augsburg, Sion, Switzerland. July 2008. (in German, 35MB) pdf
Abstract:

Automated Reasoning for Hybrid Systems—Two Case Studies.
10th International Conference on Relational Methods in Computer Science, 5th International Conference on Applications of Kleene Algebra, Frauenwörth (near Munich), Germany. April 2008. abstract  pdf
Abstract:
At an abstract level hybrid systems are related to variants of Kleene algebra. Since it has recently been showed 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.
2007

Proof Automation in Kleene Algebra.
14. Kolloquium Programmiersprachen und Grundlagen der Programmierung, Timmendorfer Strand, Germany. October 2007. abstract  pdf
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.

Automated Reasoning in Kleene Algebra.
University of Augsburg, Augsburg, Germany. August 2007. pdf
Abstract:

Automated Reasoning in Kleene Algebra.
21st International Conference on Automated Deduction, Bremen, Germany. July 2007. abstract  pdf
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.

LightWeight Formal Methods with HeavyWeight Automation —or— One Year in Sheffield is not enough.
University of Sheffield, Sheffield, UK. June 2007. abstract  pdf
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. As a result we show that variants of Kleene algebras might provide lightweight formal methods with heavyweight automation. The first part of the talk will focus on case studies where this approach was successfully applied, including Hoare logic, concurrency control and refinement calculus. The second part outlines how this can be extended to an algebraic verification environment for programs and software systems. Since there is a lot more to do it shows that (for me) one year in Sheffield was not enough.

An Algebra of Hybrid Systems.
University of Sheffield, Sheffield, UK. February 2007. abstract  pdf
Abstract:
Hybrid systems are heterogeneous systems characterised by the interaction of discrete and continuous dynamics. They have many applications, such as automated highway systems, airtraffic control, automotive controllers, robotics, chemical and biological processes. Hybrid automata are widely popular for designing and modelling hybrid systems. Nevertheless, they are quite unhandy in calculations concerning liveness and safety properties. The first part of the talk gives a short introduction to hybrid systems and hybrid automata. Furthermore it presents a trajectorybased model for describing hybrid systems. This approach uses a variant of Kleene algebra. It mwill be shown that hybrid automata can conveniently be embedded into the algebra. Moreover some important advantages of the algebraic approach are discussed. The second part will be a longer discussion about what we have done in the area of hybrid systems, what we do at the moment and what we are planning to do.
2006

Lazy Semiring Neighbours and Some Applications.
9th International Conference on Relational Methods in Computer Science, 4th International Conference on Applications of Kleene Algebra, Manchester, UK. August 2006. abstract  pdf
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.

Omega Algebra, Demonic Refinement Algebra and Commands.
9th International Conference on Relational Methods in Computer Science, 4th International Conference on Applications of Kleene Algebra, Manchester, UK. August 2006. abstract  pdf
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.

fGenerated Kleene Algebra.
9th International Conference on Relational Methods in Computer Science, 4th International Conference on Applications of Kleene Algebra, Manchester, UK. August 2006. (PhD programme) abstract  pdf
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.
2005

Semiring Neighbours: An Algebraic Embedding and Extension of Neighbourhood Logic.
5th International Conference on Integrated Formal Methods, Eindhoven, The Netherlands. November 2005. (Doctoral Symposium) abstract  pdf
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.

Algebra of Hybrid Systems.
Kolloquium Programmiersprachen und Grundlagen der Programmierung, Fischbachau, Germany. September 2005. pdf
Abstract:

An Algebraic Semantics for Duration Calculus.
17th European Summer School in Logic, Language and Information, Edinburgh, Scotland. August 2005. (Student Session) abstract  pdf
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.

Towards an Algebra of Hybrid Systems.
8th International Conference on Relational Methods in Computer Science, 3rd International Conference on Applications of Kleene Algebra, St. Catherines, Canada. February 2005. abstract  pdf
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.
Last update: Apr 02, 2019