Temporal Representation and Reasoning, International Syposium on (2005)
June 23, 2005 to June 25, 2005
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2005.34
Alexei Lisitsa , University of Liverpool
Igor Potapov , University of Liverpool
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.
I. Potapov and A. Lisitsa, "Temporal Logic with Predicate λ-Abstraction," Proceedings. 12th International Symposium on Temporal Representation and Reasoning(TIME), Burlington, VT, USA, 2005, pp. 147-155.