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