Hi.
How would I go about checking that a system where certain actions taking place at some non-deterministic interleaving (let's call it an asynchronous system) is "essentially identical" -- i.e. does not introduce any bugs additional bugs -- to a system where actions can only occur in a certain order (let's call it the synchronous system)? Obviously, the asynchronous system implements the synchronous one, but I'd like to check the other direction. I could specify them both and show that they both satisfy the set of invariants I've defined, but I'm looking for a stronger resemblance, which I can't quite formally define, a resemblance that means that no property on certain "externally observable" behavior, whether explicitly defined or not, could possibly be violated by the asynchronous system. I think what I'm looking for is a manual partial-order reduction, but I'm not quite clear on the formal definition of that, either (although I may need to look into that in more depth).
A bit more concretely, suppose I'm modeling a distributed system where one node may notice a change in another node's state, and at some later time it may notice another change, and I'd like to check whether that nondeterminism is any "worse" than noticing both changes at once (or in two consecutive transitions). If true, my hypothesis would make abstracting the system (i.e., the opposite of refinement) much easier.
Ron