Abstract Diagnosis for tccp using a Linear Temporal Logic

Abstract

This extended abstract is a summary of [5], where we provided an automatic decision method to check whether a given property, specified in a linear temporal logic, is valid w.r.t. a tccp program. Our proposal (based on abstract interpretation techniques) does not require to build any model of the program, in constrast with standard verification methods such as model checking. Our results guarantee correctness but, as usual when using an abstract semantics, completeness is lost.