M. Laveaux, T. Neele, O. Bunte: The 201808.0 mCRL2 release
In this talk, we will give an overview of the additions and improvements to mCRL2 from the last couple of years. First, the mCRL2 language has been expanded with the possibility to specify probabilistic behaviour. …continue reading
Rick Erkens: Up-to Techniques for Branching Bisimulation
Branching bisimilarity is a notion of behavioral equivalence between processes. To prove that two processes are branching bisimilar one should provide a relation (a set of pairs) containing the two processes, such that the relation …continue reading
Dragan Bosnacki: Analysis of a Boolean Model for Rheumatoid Arthritis Using SMTSolvers
Rheumatoid Arthritis (RA) is an autoimmune disease that affects about one percent of the world population. A medicine for RA has not yet been found, current treatment options only decelerating the progress of the disease. …continue reading
Erik de Vink: Extending Paradigm with Data (Joint work with Luuk Groenewegen and Jan Verschuren)
We discuss an extension of the coordination modelling language Paradigm. The extension is geared towards data-dependent interaction among components, where the coordination is influenced by possibly distributed data. The approach is illustrated by the well-known …continue reading
Tim Willemse: A Comparison of BDD-Based Parity Game Solvers (Joint work with Lisette Sanchez and Wieger Wesselink)
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 …continue reading
Thomas Neele: Fixing mistakes: narrowing the scope of quantifiers in PBESs
In the mCRL2 toolset, formal properties are specified in the modal mu-calculus with data. This formalism allows the use of quantifiers (∀ and ∃) to bind data variables. However, when a user puts a quantifier …continue reading
Joel Garcia: Behavioural modelling of a wafer transport unit using mCRL2
As a master’s student I’m doing an internship with the assignement to design a model for an ASML wafer transport unit. The objective is to model the behaviour of two stages of the wafer transport …continue reading
Omar Alduhaiby: Learning Product Automata
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 …continue reading
Julien Schmaltz: On the definition of block and idle for xMAS automata.
xMAS is a language initially proposed by Intel for architectural modelling and verification. The main feature of xMAS is to enable a boolean encoding of liveness that can be efficiently checked using SAT-based techniques. xMAS …continue reading
Tatiana Shmeleva: Modeling Networks with Infinite Petri Nets
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 …continue reading