In: Mazurkiewicz, A.; Winkowski, J.: Lecture Notes in Computer Science, Vol. 1243: CONCUR'97: Concurrency Theory, 8th International Conference, Warshaw, Poland, July 1997, pages 119-134. Germany, Berlin: Springer-Verlag, July 1997.
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 additon 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.