Sublogics of a Branching Time Logic of Robustness

McCabe-Dansted, John, Dixon, CL ORCID: 0000-0002-4610-9533, French, Tim and Reynolds, Mark (2019) Sublogics of a Branching Time Logic of Robustness. Information and Computation, 266. pp. 126-160.

Access the full-text of this item by clicking on the Open Access link.

Text elsart3.pdf - Author Accepted Manuscript Download (615kB)

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.

Item Type:	Article
Uncontrolled Keywords:	RoCTL*, bundles, tableau, CTL
Depositing User:	Symplectic Admin
Date Deposited:	01 Mar 2019 08:46
Last Modified:	19 Jan 2023 01:01
DOI:	10.1016/j.ic.2019.02.003
Open Access URL:	http://doi.org/10.1016/j.ic.2019.02.003
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3033512