Abstract diagnosis for TCCP using a linear temporal logic