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
相关论文
共 50 条
[21]   A residualizing semantics for the partial evaluation of functional logic programs [J].
Albert, E ;
Hanus, M ;
Vidal, G .
INFORMATION PROCESSING LETTERS, 2003, 85 (01) :19-25
[22]   Elimination of Local Variables from Definite Logic Programs [J].
Alvez, Javier ;
Lucio, Paqui .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 137 (01) :5-24
[23]   Transformation rules and strategies for functional-logic programs [J].
Moreno, G .
AI COMMUNICATIONS, 2002, 15 (2-3) :163-165
[24]   A Navigation Logic for Recursive Programs with Dynamic Thread Creation [J].
Lakenbrink, Roman ;
Mueller-Olm, Markus ;
Ohrem, Christoph ;
Gutsfeld, Jens .
VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2024, PT II, 2024, 14500 :48-70
[25]   A Temporal Logic for Higher-Order Functional Programs [J].
Okuyama, Yuya ;
Tsukada, Takeshi ;
Kobayashi, Naoki .
STATIC ANALYSIS (SAS 2019), 2019, 11822 :437-458
[26]   PQL - MODAL LOGIC FOR COMPOSITIONAL VERIFICATION OF CONCURRENT PROGRAMS [J].
UCHIHIRA, N .
SYSTEMS AND COMPUTERS IN JAPAN, 1994, 25 (01) :1-16
[27]   Unfolding-based Improvements on Fuzzy Logic Programs [J].
Julian, Pascual ;
Moreno, Gines ;
Penabad, Jaime .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 137 (01) :69-103
[28]   An unfold/fold transformation framework for definite logic programs [J].
Roychoudhury, A ;
Kumar, KN ;
Ramakrishnan, CR ;
Ramakrishnan, IV .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2004, 26 (03) :464-509
[29]   Optimizing Fuzzy Logic Programs by Unfolding, Aggregation and Folding [J].
Guerrero, Juan Antonio ;
Moreno, Gines .
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2008, 219 (0C) :19-34
[30]   Constraint-based correctness proofs for logic program transformations [J].
Pettorossi, Alberto ;
Proietti, Maurizio ;
Senni, Valerio .
FORMAL ASPECTS OF COMPUTING, 2012, 24 (4-6) :569-594
12345