Branching time and abstraction in bisimulation semantics

摘要: In comparative concurrency semantics, one usually distinguishes between linear time and branching semantic equivalences. Milner's notion of observatin equivalence is often mentioned as the standard example a equivalence. this paper we investigate whether observation really does respect structure processes, find that in presence unobservable action t CCS not case.Therefore, bisimulation introduced which strongly preserves sense it computations together with potentials all intermediate states are passed through, even if silent moves involved. On closed CCS-terms congruence can be completely axiomatized by single axion scheme: a.(t.(y+z)+y)=a.(y+z) (where ranges over actions) usual loaws for strong congruence.We also establish sequential processes preserved under refinement actions, whereas is.For large class turns out same. As far know, protocols have been verified setting happen to fit class, hence valid stronger