Concurreny based transition refinement for the verification of distributed algorithms

We suggest a new notion of behaviour preserving transition refinement based on partial order semantics. This notion is called transition refinement. We introduced transition refinement for elementary (low-level) Petri Nets earlier. For modelling and verifying complex distributed algorithms, high-level (Algebraic) Petri nets are usually used. In this paper, we define transition refinement for Algebraic Petri Nets. This notion is more powerful than transition refinement for elementary Petri nets because it corresponds to the simultaneous refinement of several transitions in an elementary Petri net. Transition refinement is particularly suitable for refinement steps that increase the degree of distribution of an algorithm, e.g. when synchronous communication is replaced by asynchronous message passing. We study how to prove that a replacement of a transition is a transition refinement.

Emotions at multiple levels: An integration

Weiss and Isen have provided many supportive comments about the multi-level perspective, but also found limitations. Isen noted the importance of integrating affect, cognition, and motivation. Weiss commented similarly that the model lacked an integrating “thread.” He suggested that, to be truly multilevel, each level should constrain processes at other levels, and also provide guidance for the development of new concepts. Weiss also noted that the focus on biological processes was a strength of the model. I respond by suggesting that these very biological processes may constitute the “missing” thread. To illustrate this, I discuss some of the recent research on emotions in organizational settings, and argue that biology both constrains and guides theory at each level of the model. Based on this proposition, I revisit each of the five levels in the model, to demonstrate how this integration can be accomplished in this fashion. Finally, I address two additional points: aggregation bias, and the possibility of extending the model to include higher levels of industry and region.