BISIMULATIONS AND PREDICATE LOGIC

Elementary (first-order) and nonelementary (set-theoretic) aspects of the largest bisimulation are considered with a view toward analyzing o perational semantics from the perspective of predicate logic. The noti on of a bisimulation is employed in two distinct ways: (i) as an exten sional notion of equivalence on programs (or processes) generalizing i nput/output equivalence (at a cost exceeding PI1(1) over certain trans ition predicates computable in log space), and (ii) as a tool for anal yzing the dependence of transitions on data (which can be shown to be elementary or nonelementary, depending on the formulation of the trans itions).