Transition Consistency Help

       The behavior of a system presented by a scenario and basic protocols can be described as a process of matching of messages and local actions defined in the scenario with the same messages and local actions defined in the basic protocols. At each step of this matching the selection of a basic protocol applicable in the current system state must be done. The applicability means that all preconditions are true in a given state. If we want to construct deterministic system then the selection of a protocol must depend only on the action (message or local action), which can be initially performed when a protocol starts (starting action). Therefore each time when some protocol can be applied, there must be only one protocol, which is applicable at this point. This property of basic protocols is called transition consistency.  The applicability of a protocol depends on the current values of state variables and is checked by validating the preconditions of a protocol. The sufficient condition for this type of consistency can be formulated as follows. If preconditions of two basic protocols are intersected, that is the negation of their conjunction cannot be proved or can be refuted, then the processes defined by these protocols must be equivalent as well as their post-conditions.  To prove transition consistency all pairs of basic protocols are considered. For each pair the consistency condition is generated as the negation of conjunction of all preconditions used in protocols. This condition is sent to proof system as a request. If it is proved (for all symbolic values of state variables and parameters), then the consistency is considered as stated: both protocols cannot be applied at the same time. Otherwise (not proved or refuted) the equivalence of respective protocols is checked. This equivalence means that protocols must generate the same traces, and their post-conditions must be equivalent as logic statements (stated by proof system). The comparison of protocols should take into consideration the dependency on parameters. This means that we can compare protocols referring to different instances. But only protocols, which have at least one common instance, are considered. Moreover, common instances should share common action, which is starting action of both protocols (otherwise they are transitionally consistent as defined above).