Towards an epistemic approach to reasoning about concurrent programs

Abstract

We show how epistemic logic may be used to reason about concurrent programs. Starting out from Halpern & Moses’ interpretation of knowledge in the context of distributed systems, where they use the interleaving model, we extend this to a setting where also truly concurrent computations can be modelled, viz. posets of action labels. Moreover, and more importantly, we prepare grounds for the verification of concurrent programs. We focus on a variant of the well-known 1978-version of Hoare's Concurrent Sequential Processes (CSP) to see how the details work out for a concrete and simple language.