A Tableau for RoBCTL*

Abstract. It can be desirable to specify polices that require a system to achieve some outcome even if a certain number of failures occur. The temporal logic of robustness RoCTL * extends CTL * with operators from Deontic logic, and a novel operator referred to as Robustly [8]. The only known decision procedure for RoCTL * involves a reduction to QCTL*. This paper presents a tableau for the related bundled tree logic RoBCTL*; this is the first decision procedure for RoBCTL*, and al-though non-elementary in degenerate cases has much better performance than the QCTL * based decision procedure for RoCTL*. The degenerate cases where this tableau performs poorly provide clues as to where we might look to prove that RoBCTL * is non-elementary