## Thomas Neele: Characterising the Winning Strategies in Binary Parity Games with Propositional Logic

A parity game is an infinite-duration game between two players who pass a token around in a directed graph. The problem of “solving” a parity game (deciding which player wins a given node) is an interesting problem since it is in UP and co-UP, but not known to be in P. In a binary parity *…continue reading*

## Pieter van Gelder: Probabilistic risk assessment of civil infrastructural systems

In this lecture I will discuss a number of methods and techniques for the probabilistic risk assessment of civil infrastructural systems, which includes extreme value statistics, system decompositioning techniques, and cost benefit analyses for risk-based optimisation. The flood defence system of the Netherlands will be used as a case study to illustrate the applicability of *…continue reading*

## Anna Stramaglia: Simplifying process parameters of unfolding algebraic data types, and Tom Franken: An Autonomous Data Language

Anna Stramaglia Title: Simplifying process parameters of unfolding algebraic data types Abstract: In preparation for ICTAC 2023, in this talk I will present the work done in collaboration with Jeroen Keiren and Thomas Neele. Complex abstract data types are often used to facilitate creating concise models of the behavior of realistic systems. However, static analysis *…continue reading*

## Valentina Castiglioni: A formal framework for Cyber-Physical Systems

Cyber-Physical Systems (CPS) are characterised by the interaction of various agents operating under highly changing and, sometimes, unpredictable environmental conditions. It is therefore fundamental to verify whether these systems are robust, i.e., whether they are able to function correctly even in perturbed circumstances. In this talk I will recap the achievements of my project on *…continue reading*

## Matthias Volk: Continuous-Time Markov Chains with Imprecisely Timed Observations

Labeled continuous-time Markov chains (CTMCs) describe processes subject to random timing and partial observability. In applications such as runtime monitoring or calculation of remaining useful life, we must incorporate past observations. The timing of these observations matters but they may be uncertain. We consider a setting in which we are given a sequence of imprecisely *…continue reading*

## Flip van Spaendonck: (Semi-)Automate Extraction of Behavioral Models from C++ Code

Accurate behavioral models of software systems can be incredibly useful thanks to the vast array of model based techniques that exist, e.g. automated testing through model based testing, verification of requirements using modal formulas, or providing visual insight using state space visualization techniques. However, acquiring such models can be quite difficult. We propose a set *…continue reading*

## Jan Friso Groote: Numerically solving Real Equation Systems

The quantitative modal mu-calculus is equal to the modal mu-calculus except that formulas yield real values including (-)infinity instead of true or false. Quantitative modal formulas can be translated to parameterised real equation systems (PRESs), and subsequently to real equation systems (RESs), which is quite similar as translating to PBESs and BESs in case of *…continue reading*

## Kevin Jilissen: Behavioral comparison of SysML and Dezyne models

In this talk, I will focus on a work-in-progress behavioral abstraction enabling the comparison of two modelling methods. The first method is an adaption of the current modelling methodology at Rijkswaterstaat for tunnel control systems based on SysML Activity Diagrams, as introduced in my previous talk. The second method relies on the Dezyne specification language *…continue reading*

## Tim Willemse: Model-Driven Engineering meets Model-Based Testing

In this talk, I will focus on a connection between stable-failures refinement and the ioco conformance relation. Both behavioural relations underlie methodologies that have gained traction in industry: stable-failures refinement is used in several commercial Model-Driven Engineering tool suites, whereas the ioco conformance relation is used in Model-Based Testing tools. Refinement-based Model-Driven Engineering approaches promise *…continue reading*

## Anton Wijs: The Hitchhiking Algorithm for Massively Parallel LTL Model Checking

Efficient algorithms have been developed to model check LTL formulae on-the-fly, such as the well-known Nested Depth-First Search, which uses a depth-first search (DFS) strategy. However, in some settings, such as when considering distributed model checking on a cluster, or many-core model checking using a Graphics Processing Unit (GPU), Breadth-First Search (BFS) is a more *…continue reading*