Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic
For researchers in concurrency verification, this work provides a formal framework that makes epistemic correctness arguments explicit, but it is an incremental extension of existing temporal and epistemic logics.
The paper introduces a past-time temporal epistemic logic for reasoning about shared-memory concurrency, and demonstrates its application to Peterson's mutual exclusion algorithm, showing that epistemic conditions yield global mutual exclusion. The logic also embeds rely-guarantee reasoning, matching classical compatibility obligations.
Shared-memory concurrency is notoriously difficult to reason about because each thread executes under interference from other threads. At the same time, many correctness arguments for classical algorithms are fundamentally epistemic: a thread enters a critical region only when, from its local view, it can rule out that another thread is concurrently in that region. We make such arguments explicit by introducing a past-time temporal epistemic logic interpreted over interleaving executions with perfect recall over local histories. Past-time operators support "since"-style reasoning, while epistemic modalities capture what a given thread can conclude from its own observation history. We give a semantics and a sound proof system, instantiate the logic to a simple shared-memory language with instrumented read/write observations, and illustrate the approach on Peterson's mutual exclusion algorithm: an epistemic condition established at the loop-exit step, combined with ownership-based stability obligations, yields global mutual exclusion. We additionally show how the logic embeds rely-guarantee reasoning as an epistemic stability-lifting principle, yielding a parallel-composition meta-theorem that matches the classical compatibility obligations.