Title :
Specifying Properties for Modular Pi-Calculus
Author :
Kitamura, Takashi ; Lin, Huimin
Author_Institution :
Lab. for Comput. Sci., Chinese Acad. of Sci., Beijing
Abstract :
We propose a modal logic for modular pi calculus: a logic to specify both temporal and spatial properties for processes in modular pi calculus. Characterization of process equivalence the logic induce is investigated, and it is shown that the distinguishing power of the logic falls between bisimilarity and structural congruence. Then a model checking algorithm for the logic over the finite-control subset of modular pi calculus is presented, and its correctness proved.
Keywords :
pi calculus; program verification; temporal logic; correctness proving; modal logic; model checking algorithm; modular pi-calculus; process equivalence; spatial properties; temporal properties; Software engineering; Modal Logics; Model checking; process algebra;
Conference_Titel :
Theoretical Aspects of Software Engineering, 2008. TASE '08. 2nd IFIP/IEEE International Symposium on
Conference_Location :
Nanjing
Print_ISBN :
978-0-7695-3249-3
DOI :
10.1109/TASE.2008.36
