Temporal Logic with Predicate lambda-Abstraction

A predicate linear temporal logic LTL/sub /spl lambda/=/ without quantifiers but with predicate /spl lambda/-abstraction mechanism and equality is considered. The models of LTL/sub /spl 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/sub /spl 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/sub /spl lambda/=/ is not recursively axiomatizable and, therefore, fully automated verification of LTL/sub /spl 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.

Authors

• Alexei Lisitsa 0001
• Igor Potapov

Keywords

• Logic
• Chromium
• Temporal Logic
• Local Memory
• Domain Elements
• Mobile Agents
• Linear Logic
• Set Of Elements
• Moment In Time
• Communication Protocol
• Future Time
• Cardinality Of The Set
• Interpretation Of Changes
• Usual Way
• Additive Constant
• Sequence Of Instructions
• First-order Structure
• Contraposition
• Counter Value
• Modal Logic
• Propositional Logic