pith. sign in

arxiv: 2606.10961 · v1 · pith:R25TQYFQnew · submitted 2026-06-09 · 💻 cs.LO

Labelled Process Logic

Yuanrui Zhang This is my paper

Pith reviewed 2026-06-27 11:22 UTC · model grok-4.3

classification 💻 cs.LO
keywords process logiclabelled proofscyclic proofsdynamic logicfirst-order logicproof theoryprogram tracesregular programs
0
0 comments X

The pith

Enriching process logic formulas with labels creates a single cyclic proof system that handles both execution traces and first-order computations.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Process logic extends dynamic logic so that formulas can describe properties of entire program execution traces instead of only final states. The paper adds explicit labels to formulas that record trace and update information during derivations, then defines two cyclic proof systems called G3PPL and G3FOPL. Soundness is established by showing that the cyclic conditions produce an infinite descent in a well-founded multiset ordering; completeness follows because the labelled systems derive all the standard rules of process logic and first-order dynamic logic. A reader would care because earlier calculi handled only fragments and kept trace reasoning separate from first-order computation, while this construction supplies a uniform framework for the full first-order case over regular programs.

Core claim

The labelled systems provide a uniform framework for process logic in which trace-based program properties and first-order computations can be handled within the same proof structure for the first time. Formulas are enriched with labels that explicitly record trace and update information. The systems G3PPL and G3FOPL are shown sound via cyclic conditions that enforce infinite descent in a multiset ordering and complete by recovering the established rules of process logic and first-order dynamic logic.

What carries the argument

Cyclic labelled proof systems G3PPL and G3FOPL that attach explicit labels to process-logic formulas to record trace and update information during derivations.

If this is right

  • Trace-based properties and first-order computations are treated inside one derivation rather than in separate calculi.
  • All established proof rules of process logic and first-order dynamic logic become derivable inside the labelled systems.
  • The framework covers the full first-order case over regular programs instead of only fragments.
  • Soundness holds uniformly through the cyclic descent argument for both the propositional and first-order systems.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The labelling method might transfer to other modal or temporal logics that need to track execution history alongside state updates.
  • An implementation in a proof assistant could combine trace checking with first-order automated reasoning for program verification tasks.
  • Similar cyclic labelling could address completeness gaps in related proof systems for regular expressions or automata.

Load-bearing premise

The chosen labels and cyclic conditions are sufficient to capture all necessary trace and update information for arbitrary regular programs without introducing incompleteness or unsoundness.

What would settle it

A concrete regular program together with a first-order process-logic formula that is valid yet underivable in G3FOPL, or invalid yet derivable, would refute the completeness or soundness claim.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 0 minor

Summary. The manuscript develops a cyclic labelled proof-theoretic framework for process logic, extending dynamic logic to reason about execution traces rather than final states. It defines two systems, G3PPL (propositional) and G3FOPL (first-order), by enriching formulas with explicit labels recording trace and update information. Soundness is asserted to follow from cyclic conditions producing infinite descent in a well-founded multiset ordering; completeness is asserted by showing that the labelled systems derive the established rules of process logic and first-order dynamic logic. The central claim is that this yields a uniform framework in which trace-based program properties and first-order computations are handled together for the first time.

Significance. If the soundness and completeness arguments hold, the work would constitute a meaningful advance by supplying the first uniform cyclic-proof treatment of full first-order process logic over regular programs, filling a gap left by prior compositional calculi. The explicit labelling technique is a standard device for preserving temporal information and is applied here in a way that could integrate trace properties with first-order reasoning inside a single proof structure. No machine-checked proofs or parameter-free derivations are reported, but the multiset-descent approach, once fully detailed, would be a verifiable strength.

major comments (2)
  1. [Abstract] Abstract (final paragraph): the soundness claim rests on cyclic conditions yielding infinite descent in a multiset ordering, yet the abstract supplies neither the definition of the cyclic conditions, the precise multiset ordering, nor any verification steps for first-order quantifiers or regular-program composition; this is load-bearing for the soundness assertion.
  2. [Abstract] Abstract (final paragraph): completeness is asserted via derivability of known process-logic and dynamic-logic rules, but no derivation steps, examples, or edge-case checks are provided, leaving open whether the chosen labels and cyclic conditions suffice for arbitrary regular programs without introducing incompleteness.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for these comments on the abstract. The points raised concern the level of detail appropriate for an abstract versus the body of the paper; we address each below and agree to revise the abstract for improved clarity while preserving its summary character.

read point-by-point responses

  1. Referee: [Abstract] Abstract (final paragraph): the soundness claim rests on cyclic conditions yielding infinite descent in a multiset ordering, yet the abstract supplies neither the definition of the cyclic conditions, the precise multiset ordering, nor any verification steps for first-order quantifiers or regular-program composition; this is load-bearing for the soundness assertion.

    Authors: The abstract is a concise overview; the cyclic conditions, the specific well-founded multiset ordering for infinite descent, and the verification steps (including handling of first-order quantifiers and regular-program composition) are defined and proved in Sections 3–5. We agree the abstract could better signal these elements and will revise it to include a brief indication of the descent argument and the relevant sections. revision: yes

  2. Referee: [Abstract] Abstract (final paragraph): completeness is asserted via derivability of known process-logic and dynamic-logic rules, but no derivation steps, examples, or edge-case checks are provided, leaving open whether the chosen labels and cyclic conditions suffice for arbitrary regular programs without introducing incompleteness.

    Authors: The abstract summarizes the completeness result; the explicit derivations of the standard rules of process logic and first-order dynamic logic, together with examples and checks for arbitrary regular programs, appear in Section 6. The manuscript demonstrates that the labelled systems and cyclic conditions are sufficient. We will revise the abstract to note that the completeness proof includes these derivations and covers the required cases. revision: yes

Circularity Check

0 steps flagged

No circularity; derivation self-contained via standard soundness/completeness arguments

full rationale

The paper establishes soundness via infinite descent on a multiset ordering induced by its own cyclic conditions and completeness by explicit derivability of independently known rules from process logic and dynamic logic. No step reduces a claimed result to a fitted parameter, self-definition, or load-bearing self-citation; the labelled enrichment is presented as a technical device whose properties are verified against external benchmarks rather than presupposed. This matches the default expectation of a non-circular proof-theoretic construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The framework rests on standard sequent-calculus background plus the novel labelling discipline and the cyclic descent condition; no free parameters or invented entities are visible in the abstract.

axioms (2)
  • domain assumption Well-founded multiset ordering on labels suffices for soundness of cyclic proofs
    Invoked in the soundness argument (abstract).
  • standard math Standard rules of first-order dynamic logic and process logic are sound and complete in their original presentations
    Used as target for completeness (abstract).

pith-pipeline@v0.9.1-grok · 5702 in / 1310 out tokens · 18732 ms · 2026-06-27T11:22:25.671796+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

24 extracted references · 4 canonical work pages

  1. [1]

    Hammad Ahmad and Jean-Baptiste Jeannin. 2021. A Program Logic to Verify Signal Temporal Logic Specifications of Hybrid Systems. In Proceedings of the 24th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2021). ACM, Nashville, TN, USA, 1–11. https://doi.org/10.1145/3447928.3456648

    work page doi:10.1145/3447928.3456648 2021

  2. [2]

    Bernhard Beckert and Daniel Bruns. 2013. Dynamic Logic with Trace Semantics. InCADE 2013. Springer Berlin Heidelberg, 315–329

    2013

  3. [3]

    2016.Dynamic Logic for Java

    Bernhard Beckert, Vladimir Klebanov, and Benjamin Weiß. 2016.Dynamic Logic for Java. Springer International Publishing, 49–106

    2016

  4. [4]

    Bernhard Beckert and Steffen Schlager. 2001. A Sequent Calculus for First-Order Dynamic Logic with Trace Modalities. InAutomated Reasoning. Springer Berlin Heidelberg, Berlin, Heidelberg, 626–641

    2001

  5. [5]

    Gérard Berry and Georges Gonthier. 1992. The Esterel synchronous programming language: design, semantics, implementation.Science of Computer Programming19, 2 (1992), 87 – 152

    1992

  6. [6]

    James Brotherston, Richard Bornat, and Cristiano Calcagno. 2008. Cyclic proofs of program termination in separation logic.SIGPLAN Not.43, 1 (2008), 101–112

    2008

  7. [7]

    James Brotherston and Alex Simpson. 2007. Complete Sequent Calculi for Induction and Infinite Descent. InLICS 2007. 51–62

    2007

  8. [8]

    Nachum Dershowitz and Zohar Manna. 1979. Proving termination with multiset orderings. InAutomata, Languages and Programming. Springer Berlin Heidelberg, Berlin, Heidelberg, 188–202

    1979

  9. [9]

    Simon Docherty and Reuben N. S. Rowe. 2019. A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic. InTABLEAUX 2019. Springer International Publishing, 335–352

    2019

  10. [10]

    1979.First-Order Dynamic Logic

    David Harel. 1979.First-Order Dynamic Logic. Lecture Notes in Computer Science (LNCS), Vol. 68. Springer

    1979

  11. [11]

    David Harel, Dexter Kozen, and Rohit Parikh. 1982. Process Logic: Expressiveness, Decidability, Completeness.J. Comput. System Sci.25, 2 (1982), 144–170

    1982

  12. [12]

    2000.Dynamic Logic

    David Harel, Dexter Kozen, and Jerzy Tiuryn. 2000.Dynamic Logic. MIT Press

    2000

  13. [13]

    Jean-Baptiste Jeannin and André Platzer. 2014. dTL2: Differential Temporal Dynamic Logic with Nested Temporalities for Hybrid Systems. In Automated Reasoning. Springer International Publishing, Cham, 292–306

    2014

  14. [14]

    R. Milner. 1982.A Calculus of Communicating Systems. Springer-Verlag, Berlin, Heidelberg

    1982

  15. [15]

    Sara Negri. 2005. Proof Analysis in Modal Logic.Journal of Philosophical Logic34, 5–6 (2005), 507–544. https://doi.org/10.1007/s10992-005-2267-3

    work page doi:10.1007/s10992-005-2267-3 2005

  16. [16]

    André Platzer. 2007. Differential Dynamic Logic for Verifying Parametric Hybrid Systems.. InTABLEAUX 2007(2007-09-20). Springer Berlin Heidelberg, 216–232

    2007

  17. [17]

    André Platzer. 2007. A Temporal Dynamic Logic for Verifying Hybrid System Invariants. InLogical Foundations of Computer Science. Springer Berlin Heidelberg, Berlin, Heidelberg, 457–471

    2007

  18. [18]

    2018.Logical Foundations of Cyber-Physical Systems

    André Platzer. 2018.Logical Foundations of Cyber-Physical Systems. Springer

    2018

  19. [19]

    Amir Pnueli. 1977. The temporal logic of programs. In18th Annual Symposium on Foundations of Computer Science (SFCS 1977). 46–57. https: //doi.org/10.1109/SFCS.1977.32

    work page doi:10.1109/sfcs.1977.32 1977

  20. [20]

    Colin Stirling and David Walker. 1991. Local model checking in the modal mu-calculus.Theor. Comput. Sci.89, 1 (1991), 161–177

    1991

  21. [21]

    Yuanrui Zhang. 2025. Parameterized Dynamic Logic – Towards A Cyclic Logical Framework for General Program Specification and Verification. arXiv:2404.18098 [cs.LO] https://arxiv.org/abs/2404.18098

    arXiv 2025

  22. [22]

    Yuanrui Zhang and Zhiming Liu. 2024. A dynamic logic with branching modalities.Journal of Logical and Algebraic Methods in Programming136 (2024), 100921. https://doi.org/10.1016/j.jlamp.2023.100921

    work page doi:10.1016/j.jlamp.2023.100921 2024

  23. [23]

    Yuanrui Zhang and Zhibin Yang. 2026. A Generic Dynamic Logic for Program Reasoning Based on Operational Semantics. InDependable Software Engineering. Theories, Tools, and Applications, Amir Goharshady and Christoph Haase (Eds.). Springer Nature Singapore, Singapore, 93–112. Manuscript submitted to ACM 26 Y. Zhang A Other Proofs of Main Theories A.1 Soundn...

    2026

  24. [24]

    Then from |=𝑋 : 𝜙 ♭ ⇒𝑋 : [𝛼 ∗ 1 ]𝜓 ♭, we also have |=𝑋 : 𝜙 ♭ ⇒𝑋 : 𝜑♭

    By Lemma 7.1, there exists an arithmetical FOL formula 𝜑♭ such that |=[𝛼 ∗ 1 ]𝜓 ♭ ↔𝜑 ♭. Then from |=𝑋 : 𝜙 ♭ ⇒𝑋 : [𝛼 ∗ 1 ]𝜓 ♭, we also have |=𝑋 : 𝜙 ♭ ⇒𝑋 : 𝜑♭. From |=[𝛼 ∗ 1 ]𝜓 ♭ ↔𝜑 ♭, by the soundness of the rules ( [∗]), ( [∪]), ( [𝜙?]) and ( [;]), it is not hard to see that |=𝜑 ♭ ↔ [𝛼 ∗ 1 ]𝜓 ♭ ↔ [true ? ∪𝛼 1 ;𝛼 ∗ 1 ]𝜓 ♭ ↔ 𝜓 ♭ ∧ [𝛼 1] [𝛼∗ 1 ]𝜓 ♭ ↔𝜓 ♭ ∧ [𝛼...