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] Strong equivalence of logic programs under the infinite-valued semantics
    Nomikos, Christos
    Rondogiannis, Panos
    Wadge, William W.
    INFORMATION PROCESSING LETTERS, 2009, 109 (11) : 576 - 581
  • [22] Neuro-symbolic Representation of Logic Programs Defining Infinite Sets
    Komendantskaya, Ekaterina
    Broda, Krysia
    Garcez, Artur d'Avila
    ARTIFICIAL NEURAL NETWORKS-ICANN 2010, PT I, 2010, 6352 : 301 - +
  • [23] On the power of stratified logic programs with value invention for expressing database transformations
    Cabibbo, L
    DATABASE THEORY - ICDT '95, 1995, 893 : 208 - 221
  • [24] Representation transformations of ordered lists
    Asvanyi, Tibor
    ANNALES MATHEMATICAE ET INFORMATICAE, 2015, 44 : 5 - 13
  • [25] Programs with lists are counter automata
    Bouajjani, Ahmed
    Bozga, Marius
    Habermehl, Peter
    Iosif, Radu
    Moro, Pierre
    Vojnar, Tomas
    FORMAL METHODS IN SYSTEM DESIGN, 2011, 38 (02) : 158 - 192
  • [26] Programs with lists are counter automata
    Bouajjani, Ahmed
    Bozga, Marius
    Habermehl, Peter
    Iosif, Radu
    Moro, Pierre
    Vojnar, Tomas
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2006, 4144 : 517 - 531
  • [27] Programs with lists are counter automata
    Ahmed Bouajjani
    Marius Bozga
    Peter Habermehl
    Radu Iosif
    Pierre Moro
    Tomáš Vojnar
    Formal Methods in System Design, 2011, 38 : 158 - 192
  • [28] Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
    Nagy, Shaan
    Kim, Jinwoo
    Reps, Thomas
    D'Antoni, Loris
    Proceedings of the ACM on Programming Languages, 2024, 8 (OOPSLA2) : 113 - 139
  • [29] TRANSFORMATIONS OF PROGRAMS
    BIRD, R
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1974, 8 (01) : 22 - 35
  • [30] ON INFINITE NIELSEN TRANSFORMATIONS
    MACEDONSKANOSALSKA, O
    MATHEMATICA SCANDINAVICA, 1982, 51 (01) : 63 - 86
12345