We show that the satisfiability problem for LTL (with past operators) over arithmetic constraints (Constraint LTL) can be answered by solving a finite amount of instances of bounded satisfiability problems when atomic formulae belong to certain suitable fragments of Presburger arithmetic. A formula is boundedly satisfiable when it admits an ultimately periodic model of the form δπ^ω , where δ and π are finite sequences of symbolic valuations. Therefore, for every formula there exists a completeness bound c, such that, if there is no ultimately periodic model with |δπ| ≤ c, then the formula is unsatisfiable.
Completeness of the Bounded Satisfiability Problem for Constraint LTL.
BERSANI, MARCELLO MARIA;FRIGERI, ACHILLE;ROSSI, MATTEO GIOVANNI;SAN PIETRO, PIERLUIGI
2011-01-01
Abstract
We show that the satisfiability problem for LTL (with past operators) over arithmetic constraints (Constraint LTL) can be answered by solving a finite amount of instances of bounded satisfiability problems when atomic formulae belong to certain suitable fragments of Presburger arithmetic. A formula is boundedly satisfiable when it admits an ultimately periodic model of the form δπ^ω , where δ and π are finite sequences of symbolic valuations. Therefore, for every formula there exists a completeness bound c, such that, if there is no ultimately periodic model with |δπ| ≤ c, then the formula is unsatisfiable.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.
