Sound and complete timed CTL model checking of timed Kripke structures and real-time rewrite theories
TCTL model checker for (dense-)timed Kripke structures in a pointwise semantics. Reduce TCTL model checking from continuous semantics to pointwise semantics. Sound and complete TCTL model checker for time-robust Real-Time Maude models.
timed ctl model checking timed kripke structures real-time maude rewriting logic