A Polynomial Translation of Mobile Ambients into Safe Petri Nets

Mobile Ambients are a modeling technique suitable to express typical network components and their behaviour e.g.\,processes passing firewalls. We derive a decidable subclass of the MA calculus by a translation into Safe Petri nets. Our translation extends to arbitrary MA processes but finiteness of the net and therefore decidability of reachability is only guaranteed for processes bounded in depth and breadth.