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 条
  • [1] Transformations of logic programs
    Nigiyan, SA
    Khachoyan, LO
    PROGRAMMING AND COMPUTER SOFTWARE, 1997, 23 (06) : 302 - 309
  • [2] Transformations of logic programs
    Nigiyan, S.A.
    Khachoyan, L.O.
    Programmirovanie, (06): : 17 - 28
  • [3] Quantitative Separation Logic and Programs with Lists
    Bozga, Marius
    Iosif, Radu
    Perarnau, Swann
    JOURNAL OF AUTOMATED REASONING, 2010, 45 (02) : 131 - 156
  • [4] Quantitative Separation Logic and programs with lists
    Bozga, Marius
    Iosit, Radu
    Perarnau, Swann
    AUTOMATED REASONING, PROCEEDINGS, 2008, 5195 : 34 - 49
  • [5] Quantitative Separation Logic and Programs with Lists
    Marius Bozga
    Radu Iosif
    Swann Perarnau
    Journal of Automated Reasoning, 2010, 45 : 131 - 156
  • [6] Infinite unfolding and transformations of nondeterministic programs
    Lisper, B
    FUNDAMENTA INFORMATICAE, 2005, 66 (04) : 415 - 439
  • [7] Infinite unfolding and transformations of nondeterministic programs
    Lisper, B., 2005, IOS Press (66)
  • [8] Improving functional logic programs by difference-lists
    Albert, E
    Ferri, C
    Steiner, F
    Vidal, G
    ADVANCES IN COMPUTING SCIENCE-ASIAN 2000, PROCEEDINGS, 2000, 1961 : 237 - 254
  • [9] Transformations of logic programs with goals as arguments
    Pettorossi, A
    Proietti, M
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2004, 4 : 495 - 537
  • [10] Transformations of logic programs related to causality and planning
    Erdem, E
    Lifschitz, V
    LOGIC PROGRAMMING AND NONMONOTONIC REASONING, 1999, 1730 : 107 - 116
12345