a1 DISP, University of Rome Tor Vergata, Via del Politecnico 1, I-00133 Rome, Italy (e-mail: email@example.com)
a2 IASI-CNR, Viale Manzoni 30, I-00185 Rome, Italy (e-mail: firstname.lastname@example.org)
a3 DISP, University of Rome Tor Vergata, Via del Politecnico 1, I-00133 Rome, Italy (e-mail: email@example.com)
We consider an extension of logic programs, called ω-programs, that can be used to define predicates over infinite lists. ω-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 ω-programs is an extension of the perfect model semantics. We present variants of the familiar unfold/fold rules which can be used for transforming ω-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 ω-programs. We demonstrate the power of our transformation-based verification methodology by proving some properties of Büchi automata and ω-regular languages.
(Received February 07 2010)
(Revised April 10 2010)
(Accepted May 21 2010)