Deriving structural labelled transitions for mobile ambients

We present a new labelled transition system (lts) for the ambient calculus. Its most important property is that ordinary (strong) bisimulation coincides with (strong) contextual equivalence. The lts is the outcome of the authors’ ongoing work towards developing general techniques and systematic procedures for deriving ltss in the structural (sos) style from the underlying reduction semantics and observability.