CATALOGO DEI PRODOTTI DELLA RICERCA
IRIS è la soluzione IT che facilita la raccolta e la gestione dei dati relativi alle attività e ai prodotti della ricerca. Fornisce a ricercatori, amministratori e valutatori gli strumenti per monitorare i risultati della ricerca, aumentarne la visibilità e allocare in modo efficace le risorse disponibili.
EnglishWe 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 |
File in questo prodotto:
Copyright © 2021