|
| | | |
On the Succinctness of RoCTL*
McCabe-Dansted, J.
It can be desirable to specify policies 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 a "Robustly" (French, McCabe-Dansted & Reynolds 2007). It is known that RoCTL* can be translated into CTL*, but that the translation must be have at least a singly exponential blowup per nested Robustly operator (McCabe-Dansted, Pinchinat, French & Reynolds 2009). We now present a translation that has asymptotically a singly exponential blowup per nested Robustly operator, matching the known lower bound. This translation uses a combination of automata and LTL. This combination is useful not due to greater theoretical expressivity than LTL, but instead because RoCTL* is more naturally expressed as a combination of automaton and LTL operators than LTL operators alone; this combination allows us to avoid the need for a round trip from automata to LTL and back for each nested Robustly operator. |
Cite as: McCabe-Dansted, J. (2011). On the Succinctness of RoCTL*. In Proc. Computing: The Australasian Theory Symposium (CATS 2011) Perth, Australia. CRPIT, 119. Alex Potanin and Taso Viglas Eds., ACS. 85-94 |
(from crpit.com)
(local if available)
|
|