This paper introduces a novel technique to decide the satisfiability of formulaeudwritten in the language of Linear Temporal Logic with both future and pastudoperators and atomic formulae belonging to constraint system D (CLTLB(D) forudshort). The technique is based on the concept of bounded satisfiability, and hingesudon an encoding of CLTLB(D) formulae into QF-EUD, the theory of quantifier-udfree equality and uninterpreted functions combined with D. Similarly to standardudLTL, where bounded model-checking and SAT-solvers can be used as an alternativeudto automata-theoretic approaches to model-checking, our approach allows usersudto solve the satisfiability problem for CLTLB(D) formulae through SMT-solvingudtechniques, rather than by checking the emptiness of the language of a suitableudautomaton. The technique is effective, and it has been implemented in our ZOTudformal verification tool.
展开▼
