Axioms for Obligation and Robustness with Temporal Logic

Abstract. RoCTL * was proposed to model and specify the robustness of reactive systems. RoCTL * extended CTL * with the addition of Oblig-atory and Robustly operators, which quantify over failure-free paths and paths with one more failure respectively. This paper gives an axiomati-sation for all the operators of RoCTL * with the exception of the Until operator; this fragment is able to express similar contrary-to-duty obli-gations to the full RoCTL * logic. We call this formal system NORA, and give a completeness proof. We also consider the fragments of the language containing only path quantifiers (but where variables are de-pendent on histories). We examine semantic properties and potential axiomatisations for these fragments.