Transformations of logic programs on infinite lists

DOI10.1017/S1471068410000177zbMATH Open1209.68096arXiv1007.4157OpenAlexW2157162154MaRDI QIDQ3585155FDOQ3585155

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)

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.

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

Recommendations

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

zbMATH Keywords

program verificationprogram transformationinfinite lists

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Logic programming and negation: A survey
• Temporal logic programming
• A Transformation System for Developing Recursive Programs
• Unfold/fold transformation of stratified programs
• Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic 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

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
• Title not available (Why is that?)
• Title not available (Why is that?)

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)