Technical Report UWA-CSSE-07-003 May 2007

A Temporal Logic of Robustness

John C. M^cCabe-Dansted, Tim French Mark Reynolds
School of Computer Science & Software Engineering, The University of Western Australia

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.

Keywords: RoCTL*, Decidability, Modal Logic, Robustness, Branching Time Logic, QCTL*