A Labeled Natural Deduction System for a Fragment of CTL*

We give a sound and complete labeled natural deduction system for an interesting fragment of CTL∗ , namely the until-free version of BCTL∗ . The logic BCTL∗ is obtained by referring to a more general semantics than that of CTL∗ , where we only require that the set of paths in a model is closed under taking suffixes (i.e. is suffix-closed) and is closed under putting together a finite prefix of one path with the suffix of any other path beginning at the same state where the prefix ends (i.e. is fusion-closed). In other words, this logic does not enjoy the so-called limit-closure property of the standard CTL∗ validity semantics.

• Type: Conference
• Year: 2009
• Where: LFCS
• Authors: Andrea Masini, Luca Viganò, Marco Volpe
• Keywords: Artificial Intelligence, CTL∗ Validity Semantics, Interesting Fragment, LFCS 2009, Natural Deduction System