A predicate spatial logic for mobile processes

A modal logic for describing temporal as well as spatial properties of mobile processes, expressed in the asynchronous π-calculus, is presented. The logic has recursive constructs built upon predicate-variables. The semantics of the logic is established and shown to be monotonic, thus guarantees the existence of fixpoints. An algorithm is developed to automatically check if a mobile process has properties described as formulas in the logic. The correctness of the algorithm is proved.