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.
Titolo: | A Labeled Natural Deduction System for a Fragment of CTL∗ |
Autori: | |
Data di pubblicazione: | 2009 |
Abstract: | 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. |
Handle: | http://hdl.handle.net/11562/332192 |
ISBN: | 9783540926863 |
Appare nelle tipologie: | 04.01 Contributo in atti di convegno |