Temporal logic with predicate abstraction

Original · EN

A predicate linear temporal logic LTLλ,₌ without quantifiers but with predicate abstraction mechanism and equality is considered. The models of LTLλ,₌ can be naturally seen as the systems of pebbles (flexible constants) moving over the elements of some (possibly infinite) domain. This allows to use LTLλ,₌ for the specification of dynamic systems using some resources, such as processes using memory locations, mobile agents occupying some sites, etc. On the other hand we show that LTLλ,₌ is not recursively axiomatizable and, therefore, fully automated verification of LTLλ,₌ specifications is not, in general, possible.