Refinement Mapping on Partially Ordered Events

35 views
Skip to first unread message

William Schultz

unread,
Feb 9, 2020, 9:19:11 AM2/9/20
to tla...@googlegroups.com
Hello,

I am trying to develop a refinement mapping between two specs H and L, where H is a high level description of a distributed system and L is a lower level one. My belief is that there exists a refinement mapping from L to H that works by re-ordering the events in the lower level spec in accordance with the partial ordering of events in the system. In L, a behavior represents a sequence of events that occur on different nodes of a distributed system. I want my refinement mapping to re-order the states/events of a behavior in a way that both satisfies the partial ordering and gives a valid refinement mapping from L to H. 

For example, consider some transition from state A to state B in L such that there is no causal dependence between A and B i.e. the event that transitioned the system to A and the event that transitioned the system to B can be considered concurrent. If the A -> B transition cannot be made to correspond to any transition in H under a refinement map, but a transition B -> A can be, then it seems that a refinement mapping should be able to take advantage of this freedom to re-order events.

When thinking about how I would define this, such a mapping feels more natural to define over behaviors as opposed to states i.e. defining a function F that maps behaviors in L to behaviors in H where F may re-order states of L. This feels harder to do when only mapping from states in L to states in H. My understanding is that a refinement mapping is defined as function F : S_L -> S_H, where S_L is the set of states of spec L and S_H is the set of states in spec H, such that F maps initial states in L to those in H, and maps transitions in L to transitions in H. From [1] and [2], I understand that in some cases I may need to add auxiliary variables to permit a refinement mapping, but it’s not clear to me yet whether this is required for my scenario. 

Does anyone have any suggestions on a good way to approach this? Or perhaps there is an alternate perspective on this problem that would simplify things. Conceptually, my goal feels reasonable, but I'm unsure how to actually define this in TLA+. I am also interested if this type of refinement mapping (i.e. re-ordering partially ordered events) has appeared elsewhere when defining refinement mappings between specifications of concurrent systems.

david streader

unread,
Feb 25, 2020, 7:06:40 PM2/25/20
to tlaplus
Hi
    If your partial ordering is modeling "true concurrency" (two events are not ordered if they can be be executed in parallel)  for example in process algebra the process  (a->x->b)|| (c->x->d) can execute a and c in any order but must wait till both have been performed before the x event is performed by both sequential components. If not you can safely skip the rest of the comment.

Using a true concurrent semantics still equates the two processes (a->x->b)|| (c->x->d)  and (a->x->d)|| (c->x->b) which may not be desirable. If you extend the high level spec to include the "location" of events (a1->x1->b1)|| (c2->x2->d2) and now all you have to do is forget the locations in order to retrieve the low level spec.

This may be of no help in you situation but I have found these "located" models useful to map back and forth between automata and Petri net (true concurrent/partial order model) representations of processes.
Reply all
Reply to author
Forward
0 new messages