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. © Springer-Verlag Berlin Heidelberg 2009.
CITATION STYLE
Masini, A., Viganò, L., & Volpe, M. (2009). A labeled natural deduction system for a fragment of CTL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5407 LNCS, pp. 338–353). https://doi.org/10.1007/978-3-540-92687-0_23
Mendeley helps you to discover research relevant for your work.