Deciding full branching time logic by program transformation

DOI10.1007/978-3-642-12592-8_2MaRDI QIDQ3558281zbMATH OpenOpenAlexFDO

Authors Alberto Pettorossi, Maurizio Proietti, Valerio Senni

Publication date 4 May 2010

Published in Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL http://eprints.imtlucca.it/1372/1/Senni_LNCS_2010_preprint.pdf

Mathematics Subject Classification ID

Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Transformations of logic programs on infinite lists
• The transformational approach to program development
• Verification of sets of infinite state processes using program transformation
• Deciding full branching time logic
• Combining logic programs and monadic second order logics by program transformation

Cited in

(7)

• On inductive proofs by extended unfold/fold transformation rules
• Extending co-logic programs for branching-time model checking
• Transformations of logic programs on infinite lists
• On Computability of Logical Approaches to Branching-Time Property Verification of Programs
• Fold/unfold transformations for fixpoint logic
• A foundation for flow-based program matching: using temporal logic and model checking
• An exercise in transformational programming: Backtracking and Branch-and- Bound

This page was built for publication: Deciding full branching time logic by program transformation

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