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.

A Labeled Natural Deduction System for a Fragment of CTL∗

MASINI, Andrea;VIGANO', Luca;VOLPE, Marco
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.
9783540926863
natural deduction; temporal logic; proof theory; labeled deduction
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/332192
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact