Temporal logic with predicate abstraction

Details Temporal logic with predicate abstraction Temporal logic with predicate abstraction

2004-10-27

arxiv.org/abs/cs/0410072v1

Computer Science

Logic in Computer Science

14 pages, 4 figures

Scientific paper

A predicate linear temporal logic LTL_{\lambda,=} without quantifiers but with predicate 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 is not, in general, possible.

Affiliated with

Also associated with

No associations

Rating

Temporal logic with predicate abstraction does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Temporal logic with predicate abstraction, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Temporal logic with predicate abstraction will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-342180