Transformations of logic programs on infinite lists

DOI10.1017/S1471068410000177MaRDI QIDQ3585155zbMATH OpenOpenAlexFDO

Authors Alberto Pettorossi, Maurizio Proietti, Valerio Senni

Publication date 19 August 2010

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1007.4157

zbMATH Keywords

program verificationprogram transformationinfinite lists

Mathematics Subject Classification ID

Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: 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 Buechi automata and omega-regular languages.

Recommendations

• Proving properties of co-logic programs by unfold/fold transformations
• scientific article; zbMATH DE number 176722
• Deciding full branching time logic by program transformation
• scientific article; zbMATH DE number 139622
• Combining logic programs and monadic second order logics by program transformation

Cites work

• scientific article; zbMATH DE number 43398 (Why is no real title available?)
• A Transformation System for Developing Recursive Programs
• A decompositional approach for computing least fixed-points of datalog programs with \(\mathcal Z\)-counters
• BEYOND TAMAKI-SATO STYLE UNFOLD/FOLD TRANSFORMATIONS FOR NORMAL LOGIC PROGRAMS
• Logic programming and negation: A survey
• Temporal logic programming
• Unfold/fold transformation of stratified programs
• Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs

Cited in

(7)

• A transformation scheme for infinitary first-order combinatorics presenting computational level of expressiveness in predicate logic
• Deciding full branching time logic by program transformation
• Combining logic programs and monadic second order logics by program transformation
• Proving properties of co-logic programs by unfold/fold transformations
• Constraint-based correctness proofs for logic program transformations
• scientific article; zbMATH DE number 176722 (Why is no real title available?)
• scientific article; zbMATH DE number 3845031 (Why is no real title available?)

This page was built for publication: Transformations of logic programs on infinite lists

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3585155)