A Logical Characterization of Efficiency Preorders

摘要

In this paper we present logical characterizations of two pre-orders, within the framework of Hennessy-Milner Logics. The two pre-orders (loosely termed bisimulation-based efficiency preorders) are on processes represented as labelled transition systems. The characterizations are particularly interesting as they explore preorders lying between strong and weak bisimilarity, guided by a principle of containment which is explained in the Introduction. Even though the proofs of the characterizations use standard methods, there are various subtleties introduced by the nature of the preorders and the logical operators needed to characterize them. The authors have not previously encountered the use of such operators in such simple logics.