Transformations of Logic Programs on Infinite Lists

Details Transformations of Logic Programs on Infinite Lists Transformations of Logic Programs on Infinite Lists

2010-07-23

arxiv.org/abs/1007.4157v1

Theory and Practice of Logic Programming, Volume 10, Special Issue 4-6, 383-399, 2010

Computer Science

Programming Languages

37 pages, including the appendix with proofs. This is an extended version of a paper published in Theory and Practice of Logic

Scientific paper

10.1017/S1471068410000177

We consider an extension of logic programs, called \omega-programs, that can be used to define predicates over infinite lists. \omega-programs allow us to specify properties of the infinite behavior of reactive systems and, in general, properties of infinite sequences of events. The semantics of \omega-programs is an extension of the perfect model semantics. We present variants of the familiar unfold/fold rules which can be used for transforming \omega-programs. We show that these new rules are correct, that is, their application preserves the perfect model semantics. Then we outline a general methodology based on program transformation for verifying properties of \omega-programs. We demonstrate the power of our transformation-based verification methodology by proving some properties of Buechi automata and \omega-regular languages.

Affiliated with

Also associated with

No associations

Rating

Transformations of Logic Programs on Infinite Lists 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 Transformations of Logic Programs on Infinite Lists, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Transformations of Logic Programs on Infinite Lists will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-139133