Combining Logic Programs and Monadic Second Order Logics by Program Transformation

TL;DR

This paper introduces a program synthesis and verification method that transforms formulas of WS1S into logic programs, enabling decision procedures and safety verification for infinite state systems.

Contribution

It presents a novel unfold/fold transformation approach for deriving logic programs from WS1S formulas, combining synthesis and proof capabilities.

Findings

Successfully derives terminating logic programs from WS1S formulas

Provides a decision procedure for WS1S formulas

Verifies safety properties of infinite state systems

Abstract

We present a program synthesis method based on unfold/fold transformation rules which can be used for deriving terminating definite logic programs from formulas of the Weak Monadic Second Order theory of one successor (WS1S). This synthesis method can also be used as a proof method which is a decision procedure for closed formulas of WS1S. We apply our synthesis method for translating CLP(WS1S) programs into logic programs and we use it also as a proof method for verifying safety properties of infinite state systems.