Theory and Practice of Logic Programming

Table of Contents - 2010 - Volume 10, Special Issue 4-6 (26th International Conference on Logic Programming)  

Regular Papers

Transformations of logic programs on infinite lists

ALBERTO PETTOROSSIa1, MAURIZIO PROIETTIa2 and VALERIO SENNIa3

a1 DISP, University of Rome Tor Vergata, Via del Politecnico 1, I-00133 Rome, Italy (e-mail: pettorossi@disp.uniroma2.it)

a2 IASI-CNR, Viale Manzoni 30, I-00185 Rome, Italy (e-mail: maurizio.proietti@iasi.cnr.it)

a3 DISP, University of Rome Tor Vergata, Via del Politecnico 1, I-00133 Rome, Italy (e-mail: senni@disp.uniroma2.it)

Abstract

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)

KEYWORDS:

  • program transformation;
  • program verification;
  • infinite lists