4 papers
Minimal and Canonical Quotients for Simulation Equivalences
Eduardo Costa Martins, Tim Willemse
Quotients have only been studied for a handful of equivalences in the linear time-branching time spectrum, for which there are results pertaining to canonicity and minimality. We e…
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…
Constructing Weakly Terminating Interface Protocols
Debjyoti Bera, Tim A. C. Willemse
Interfaces play a central role in determining compatible component compositions by prescribing permissible interactions between a service provider (server) and its consumers (clien…
Efficient Evidence Generation for Modal -Calculus Model Checking (extended version)
Anna Stramaglia, Jeroen J. A. Keiren, Maurice Laveaux +1
Model checking is a technique to automatically assess whether a model of the behaviour of a system meets its requirements. Evidence explaining why the behaviour does (not) meet its…