Transformations of logic programs on infinite lists

We consider an extension of logic programs, called w-programs, that can be used to define predicates over infinite lists. w-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 w-programs is an extension of the perfect model semantics. We present variants of the familiar unfold/fold rules which can be used for transforming w-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 w-programs. We demonstrate the power of our transformation-based verification methodology by proving some properties of Buchi automata and w-regular languages.