Our logic

RoCTL* • We proposed a new logic, RoCTL * (McCabe-Dansted et al., 2007), for modelling and verifying specifications that deal with • Time (extends CTL*) • Obligation (what the system should do) • Robustness (what the system will do even if n failures occur, etc.) • We motivated its use, apply to simple problems. • We showed that RoCTL * is decidable • We now present a tableau based decision procedure • For a “bundled ” variant RoBCTL* • Extends tableau for BCTL * (Reynolds, 2007