Bisimulations and predicate logic

Abstract

Elementary (first-order) and nonelementary (set-theoretic) aspects of the largest bisimulation are considered with a view toward analyzing operational semantics from the perspective of predicate logic. The notion of a bisimulation is employed in two distinct ways: (i) as an extensional notion of equivalence on programs (or processes) generalizing input/output equivalence (at a cost exceedingover certain transition predicates computable in log space), and (ii) as a tool for analyzing the dependence of transitions on data (which can be shown to be elementary or nonelementary, depending on the formulation of the transitions).