Seminar Formal System Analysis (2IMF00)

List of topics for 2016/2017

Jan Friso Groote MF 6.079b, j.f.groote@TUE.nl

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.

Bas Luttik MF 6.072, s.p.luttik@tue.nl

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.


Bas Luttik MF 6.072, s.p.luttik@tue.nl, and Tim Willemse MF 6.073, t.a.c.willemse@tue.nl

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.


Tim Willemse MF 6.073, t.a.c.willemse@tue.nl

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.


Erik de Vink MF 6.075, e.p.d.vink@tue.nl

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


Julien Schmaltz MF 6.071b, j.schmaltz@tue.nl

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: All assignments can have a more practical or more theoretical taste depending on your preferences.


Herman Geuvers MF 6.079a, herman@cs.ru.nl

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:

Wieger Wesselink MF 6.076, j.w.wesselink@tue.nl

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.


Hans Zantema, MF 6.078, h.zantema@tue.nl

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.


Anton Wijs, MF 6.077, a.j.wijs@tue.nl, and Sander de Putter, S.M.J.d.Putter@tue.nl

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