Labelled Process Logic

Abstract

This paper develops a complete labelled proof-theoretic framework for process logic --- an extension of dynamic logic in which formulas specify properties of execution traces rather than only final states. The main difficulty is that first-order process logic must reason about concrete computations while preserving temporal information along regular-program traces. Existing compositional calculi cover important fragments but do not provide a complete treatment of full first-order process logic over regular programs. We address this difficulty by enriching process-logic formulas with labels that explicitly record trace and update information during derivations. Based on this construction, we define cyclic labelled proof systems for both propositional and first-order process logic, respectively denoted by \GiiiPPLcyc\ and \GiiiFOPLcyc. We study their soundness and completeness. Their soundness follows from a global progress condition: an invalid cyclic derivation would induce infinitely many strict decreases in a natural-valued counter-example measure. The completeness of \GiiiPPLcyc\ is established by deriving the axioms and rules of the Hilbert system for propositional process logic, while the completeness of \GiiiFOPLcyc\ is obtained relative to the underlying arithmetic theory through the standard arithmetical encoding used for first-order dynamic logic.

arXiv commentRevised from the last version:1. revise the proof of the soundness of G3PPL; 2. Fix several small problems in the proof of the completeness of G3FOPL; 3. Other types or technical details 4. Add some additional recent works for comparison