Model Checking Mobile Processes

We introduce a temporal logic for the polyadicπ-calculus based on fixed point extensions of Hennessy–Milner logic. Features are added to account for parametrisation, generation, and passing of names, including the use, following Milner, of dependent sum and product to account for (unlocalised) input and output, and explicit parametrisation on names usingλ-abstraction and application. The latter provides a single name binding mechanism supporting all parametrisation needed. A proof system and decision procedure is developed based on Stirling and Walker's approach to model checking the modalμ-calculus using constants. One difficulty, for both conceptual and efficiency-based reasons, is to avoid the explicit use of theω-rule for parametrised processes. A key idea, following Hennessy and Lin's approach to deciding bisimulation for certain types of value-passing processes, is the relativisation of correctness assertions to conditions on names. Based on this idea, a proof system and a decision procedure are obtained for arbitraryπ-calculus processes with finite control, π-calculus correlates of CCS finite-state processes, avoiding the use of parallel composition in recursively defined processes.

Authors

• Mads Dam

Keywords

No keywords are indexed for this paper.