A Timed CTL Model Checker for Real-Time Maude

摘要

This paper describes a recent timed CTL (TCTL) model checker for Real-Time Maude. Our model checker is sound and complete for large classes of systems for which there were previously no TCTL model checkers. Furthermore, since Real-Time Maude also provides a formal analysis back-end to a number of modeling languages, our model checker also equips such languages with a TCTL model checker for free.