Temporal logic with predicate λ-abstraction

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 via validity checking is not, in general, possible. The result is based on computational universality of the above abstract computational model of pebble systems, which is of independent interest due to the range of possible interpretations of such systems.