SCIENCE@home

Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic

Mads Dam,Hamed Nemati

Published 2025 in arXiv.org

ABSTRACT

Shared-memory concurrency is difficult to reason about because each thread executes under interference from other threads. At the same time, many correctness arguments for classic algorithms are 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 local histories. Past-time operators support"since"reasoning, while epistemic modalities capture what a given thread can conclude from its own observation history. We give 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 by proving a local knowledge condition that implies mutual exclusion.

PUBLICATION RECORD

CITATION MAP

EXTRACTION MAP

CLAIMS

  • No claims are published for this paper.

CONCEPTS

  • No concepts are published for this paper.

REFERENCES

Showing 1-52 of 52 references · Page 1 of 1

CITED BY