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.
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?
Bas Luttik MF 6.072, firstname.lastname@example.org
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 , 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.
 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, email@example.com, and
Tim Willemse MF 6.073, firstname.lastname@example.org
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, email@example.com
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, firstname.lastname@example.org
Topic: Family-based vs. Product-Based Model Checking using
ProVeLines and mCRL2. For details, see
MF 6.071b, email@example.com
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
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.
MF 6.079a, firstname.lastname@example.org
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
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
MF 6.076, email@example.com
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, firstname.lastname@example.org
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, email@example.com, 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