Transformations of logic programs on infinite lists

作     者：Pettorossi, Alberto Senni, Valerio Proietti, Maurizio 

作者机构：Univ Roma Tor Vergata DISP I-00133 Rome Italy CNR IASI I-00185 Rome Italy 

出 版 物：《THEORY AND PRACTICE OF LOGIC PROGRAMMING》 

年 卷 期：2010年第10卷第4-6期

页      面：383-399页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0701[理学-数学] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

主　　题：program transformation program verification infinite lists 

摘      要：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 Buchi automata and omega-regular languages.