This paper introduces a novel technique to decide the satisfiability of formulae written in the language of Linear Temporal Logic with both future and past operators and atomic formulae belonging to constraint system D (CLTLB(D) for short). The technique is based on the concept of bounded satisfiability, and hinges on an encoding of CLTLB(D) formulae into QF-EUD, the theory of quantifier- free equality and uninterpreted functions combined with D. Similarly to standard LTL, where bounded model-checking and SAT-solvers can be used as an alternative to automata-theoretic approaches to model-checking, our approach allows users to solve the satisfiability problem for CLTLB(D) formulae through SMT-solving techniques, rather than by checking the emptiness of the language of a suitable automaton. The technique is effective, and it has been implemented in our ZOT formal verification tool.

Constraint LTL Satisfiability Checking without Automata

BERSANI, MARCELLO MARIA;FRIGERI, ACHILLE;MORZENTI, ANGELO CARLO;PRADELLA, MATTEO;ROSSI, MATTEO GIOVANNI;SAN PIETRO, PIERLUIGI
2014

Abstract

This paper introduces a novel technique to decide the satisfiability of formulae written in the language of Linear Temporal Logic with both future and past operators and atomic formulae belonging to constraint system D (CLTLB(D) for short). The technique is based on the concept of bounded satisfiability, and hinges on an encoding of CLTLB(D) formulae into QF-EUD, the theory of quantifier- free equality and uninterpreted functions combined with D. Similarly to standard LTL, where bounded model-checking and SAT-solvers can be used as an alternative to automata-theoretic approaches to model-checking, our approach allows users to solve the satisfiability problem for CLTLB(D) formulae through SMT-solving techniques, rather than by checking the emptiness of the language of a suitable automaton. The technique is effective, and it has been implemented in our ZOT formal verification tool.
Satisfiability; Constraint LTL; Bounded satisfiability checking
File in questo prodotto:
File Dimensione Formato  
jal-accepted.pdf

accesso aperto

: Post-Print (DRAFT o Author’s Accepted Manuscript-AAM)
Dimensione 605.56 kB
Formato Adobe PDF
605.56 kB Adobe PDF Visualizza/Apri
1-s2.0-S1570868314000615-main.pdf

Accesso riservato

Descrizione: Versione pubblicata
: Publisher’s version
Dimensione 886.13 kB
Formato Adobe PDF
886.13 kB Adobe PDF   Visualizza/Apri

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: https://hdl.handle.net/11311/926558
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 7
social impact