Labelled Process Logic

Abstract

This paper develops a cyclic 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 propositional and first-order process logic, respectively denoted by G3PPL and G3FOPL. We prove the soundness by using the cyclic conditions to obtain an infinite descent in a well-founded multiset ordering, and prove the completeness by showing that the labelled systems can derive the established proof rules of process logic and first-order dynamic logic. The result is a uniform framework for process logic in which for the first time, trace-based program properties and first-order computations can be handled within the same proof structure.