Temporal logic with predicate lambda-abstraction Alexei Lisitsa and Igor Potapov   View Paper (PDF)   Return to Temporal Logic in Computer Science 2 Abstract A predicate linear temporal logic LTL lambda= without quantifiers but with predicate lambda-abstraction mechanism and equality is considered. The models of LTL lambda= 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 lambda= 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 lambda= is not recursively axiomatizable and, therefore, fully automated verification of LTL lambda= 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. ©2006 Association for Computing Machinery