A Study On The Potential Active Names of π-Agents

Verification techniques for CCS [Milner, R. “Communication and Concurrency,” Prentice-Hall, Englewood Cliffs, New Jersey, 1989] cannot be directly used to verify π-calculus [Milner, R. “Communicating and Mobile Systems: the π-Calculus,” Cambridge University Press, 1999; J. Inform. Comput. 100 (1992) 1; Parrow, J. An introduction to the π-calculus, in: Bergstra, Ponse and Smolka, editors, Handbook of Process Algebra, Elsevier, 2001 pp. 479–543] agents. Montanari and Pistore [Montanari, U. and M. Pistore, Checking bisimilarity for finitary π-calculus, in: I. Lee and S. A. Smolka, editors, Proceedings of CONCUR '95, LNCS 962 (1995), pp. 42–56] have pointed out that, under certain restrictions, if only active names are considered, labelled transition systems (LTS) for π-agents can be built in order to have tools and algorithms for CCS also used to check some equivalences in π-calculus.There, they suggested a method for calculation of agents active names based on semantic models – the whole LTS is built first and the active names are calculated later on. This paper presents a syntactic characterisation of active names for π-agents. In this way, active names can be calculated for agents expressions instead of its corresponding LTS. The results from this study can be applied to reduce the size of π-agents in verification techniques based on both rewriting and behavioural models