Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909998311800832 |
|---|---|
| author | Nemati, Hamed Dam, Mads |
| author_facet | Nemati, Hamed Dam, Mads |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_18885 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic Nemati, Hamed Dam, Mads Logic in Computer Science 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. |
| title | Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2502.18885 |