A Temporal Logic of Robustness

Abstract. It can be desirable to specify polices that require a system to achieve some outcome even if a certain number of failures occur. This paper proposes a logic, RoCTL*, which extends CTL * with operators from Deontic logic, and a novel operator referred to as Robustly. This novel operator acts as variety of path quantifier allowing us to consider paths which deviate from the desired behaviour of the system. Unlike most path quantifiers, the Robustly operator must be evaluated over a path rather than just a state. The Robustly operator represents the phrase "even if an additional failure occurs now or in the future", and thus the paths quantified over depend upon the failures already on the path. This paper examines the expressivity of this new logic, motivates its use and shows that it is decidable