Show description

We interpret sequential composition as concatenation of traces, and parallel composition as a resource-sensitive form of interleaving of traces that enforces mutually exclusive access to each resource. 2 We will exploit this feature later, when we use the semantics to prove soundness of a concurrent separation logic. We start by providing an interpretation of actions using a global notion of state; later we will set up a more refined local notion of state with which it is easier to reason about ownership.

This leads us to the following rigorous formulation of validity. Again we write for Definition 5. The formula that then is valid if for all traces and all of if all local states and such and This definition uses the local enabling relation, so that the quantification ranges over local states consistent with for which Furthermore, this notion of validity involves all traces of not just the sequential traces and not just the finite traces9. When is the empty context and validity of implies the usual notion of partial correctness together with the guaranteed absence of runtime errors.

The quotienting does not increase the transitive closure of the transducer. To explain the idea, let us first build explicitly a transducer for as the union of transducers for Each state of is labeled with a sequence of states from T, resulting from the product construction using copies of T. The result is called the history transducer. The history transducer corresponding to Figure 1(b) is shown below. A. Abdulla et al. Recall minimization algorithms for automata. They are based on building a forward bisimulation on the states, and then carry out minimization by quotienting.