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 条
[41]   Proving soundness of program transformations in optimizing compilation based on temporal logic [J].
Tao, Qiu-Ming ;
Zhao, Chen ;
Guo, Liang .
Ruan Jian Xue Bao/Journal of Software, 2009, 20 (08) :2074-2086
[42]   Events and constraints: A graphical editor for capturing logic requirements of programs [J].
Smith, MH ;
Holzmann, GJ ;
Etessami, K .
FIFTH IEEE INTERNATIONAL SYMPOSIUM ON REQUIREMENTS ENGINEERING, PROCEEDINGS, 2001, :14-22
[43]   Fresh Approaches for Structured Text Programmable Logic Controllers Programs Verification [J].
Siboulet, Emile ;
Pottier, Louen ;
Ranger, Tom ;
Riera, Bernard .
PROCESSES, 2023, 11 (03)
[44]   PARTIAL DEDUCTION OF LOGIC PROGRAMS WRT WELL-FOUNDED SEMANTICS [J].
ARAVINDAN, C ;
DUNG, PM .
LECTURE NOTES IN COMPUTER SCIENCE, 1992, 632 :384-402
[45]   RGITL: A temporal logic framework for compositional reasoning about interleaved programs [J].
Schellhorn, Gerhard ;
Tofan, Bogdan ;
Ernst, Gidon ;
Pfaehler, Joerg ;
Reif, Wolfgang .
ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2014, 71 (1-3) :131-174
[46]   PERMISSION-BASED SEPARATION LOGIC FOR MULTITHREADED JAVA']JAVA PROGRAMS [J].
Amighi, Afshin ;
Haack, Citristian ;
Huisman, Marieke ;
Hurlin, Clement .
LOGICAL METHODS IN COMPUTER SCIENCE, 2015, 11 (01)
[47]   RGITL: A temporal logic framework for compositional reasoning about interleaved programs [J].
Gerhard Schellhorn ;
Bogdan Tofan ;
Gidon Ernst ;
Jörg Pfähler ;
Wolfgang Reif .
Annals of Mathematics and Artificial Intelligence, 2014, 71 :131-174
[48]   PARTIAL DEDUCTION OF LOGIC PROGRAMS WRT WELL-FOUNDED SEMANTICS [J].
ARAVINDAN, C ;
DUNG, PM .
NEW GENERATION COMPUTING, 1994, 13 (01) :45-74
[49]   A Folding Rule for Eliminating Existential Variables from Constraint Logic Programs [J].
Senni, Valerio ;
Pettorossi, Alberto ;
Proietti, Maurizio .
FUNDAMENTA INFORMATICAE, 2009, 96 (03) :373-393
[50]   Specifying Imperative ML-Like Programs Using Dynamic Logic [J].
Maingaud, Severine ;
Balat, Vincent ;
Bubel, Richard ;
Haehnle, Reiner ;
Miquel, Alexandre .
FORMAL VERIFICATION OF OBJECT-ORIENTED SOFTWARE, 2011, 6528 :122-+
12345