Implementing a Model Checker for Performability Behaviour
Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser · University of Twente Research Information · 2001
We describe a novel model checking algorithm for analysing the behaviour of stochastic systems with respect to their performability. Systems are modelled as actionlabelled CTMCs, and the properties to be veri#ed are speci#ed with the help of the action-based temporal logic aCSL.