Ambient calculus-based modal logics for mobile ambients