FOR UP-TO-DATE INFORMATION REGARDING THE PROGRAMME, SEE THE 2IMF00 CANVAS PAGES

2IMF00 --- Seminar Formal System Analysis (2020-2021)

In 2020/2021 this seminar will be held in quartile 2, the first meeting will be on Monday, November 9, 2020. Supervisor: Dr.ir. T.A.C. Willemse, Metaforum 6.073, tel 2999, t.a.c.willemse@tue.nl. For previous incarnations of this course, see this page (2018/19) or this page (before 2018).


Goal/contents

In this seminar, a group of master students will conduct research in the field of formal system analysis, i.e. the study of formalisms (e.g. their syntax, semantics and/or algorithmics) and their use in specifying, analysis and/or verifying (software) systems, as a preparation to the master's project. This will be done in the following ways:
  • Every student chooses a topic from the list of topics proposed by researchers in the group, and contacts the group member who proposed it, and together they decide about the topic to be investigated before the second meeting. These topics will be briefly presented/discussed on the first meeting. The supervision will be mainly done by the staff member proposing the assignment. You can also propose your own topic after consultation with, and agreement of an FSA supervisor; if you have a topic in mind for which no supervisor is obvious, please contact the coordinator.
  • In the second meeting, the students communicate the choice they have made and the research question(s) they will address in a 5-minute (powerpoint) presentation. Guidelines will be discussed during the first lecture
  • Research papers and/or book chapters will be studied and presented by the students, with a focus on research questions.
  • Examples related to the presented material or other investigations will be elaborated. If suitable, experiments related to these examples will be executed, either by using existing implementations or by developing ad hoc implementation.
  • Every student will give a technical 'mid-term' presentation of 20 minutes and a final presentation of 45 minutes.
  • Conclusions of the investigations are presented in a report. This report has the format of a paper with introduction, conclusions and bibliography, has a size of at most 30 pages, but preferrably much less.
  • This version will be considered by two other students who have to provide a one-page review on this report within one week.
  • All students are expected to be present at all presentations, and participate in discussions.


Guidelines for grading

The final grade is mainly established on the basis of the following ingredients:
  • The quality and contents of the presentations,
  • The quality and contents of the report,
  • The process of dealing with the topic, the initiatives taken and the amount of supervision required,
  • The quality of the review(s),
  • The level of participation in all meetings.


Staff members

dr. Erik de Vink, email: e.p.d.vink@tue.nl
dr.ir. Jeroen Keiren, email: j.j.a.keiren@tue.nl
dr. Bas Luttik, email: s.p.luttik@tue.nl
dr.ir Wieger Wesselink, email: j.w.wesselink@tue.nl
dr.ir Tim Willemse, email: t.a.c.willemse@tue.nl
prof.dr. Herman Geuvers, email: herman@cs.ru.nl
prof.dr.ir. Jan Friso Groote, email: j.f.groote@tue.nl
prof.dr. Hans Zantema, email: h.zantema@tue.nl


Assignments


  • (Keiren) Refining our confidence in refinable partition data structures.
    Efficient algorithms for behavioural equivalences such as stuttering bisimulation and branching bisimulation rely on refinable partition data structures [1]. We recently developed an O(m log n) algorithm for computing branching bisimulation equivalence of labelled transition systems [2], and implemented it in the mCRL2 toolset. Since the proofs of correctness and of the time complexity of the algorithm are highly non-trivial, it is desired to formally verify these proofs. As a stepping stone towards the full verification of the algorithm, in this project you formalise the refinable partition data structures used in the algorithm. For this, you use one of the theorem provers Coq or Isabelle. You also identify and prove some of the properties that the branching bisimulation algorithm requires to hold in the correctness or complexity arguments.

    [1] Valmari, A., Lehtinen, P.: Efficient Minimization of DFAs with Partial Transition Functions. (Links to an external site.) In: Albers, S. and Weil, P. (eds.) STACS. pp. 645–656 Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2008).
    [2] Jansen, D.N. et al.: A simpler O(m log n) algorithm for branching bisimilarity on labelled transition systems (Links to an external site.). (2019).

    (Keiren) Should we preprocess parity games using stuttering bisimulation?
    The model checking problem can be translated into parity games. In the past, several equivalences on parity games have been studied, based on behavioural equivalences from the domain of process theory. In particular, we showed that parity games can be reduced using stuttering bisimulation while preserving the solution. Whether it is actually useful in practice to preprocess a parity game using stuttering bisimulation is not so clear. In our original work [1] we performed experiments that indicate that it is useful to do this preprocessing. However, advances in the implementations of parity game solvers tipped the scales in the other direction, leading me to conclude in my PhD thesis that this preprocessing is generally unwise [2].
    Recently, however, the complexity of the algorithm for stuttering bisimulation equivalence for Kripke structures has been improved from O(mn) to O(m log n), where m is the number of transitions and n is the number of states in a Kripke structure [3]. This improved algorithm has been implemented in the mCRL2 toolset. Additionally, there have been several improvements in the state of the art of parity game solving, using new algorithms and new implementations. A particularly fast parity game solver is Oink [4].
    In this assignment, the O(m log n) algorithm for Kripke structures in the mCRL2 toolset should be adapted to allow reducing parity games. Furthermore, the experiments from [2] should be redone using this new implementation, and using the fastest parity game solvers that are currently available. This should ultimately lead to a recommendation whether we should preprocess parity games using stuttering bisimulation prior to solving or not.

    [1] Cranen, S. et al.: Stuttering Mostly Speeds Up Solving Parity Games (Links to an external site.). In: Bobaru, M. et al. (eds.) NFM. pp. 207-221 Springer, Berlin, Heidelberg (2011).
    [2] Keiren, J.J.A.: Advanced reduction techniques for model checking (Links to an external site.). Eindhoven University of Technology (2013).  (Chapter 5)
    [3] Groote, J.F. et al.: An O(m log n) algorithm for computing stuttering equivalence and branching bisimulation (Links to an external site.). ACM Trans. Comput. Logic. 18, 2, 13:1-13:34 (2017).
    [4] van Dijk, T.: Oink: An Implementation and Evaluation of Modern Parity Game Solvers (Links to an external site.). In: Beyer, D. and Huisman, M. (eds.) TACAS. pp. 291-308 Springer International Publishing, Cham (2018).

  • (De Vink) Spatial Model Checking with mCRL2
    Neural networks are finding invasively their way in many business applications and technological innovation. With the advent of deep learning, image classification and recognition is currently done with high performance and reliability. An inherent drawback though of the approach is what is referred to as ‘explainability’. The underlying algorithms, based on error minimization techniques, are black-box and provide little insight why specific images aren’t recognized or why other images are classified wrongly.
    In their TACAS-paper Belmonte and Ciancia c.s. introduce the spatial modelchecker VoxLogicA, aimed to support the formal analysis of images, in particular in medical applications. With spatial model checking one aims to prove formally, though tool supported, that a spatical model, often an image, has or doesn’t have a particular property. Here, the model is an instance of a so-called closure space, a generalization of the mathematical hallmark of a topological space; the property is specified in a specific modal logic called SLCS, Spatial Logic for Closure Spaces, involving a modality for neighborhood and an path operator.
    The VoxLogicA modelchecker a brand new system built specifically for the SLCS logic. Contrary, mCRL2 is an industrial-size tool suit in which many man year have been invested since the early 90’s. However, the question is not so much whether the same spatial model checking problems addressed with SLCS over closure spaces can be expressed in model checking problems over the µ-calculus over transition systems. Likely this can be achived. But, the question is whether the performance will be acceptable.
    In the proposed project a inital set-up for spatial model checking with mCRL2 is to be constructed and compared with the achievements of VoxLogicA. In a possible follow-up master thesis project the goal is either apply the mCRL2-based approach to the medical applications targetted by VoxLogicA or a theoretical investigation of the mathematical relationship of SLCS and closure models on the one hand, and the ensuing fragment of the µ-calculus and subclass of labeled transition systems, on the other hand. Literature The TACAS paper of Belmonte and Ciancia c.s. is reference [1]. A more elaborate version has appeared in the arXiv-es [2].
    [1] G. Belmonte, V. Ciancia, D. Latella, and M. Massink. Voxlogica: A spatial model checker for declarative image analysis. In TACAS 2019, volume 11427 of Lecture Notes in Computer Science, pages 281–298. Springer, 2019.
    [2] Gina Belmonte, Vincenzo Ciancia, Diego Latella, and Mieke Massink. Voxlogica: a spatial model checker for declarative image analysis (extended version). CoRR, abs/1811.05677, 2018.

  • (Willemse) Fair Testing Preorder
    Behavioural preorders have application in a step-wise software development methodology. In such a methodology, a formal, behavioural specification of a system is refined into an implementation in a step-wise manner. There are many refinement theories; popular ones include the stable failures refinement and the failures-divergence refinement [1] prominently used in the CSP process algebra, but also in industry (e.g. in the Dezyne language, developed by Verum Software Tools, B.V. in the Eindhoven region). Most refinement relations deal with divergences either by ignoring these or by considering these as catastrophic. The refinement relation called Fair Testing [2], however, treats divergences in a special way, allowing for some room of fairness in 'exiting' a divergent computation. The assignment is to study the Fair Testing preorder, compare it to the aforementioned preorders and, e.g., the Impossible Futures relation, or to study the algorithm for deciding the fair testing preorder.

    [1] M. Laveaux, J.F. Groote and T.A.C. Willemse: Correct and Efficient Antichain Algorithms for Refinement Checking. FORTE 2019: 185-203
    [2] Arend Rensink and Walter Vogler: Fair testing. Inf. Comput. 205(2): 125-198 (2007)

  • (Willemse/Wesselink) Program verification using parameterised Boolean equation systems
    The verification of programs and algorithms is often reduced to satisfiability or decision problems in logic. For instance, checking for the absence of null pointer dereferences in an imperative program is equivalent to showing the unsatisfiability of any constraint system that characterises a path through a state where a null pointer is dereferenced. In [1], Higher-order fixed point equation systems are used to verify the correctness of programs. These higher-order fixed point equation systems are closely related to parameterised Boolean equation systems, which, in turn, are used to decide the model checking problem for the first-order modal mu-calculus in mCRL2 [2]. This assignment involves devising an imperative, guarded command-like language and a formalism for annotating programs in this language, and mapping the verification of such annotations to the problem of solving a parameterised Boolean equation system.

    [1] Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, Hiroshi Unno: Temporal Verification of Programs via First-Order Fixpoint Logic. SAS 2019: 413-436
    [2] Jan Friso Groote, Tim A. C. Willemse: Model-checking processes with data. Sci. Comput. Program. 56(3): 251-273 (2005)

  • (Zantema) 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.