Causal Event Structures with Complete Transformation Rules(Programming)

概要

論文の詳細を見る
Wm propose the causal event structure, a new formal model for concurrent systems in which simultaneity among the events that systems perform is fully considered. Our new model is defined with the following features in its syntax and semantics. The model incorporates a way to express not only enabling and disabling that are conventional but also synchronization among events without using redundant events. A trace, a possible system run, is defined as a sequence of sets of events so that it can represent synchronized occurrences among events explicitly. With these features, we are able to describe a system's specification in a simple, intuitive manner, avoiding the explosion of the number of events. Further, we give a complete set of the transformation rules on the model. Through a transformation rule, a system can be transformed formally into another with. the same traces. Using the transformation rules in this manner, we can infer properties on the event occurrences such as deadlock, conflict, and simultaneity. Their completeness is a desirable feature because it implies that whether two systems are equal in the observed behavior is decidable formally.
一般社団法人情報処理学会の論文
2003-01-15