Back to Search
Start Over
Sublogics of a branching time logic of robustness.
- Source :
-
Information & Computation . Jun2019, Vol. 266, p126-160. 35p. - Publication Year :
- 2019
-
Abstract
- In this paper we study sublogics of RoCTL*, a recently proposed logic for specifying robustness. RoCTL* allows specifying robustness in terms of properties that are robust to a certain number of failures. RoCTL* is an extension of the branching time logic CTL* which in turn extends CTL by removing the requirement that temporal operators be paired with path quantifiers. In this paper we consider three sublogics of RoCTL*. We present a tableau for RoBCTL*, a bundled variant of RoCTL* that allows fairness constraints to be placed on allowable paths. We then examine two CTL-like restrictions of CTL*. Pair-RoCTL* requires a temporal operator to be paired with a path quantifier; we show that Pair-RoCTL* is as hard to reason about as the full CTL*. State-RoCTL* is restricted to State formulas, and we show that there is a linear truth preserving translation of State-RoCTL into CTL, allowing State-RoCTL to be reasoned about as efficiently as CTL. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 08905401
- Volume :
- 266
- Database :
- Academic Search Index
- Journal :
- Information & Computation
- Publication Type :
- Academic Journal
- Accession number :
- 136014588
- Full Text :
- https://doi.org/10.1016/j.ic.2019.02.003