Propositional Linear Temporal Logic (LTL) is well-suited for describing properties of timed systems in which data belong to finite domains. However, when one needs to capture infinite domains, as is typically the case in software systems, extensions of LTL are better suited to be used as specification languages. Constraint LTL (CLTL) and its variant CLTL-over-clocks (CLTLoc) are examples of such extensions; both logics are decidable, and so-called bounded decision procedures based on Satisfiability Modulo Theories (SMT) solving techniques have been implemented for them. In this paper we adapt a previously-introduced bounded decision procedure for LTL based on Bit-Vector Logic to deal with the infinite domains that are typical of CLTL and CLTLoc. We report on a thorough experimental comparison, which was carried out between the existing tool and the new, Bit-Vector Logic-based one, and we show how the latter outperforms the former in the vast majority of cases.
How bit-vector logic can help improve the verification of LTL specifications over infinite domains
BARESI, LUCIANO;ROSSI, MATTEO GIOVANNI
2016-01-01
Abstract
Propositional Linear Temporal Logic (LTL) is well-suited for describing properties of timed systems in which data belong to finite domains. However, when one needs to capture infinite domains, as is typically the case in software systems, extensions of LTL are better suited to be used as specification languages. Constraint LTL (CLTL) and its variant CLTL-over-clocks (CLTLoc) are examples of such extensions; both logics are decidable, and so-called bounded decision procedures based on Satisfiability Modulo Theories (SMT) solving techniques have been implemented for them. In this paper we adapt a previously-introduced bounded decision procedure for LTL based on Bit-Vector Logic to deal with the infinite domains that are typical of CLTL and CLTLoc. We report on a thorough experimental comparison, which was carried out between the existing tool and the new, Bit-Vector Logic-based one, and we show how the latter outperforms the former in the vast majority of cases.File | Dimensione | Formato | |
---|---|---|---|
ae2bvzot_main.pdf
accesso aperto
Descrizione: Versione accettata
:
Post-Print (DRAFT o Author’s Accepted Manuscript-AAM)
Dimensione
352.92 kB
Formato
Adobe PDF
|
352.92 kB | Adobe PDF | Visualizza/Apri |
p1666-baresi.pdf
Accesso riservato
Descrizione: Versione pubblicata
:
Publisher’s version
Dimensione
791.17 kB
Formato
Adobe PDF
|
791.17 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.