3 papers
cs.LO2026
Verification of Parametric Markov Automata under Time-bounded Reachability
Kevin van de Glind, Matthias Volk, Tim Willemse
Analysis of Markov models is of high importance for formal verification. Until now, analysis of Markov Automata required them to be fully specified, which is a considerable restric…
eess.SY2025
A formal specification of the desired software behaviour of the Princess Marijke lock complex
Jan Friso Groote, Matthias Volk
The Princess Marijke lock complex is a large lock and water-protection installation in the Netherlands between the river Rhine and the Amsterdam-Rijnkanaal -- a large waterway conn…
cs.LO2024
Formal Modelling and Analysis of Slot Machines
Jan Friso Groote, Sander van Heesch, Matthias Volk
Slot machines can have fairly complex behaviour. Determining the RTP (return to player) can be involved, especially when a player has an influence on the course of the game. In thi…