Alchecker: A Tool For Checking Mobile Ambients

Ambient Calculus is widely used in describing the movement of devices and processes. Ambient Logic is a modal logic for specifying the properties of mobile ambients. Although researchers have proposed some model checking algorithms for Ambient Logic, utility tools are still lacking. To this end, we design and implement a general tool for checking mobile ambients, named ALChecker. We also present a case study and an evaluation to demonstrate the usability of the proposed tool.