Transformations of logic programs on infinite lists

被引：2

作者：

Pettorossi, Alberto ^{[1
]}

Senni, Valerio ^{[1
]}

Proietti, Maurizio ^{[2
]}

机构：

[1] Univ Roma Tor Vergata, DISP, I-00133 Rome, Italy

[2] CNR, IASI, I-00185 Rome, Italy

来源：

THEORY AND PRACTICE OF LOGIC PROGRAMMING | 2010年 / 10卷

关键词：

program transformation; program verification; infinite lists; MODEL CHECKING;

D O I：

10.1017/S1471068410000177

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：383 / 399

页数：17

共 28 条

[1] TEMPORAL LOGIC PROGRAMMING [J].

ABADI, M ;

MANNA, Z .

JOURNAL OF SYMBOLIC COMPUTATION, 1989, 8 (03) :277-295

[2]

[Anonymous], 1982, Logic Programming

[3]

[Anonymous], HDB THEORETICAL COMP

[4] LOGIC PROGRAMMING AND NEGATION - A SURVEY [J].

APT, KR ;

BOL, RN .

JOURNAL OF LOGIC PROGRAMMING, 1994, 20 (1-3) :9-71

[5] TRANSFORMATION SYSTEM FOR DEVELOPING RECURSIVE PROGRAMS [J].

BURSTALL, RM ;

DARLINGTON, J .

JOURNAL OF THE ACM, 1977, 24 (01) :44-67

[6]

Clarke EM, 1999, MODEL CHECKING, P1

[7] Constraint-based deductive model checking [J].

Delzanno G. ;

Podelski A. .

International Journal on Software Tools for Technology Transfer, 2001, 3 (3) :250-270

[8] Transformations of CCP programs [J].

Etalle, S ;

Gabbrielli, M ;

Meo, MC .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2001, 23 (03) :304-395

[9]

Fioravanti F, 2004, LECT NOTES COMPUT SC, V3049, P291

[10] A Decompositional Approach for Computing Least Fixed-Points of Datalog Programs with Z-Counters [J].

Laurent Fribourg ;

Hans Olsén .

Constraints, 1997, 2 (3-4) :305-335

← 1 2 3 →