Events at MetaForum MF 7.084

Parity games are two player games with omega-winning conditions, played on finite graphs. Such games play an important role in verification, satisfiability and synthesis. It is therefore important to identify algorithms that can efficiently deal with large games that arise from such applications. In this paper, we describe our experiments with BDD-based implementations of four …continue reading

Following a discussion with my colleague at University of Radboud Joshua Moerman on learning the product of independent automata, he pursued the subject of independence of outputs while I the independence of inputs. In this presentation I will summarise his recent paper titled ‘Learning Product Automata’ and how it relates to my work. I will …continue reading

A composition and analysis technique is developed for investigation of infinite Petri nets with regular structure, introduced for modeling networks, clusters and computing grids, that also concerns cellular automata and biological systems. A case study of a square grid structure composition and analysis is presented. Parametric specification of Petri nets, parametric representation of infinite systems …continue reading

Currently the mCRL2 toolset uses sequential algorithms exclusively. From these sequential algorithms the term rewriting algorithm often has the most prominent run-time cost. Developing a parallel term rewriting algorithm requires an efficient term library. This library facilitates the creation and destruction of terms. In this presentation I will present several challenges that I encountered while …continue reading

To make my lectures Automated Reasoning more accessible worldwide, I started developing a series of MOOCs (massive open online course). Professional facilities are provided by EIT Digital and Coursera. At the moment 21 lectures have been recorded, each covering around 10 minutes, by which the first MOOC on satisfiability is nearly finished. Roughly this MOOC …continue reading

In this presentation I talk about the problem of approximating the behaviour of middle-sized population models involving non-linear rates. I describe a number of systems, each with a very different non-linear behaviour, and then show that the binomial and Poisson moment closure approximations have the potential to accurately represent the expected behaviour of these models. …continue reading

Legacy software is a prominent bottleneck in modern industry: it is hard and costly to maintain, yet contains valuable knowledge not available elsewhere. Static analysis provides insight by extracting facts from existing code bases. In this talk, I will address complications and progress on my static analysis tooling in Rascal.

The main goal of this talk is to introduce my research to the FSA group and discuss possibilities and opportunities on how this research can be combined with model checking in general and with mCRL2 in particular in the context of the recently accepted TOP project AVVA (Accelerated Verification and Verified Acceleration). I will present …continue reading

In this talk, I will discuss two problems on examining in which cases context-free processes and pushdown processes are the same. In particular, we depart from the well-known case of language equivalence and instead look at processes using process theory and more fine-grained equivalences, such as branching bisimulation and contrasimulation. We identify two difficulties when …continue reading