Probabilistic transition systems are transition systems where after each action several states can be reached with a certain probability. These transition systems are very convenient to describe systems in which actions happen with a certain probability. One can think not only of games, but also of scheduling systems, data transfer systems etc.

We have two questions that needs addressing.

- What is probabilistic trace and probabilistic weak trace equivalence, and what are algorithms to solve them? Can we use for instance the standard determination algorithm, or are other algorithms more useful?
- For probabilistic modal formulas, what is it syntax and how to translate those to PRESs, which are the pendant of PBESs for probabilistic systems?

Adding sequential composition to the axiomatisations of van Glabbeek's spectrum.

For all behavioural equivalences in van Glabbeek's linear time - branching time spectrum it is known whether there exists a finite axiomatisation in the context of the language BCCSP (which has a constant 0, unary action prefixes a. and a binary operation + for choice). In [1], an overview of these results is presented. It would be interesting to investigate what is the effect of adding operations such as sequential composition, parallel composition, ... on the existence of finite axiomatisations.

For some behavioural equivalences in the spectrum it will be reasonably straightforward to extend the existing finite axiomatisation for BCCSP with sequential composition, or to prove that the non-existence of a finite axiomatisation still holds true if sequential composition is added. For some others it will be harder. The assignment would be to make a start with considering the spectrum in the context of a language with sequential composition.

Reference: [1] Taolue Chen, Wan Fokkink, Bas Luttik, and Sumit Nain. On finite alphabets and infinite bases. Information and Computation 206(5):492-519, 2008.

Topic: Explicit Divergence in Weak Bisimulation

Branching bisimilarity and weak bisimilarity are typically used in process algebras where silent steps are used to abstract from internal behaviours. This facilitates relating implementations and specifications. For branching bisimilarity, there is a natural notion of sensitivity to divergence (i.e. infinite internal activity), and there are a number of ways in which branching bisimilarity with explicit divergence can be characterised: relationally, through coloured traces, or through an appropriate modal logic. For weak bisimilarity, the case is less clear; that is, it is not clear what the natural notion of divergence sensitivity is in the context of weak bisimilarity. This assignment deals with investigating divergence aware extensions of the relational characterisation of weak bisimilarity and, time permitting, linking these to an appropriate modal logic.

Topic: mCRL2 with global variables

The process specification language mCRL2 does not have a notion of global variable; parallel components can only communicate by message passing. For many applications, especially when mCRL2 specifications are obtained through translation from another formalism that does have global variables, their absence in mCRL2 is inconvenient. It would therefore be interesting to investigate how a notion of global variable can be added to mCRL2, and what would be the theoretical and practical implications of such an addition.

The assignment would consist of addressing some of the following questions: What are the implications for the process-algebraic semantics of mCRL2 specifications? What are the appropriate notions of behavioural equivalence? How should global variables be used in modal logics for specifying properties of mCRL2 specifications? How would adding a notion of global variable to mCRL2 affect the tools in the mCRL2 toolset.

Starting point for this research would be the paper "Process Algebra with Propositional Signals" by Jan A. Bergstra and Jos C. M. Baeten, Theoretical Computer Science 177(2):381-405, 1997.

Topic: An experimental study of new parity game solving algorithms

Parity games are two-player, infinite duration games. Several important decision problems can be effectively encoded in parity games, and by solving the resulting parity games, the decision problem can be answered. There are several algorithms for solving a parity game. Some of these have a very nice theoretical (worst-case) time complexity but perform pretty bad in practice, while others do not have such nice (worst-case) time complexities but, in practice, manage to solve parity games rather comfortably and efficiently. Recently, a few new algorithms have been proposed that are claimed to fall in the latter category. The assignment is to take such an algorithm, implement it and compare it against one of the more classical algorithms to see whether the algorithm lives up to its claims.

Topic: Family-based vs. Product-Based Model Checking using ProVeLines and mCRL2. For details, see here.

Seminar project: Formal verification of networks

Our research is concerned with formally verifying the correctness of communication networks, in particular networks deployed in so called Systems-on-Chip (SoCs in cars, phones etc.). For this purpose, we are developing a specification language together with algorithms and tools. There are many questions we would like to address. Here are some examples:

- equivalence between networks: the fundamental question is about defining the notion of "equality" between networks. What does "equal" mean for networks? What properties are preserved under which definition of equivalence?
- Labelled Transition Systems (LTS) semantics: we are working on using LTS-based techniques to express the semantics of our language. We are also interested in looking at LTS-based model-checking techniques applied to our network specifications. The challenge is the size of the state space: it gets very big very quickly. A possible assignment would here be to use our initial results in generating LTSs from network specification to explore the application of model checking techniques like mCRL2 or LTSMIN in our context
- Compositional liveness verification: Liveness properties are about "goods things that eventually happen". The fact that good things happen depends heavily on the interaction of the different components of a system. It is very often difficult to break down the verification liveness to the level of components. It often has to be proven at the system level. Still, there have been proposals (and we have some ideas as well :-) for compositional liveness verification. In this assignment, we would like to look at this problem. In particular, we would like to study what pre-orders can be used in our setting to decompose liveness proofs.

Teaches the course: Proving with Computer Assistance (3d quarter). He is only at the TUE on Thursday (otherwise at RU Nijmegen), but November is special: then the options to meet are: Monday 7 Nov, Thursday 10 Nov 9:00 -11:00. He is not available on Thursday 17 Nov and 24 Nov and 1 Dec, but is available on Wednesday 30 Nov.

Topic: Type theory and lambda calculus as foundations for (functional) programming and proof assistants.

Concrete seminar projects:

- Subtyping, inheritance and overloading in typed lambda calculus
- Data types with laws: adding equations to abstract data types, an old idea of David Turner (the developer of the functional language Miranda); how to do this consistently and what are the associated proof principles?
- The "Lean" theorem prover: a new proof assistant (based on type theory), developed by Microsoft Research (together with Carnegie Mellon Univ); what is it and what are its key differentiating features?

Seminar project: Translating programming statements into mCRL2

The mCRL2 toolset can be used for analysis and verification of software systems. In many cases this is done by making a concrete mCRL2 model for an exisiting system. But a trend is that companies are using their own domain specific languages to describe their systems. These DSLs may contain arbitrary programming statements, and the question is how to translate these into mCRL2. Recently an automated translation of the Dezyne modeling language of the company Verum has been realized, and several similar projects are under way.

The goal of this assignment is to make an overview of common programming statements, and to investigate how they can be translated into mCRL2, i.e. in terms of process algebra equations. The first part of the assignment is to study existing approaches for that. The second part is to extend this with translations of missing statements. Undoubtedly there will be statements that are hard to translate, or not well suited for verification. In such cases possible approaches to deal with that (simplifications, abstractions) can be discussed.

Seminar project: Learning automata by SAT solving

We consider the issue of finding an automaton (DFA, NFA) satisfying a given set of constraints. These constraints can be of the shape that particular strings should or should not be accepted by the automaton, but can also involve properties of the accepting language or behavioral properties in considering the automaton as a transition system. In this project it will be investigated, based on some initial literature, how SAT/SMT solving may serve for solving this problem.

As an alternative seminar project also other problems may be considered to exploit SAT/SMT solvers, like scheduling problems.

Topic: Specification and verification of infinite LTSs using graph grammars.

Using a so-called LTS rewrite system, it is possible to specify a system with an infinite state space. This is similar to the use of infinite recursive specifications in process algebra. With a combination of graph rewrite rules, an infinite LTS can be specified. These LTSs can no longer be model checked by traversing the state space in the traditional way. However, with the introduction of model checking techniques for graph rewrite rules, it becomes possible to verify these LTSs specified as graph grammars. The assignment is to investigate the possibilities of model checking techniques for graph rewrite rules to verify infinite LTSs.

Topic: Verifying whether partial models satisfy partial properties

In model-driven development, systems are often incrementally designed, meaning that functional details about the system are introduced in a number of steps. In such a workflow, formal verification could be particularly effective if the used technique can handle the fact that parts of the current system design and/or property to be checked are currently not well-specified. Then, at a later stage when some of those gaps have been filled, ideally, the technique can reuse earlier results to efficiently determine whether the more concrete system still satisfies the more concrete property. Several approaches to handle partial state spaces and partial properties have been suggested in the literature.

In the last few years, we have developed a verification technique to verify whether model transformations, formalised as LTS transformations, preserve particular functional properties. The next step is to determine whether a transformation applicable on both systems and properties is guaranteed to produce new systems that satisfy the accompanying new properties. This would allow for the maintenance of properties, instead of leaving them the way they are initially specified. Ideas from the work on partial state spaces may be applicable in this context as well, but this is currently not known. The assignment is to conduct a literature study to investigate the current state-of-the-art in the verification of partially specified systems using partially specified properties, with the aim to determine to what extent the findings are applicable on the verification of transformations. If desired, this assignment could be extended to a master thesis assignment, by subsequently working on the verification of transformations that transform both systems and properties.

Last change: November 10, 2016