A Transformation Strategy for Verifying Logic Programs on Infinite Lists

We consider an extension of the class of logic programs, called !-programs, that can be used to define predicates over infinite lists. The ω-programs allow us to specify properties of the infinite behaviour of reactive systems and, in general, properties of infinite sequences of events. The semantics of ω-programs is an extension of the perfect model semantics. We present a general methodology based on an extension of the unfold/fold transformation rules which can be used for verifying properties of ω-programs. Then we propose a strategy for the mechanical application of those rules and we demonstrate the power of that strategy by proving some properties of ω-regular languages and Büchi automata