Affiliations: Make Systems, 4000 Regency Parkway, Cary, NC 27511-8502. email: girish@makesys.com | Bell Laboratories, 700 Mountain Ave., Murray Hill, NJ, 07974, USA. email: doron@research.bell-labs.com
Note: [] This paper was written while the first author was at the Department of Computer Science, North Carolina State University, Raleigh, NC 27606, USA, and during a visit to Bell Laboratories. Address for correspondence: Make Systems, 4000 Regency Parkway, Cary, NC 27511-8502, USA.
Note: [] Address for correspondence: Bell Laboratories, 700 Mountain Ave., Murray Hill, NJ, 07974, USA.
Abstract: Modeling execution as partial orders increases the flexibility in reasoning about concurrent programs by allowing the use of alternative, equivalent execution sequences. This is a desirable feature in specifying concurrent systems which allows formalizing frequently used arguments such as ‘in an equivalent execution sequence’, or ‘in a consistent global state, not necessarily on the execution sequence’ to be formalized. However, due to the addition of structure to the model, verification of partial order properties is non-trivial and sparse. We present here a new approach which allows expressing and verifying partial order properties. It is based on modeling an execution as a linear sequence of global states, where each state is equipped with its past partial-order history. The temporal logic BPLTL (for Branching Past Linear Temporal Logic) is introduced. We provide a sound and relatively complete proof system for the logic BPLTL over transitions programs. Our proof system augments an existing proof system for LTL.
