Expressiveness and succinctness of a logic of robustness

Journal of Applied Non-Classical Logics 25 (3):193-228 (2015)
  Copy   BIBTEX

Abstract

This paper compares the recently proposed Robust Full Computational Tree Logic to model robustness in concurrent systems with other computational tree logic -based logics. RoCTL* extends CTL* with the addition of the operators Obligatory and Robustly, which quantify over failure-free paths and paths with one more failure respectively. This paper focuses on examining the succinctness and expressiveness of RoCTL* by presenting translations to and from RoCTL*. The core result of this paper is to show that RoCTL* is expressively equivalent to CTL* but is non-elementarily more succinct. That is, RoCTL* does not add any expressive power over CTL*, but can represent some properties using vastly reduced formulae. We present a translation from RoCTL* into CTL* that preserves truth but may result in non-elementary growth in the length of the translated formula, as each nested Robustly operator may result in an extra exponential blowup. However, we show that this translation is optimal in the sense th..

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,593

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Complexity and nicety of fluted logic.William C. Purdy - 2002 - Studia Logica 71 (2):177 - 198.
Relating word and tree automata.Orna Kupferman, Shmuel Safra & Moshe Y. Vardi - 2006 - Annals of Pure and Applied Logic 138 (1):126-146.
Expressive completeness of temporal logic of trees.Bernd-Holger Schlingloff - 1992 - Journal of Applied Non-Classical Logics 2 (2):157-180.
Three-valued logics in modal logic.Barteld Kooi & Allard Tamminga - 2013 - Studia Logica 101 (5):1061-1072.
Truth as translation – part a.Hannes Leitgeb - 2001 - Journal of Philosophical Logic 30 (4):281-307.
Expressive Logics for Coalgebras via Terminal Sequence Induction.Dirk Pattinson - 2004 - Notre Dame Journal of Formal Logic 45 (1):19-33.
Robustness and sensitivity of biological models.Jani Raerinne - 2013 - Philosophical Studies 166 (2):285-303.
On Minimal Models.Francicleber Ferreira & Ana Teresa Martins - 2007 - Logic Journal of the IGPL 15 (5-6):503-526.
Being Wrong: Logics for False Belief.Christopher Steinsvold - 2011 - Notre Dame Journal of Formal Logic 52 (3):245-253.

Analytics

Added to PP
2015-07-16

Downloads
14 (#846,545)

6 months
1 (#1,040,386)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

No citations found.

Add more citations

References found in this work

Deontic logic.G. H. von Wright - 1951 - Mind 60 (237):1-15.
I. deontic logic.G. H. von Wright - 1951 - Mind 60 (237):1-15.
Deontic Logic.G. H. von Wright - 1952 - Journal of Symbolic Logic 17 (2):140-140.
Gentle murder, or the adverbial samaritan.James William Forrester - 1984 - Journal of Philosophy 81 (4):193-197.

View all 8 references / Add more references