传值进程与移动进程的模型检测方法
|
摘要
并发理论研究并发现象,即多个独立运行的计算主体(进程)相互间通过交换信息(通信)实现协作,以共同完成预定的任务的计算现象。自六七十年代起各种并发理论相继提出并得到广泛研究,例如,Petri Net、进程代数、模态逻辑等。本文的工作主要集中于传值进程理论和移动界程理论上。
模型检测是一种针对并发系统的自动分析与验证技术。其基本原理是用状态迁移图S表示要分析的系统,用模态/时序逻辑公式φ描述要检查的性质。系统是否具有所要求的性质就转化为S是否满足φ,对有限状态系统这个问题是可判定的。和其他验证方法(如:模拟、测试、机器证明等)相比模型检测方法具有两项突出的优点:其一,验证过程完全自动化:其二,当抽象模型不满足逻辑公式时,检测工具会自动产生一个反例来说明为什么不满足,以用于查错和修改。
本文的研究工作主要由传值系统的模型检测方法和移动系统的模型检测方法两部分组成。
在传值进程系统中,本文的工作主要包括三方面:首先本文讨论谓词μ演算和模态图之间的语义等价问题。模态图是谓词μ演算的一种图形表示形式,它的提出是为了克服线性谓词μ演算公式复杂难懂,不利于机器处理的缺点;将谓词μ演算应用到传值进程的模型检测中。本文通过定义嵌套谓词等式系来建立两者之间的联系。提出了从文本公式到模态图的转换算法并证明了转换的正确性。其次,本文研究了传值进程模型检测中诊断信息的生成问题,引入两种有效的诊断信息表示结构:证明图和示例;提出了相应的诊断信息生成算法并予以实现。此外,为了对付模型检测的状态爆炸问题,本文研究了弱谓词μ演算和弱互模拟之间的关系。定义基于STGA的惰性迁移的概念,并证明惰性迁移的前后状态是弱互模拟的,并且在象有限的模型下,它们满足相同的弱谓词μ演算性质。在此基础上提出了传值进程模型检测的一种偏序归约方法,并将该方法集成到已实现的自动检测工具中。
在移动进程系统方面,本文的工作主要是实现了移动界程的模型检测系统。主要工作包括提出移动界程的底层de Bruijn表示;并将其应用到有限控制移动界程的范式表示上,提出了移动界程的有效的底层表示方法。在此基础上实现了带不动点算子的界程逻辑的模型检测算法。该工具是首个能检测带递归性质的移动界程模型检测系统。
Concurrency theory studies the phenomenon of concurrent computation in which many distributed computing agents participate in a common computation task and cooperate with each other by exchanging message (Communication). Since 1960's, a number of concurrency theory have been proposed and extensively studied, including Petri nets, process algebra, modal logic etc. Among them, CCS (Calculus of Communication System) and its variations is one of the most influenced.Model checking is an automatic technique for analysing and verifying finite state concurrent systems. Its basic idea is to model a concurrent system as a state transition graph S and to describe system property as a modal/temporal logic formula φ, then the problem "if system has the desired property" becomes the mathmatical problem "whether S satisfies φ", denoted as S φ. For finite state model S, this is decidable. Generally speaking, model checking enjoys two remarkable virtues: It is fully automatic and when the system fails to satify a desired property, a diagnostic message can be generated which demonstrates a behavior violating the property.The content of the thesis cosists of two parts: model checking methods for value-passing systems and for mobile systems, both based on first-order extensions of μ—calculus.The first part concerns value-passing CCS. Firstly, the consistency between the predicate μ—calculi and modal graphs is studied. To make predicate μ—calculus formulae easier manipulated by computer programs, modal graphs are proposed as a graphical formulation of predicate μ—calculus. With the introduction of predicate equation systems, the semantic consistency between the logic and modal graphs is established. Moreover, a better algorithm is proposed to transform a predicate μ—calculi formula to a modal graph. Secondly, a method is put forward to generate useful diagnostic information in model checking value-passing processes. Two diagnostic forms, proof graphs and witnesses are defined. Correspondingly, their construction algorithms are proposed. The method has been implemented as part of our model checker and tested by several examples. Thirdly, a patial order reduction method for value-passing CCS is proposed to cope with the state-explosion problem. With studies on the relationship between the weak predicate μ—calculi and the weak bisimulation of STGA, it is prove that in value-passing CCS, two weak bisimular processes satisfy the same weak predicate μ—calculus formulae, moreover for finite-image systems reverse statement is also true. The inert transitions in STGAs are defined and it is proved that two states before and after an inert transition
are weak bisimular. Theofore, they satisfy the same weak predicate —calculi formulae. Based on the above results, we propose apatrial order reduction method for value-passing CCS and it is now interiged in our tool.The second part concerns mobile ambients, a process calculus for mobile systems. We implement a model checker for finite-control mobile ambients. First, we propose a de bruijn notation for finite-control mobile ambients and moreover with its normal form, a lower-layer notation for the processes are contructed. The structure congruence realtion and reduction relation for the processes are both implemented. Based on the above results, we implement a model checking algorithm for finite-control mobile ambients which can deal with ambient logic with fixed-point opertors. It is the first such tool for model checking mobile ambients.
模型检测是一种针对并发系统的自动分析与验证技术。其基本原理是用状态迁移图S表示要分析的系统,用模态/时序逻辑公式φ描述要检查的性质。系统是否具有所要求的性质就转化为S是否满足φ,对有限状态系统这个问题是可判定的。和其他验证方法(如:模拟、测试、机器证明等)相比模型检测方法具有两项突出的优点:其一,验证过程完全自动化:其二,当抽象模型不满足逻辑公式时,检测工具会自动产生一个反例来说明为什么不满足,以用于查错和修改。
本文的研究工作主要由传值系统的模型检测方法和移动系统的模型检测方法两部分组成。
在传值进程系统中,本文的工作主要包括三方面:首先本文讨论谓词μ演算和模态图之间的语义等价问题。模态图是谓词μ演算的一种图形表示形式,它的提出是为了克服线性谓词μ演算公式复杂难懂,不利于机器处理的缺点;将谓词μ演算应用到传值进程的模型检测中。本文通过定义嵌套谓词等式系来建立两者之间的联系。提出了从文本公式到模态图的转换算法并证明了转换的正确性。其次,本文研究了传值进程模型检测中诊断信息的生成问题,引入两种有效的诊断信息表示结构:证明图和示例;提出了相应的诊断信息生成算法并予以实现。此外,为了对付模型检测的状态爆炸问题,本文研究了弱谓词μ演算和弱互模拟之间的关系。定义基于STGA的惰性迁移的概念,并证明惰性迁移的前后状态是弱互模拟的,并且在象有限的模型下,它们满足相同的弱谓词μ演算性质。在此基础上提出了传值进程模型检测的一种偏序归约方法,并将该方法集成到已实现的自动检测工具中。
在移动进程系统方面,本文的工作主要是实现了移动界程的模型检测系统。主要工作包括提出移动界程的底层de Bruijn表示;并将其应用到有限控制移动界程的范式表示上,提出了移动界程的有效的底层表示方法。在此基础上实现了带不动点算子的界程逻辑的模型检测算法。该工具是首个能检测带递归性质的移动界程模型检测系统。
Concurrency theory studies the phenomenon of concurrent computation in which many distributed computing agents participate in a common computation task and cooperate with each other by exchanging message (Communication). Since 1960's, a number of concurrency theory have been proposed and extensively studied, including Petri nets, process algebra, modal logic etc. Among them, CCS (Calculus of Communication System) and its variations is one of the most influenced.Model checking is an automatic technique for analysing and verifying finite state concurrent systems. Its basic idea is to model a concurrent system as a state transition graph S and to describe system property as a modal/temporal logic formula φ, then the problem "if system has the desired property" becomes the mathmatical problem "whether S satisfies φ", denoted as S φ. For finite state model S, this is decidable. Generally speaking, model checking enjoys two remarkable virtues: It is fully automatic and when the system fails to satify a desired property, a diagnostic message can be generated which demonstrates a behavior violating the property.The content of the thesis cosists of two parts: model checking methods for value-passing systems and for mobile systems, both based on first-order extensions of μ—calculus.The first part concerns value-passing CCS. Firstly, the consistency between the predicate μ—calculi and modal graphs is studied. To make predicate μ—calculus formulae easier manipulated by computer programs, modal graphs are proposed as a graphical formulation of predicate μ—calculus. With the introduction of predicate equation systems, the semantic consistency between the logic and modal graphs is established. Moreover, a better algorithm is proposed to transform a predicate μ—calculi formula to a modal graph. Secondly, a method is put forward to generate useful diagnostic information in model checking value-passing processes. Two diagnostic forms, proof graphs and witnesses are defined. Correspondingly, their construction algorithms are proposed. The method has been implemented as part of our model checker and tested by several examples. Thirdly, a patial order reduction method for value-passing CCS is proposed to cope with the state-explosion problem. With studies on the relationship between the weak predicate μ—calculi and the weak bisimulation of STGA, it is prove that in value-passing CCS, two weak bisimular processes satisfy the same weak predicate μ—calculus formulae, moreover for finite-image systems reverse statement is also true. The inert transitions in STGAs are defined and it is proved that two states before and after an inert transition
are weak bisimular. Theofore, they satisfy the same weak predicate —calculi formulae. Based on the above results, we propose apatrial order reduction method for value-passing CCS and it is now interiged in our tool.The second part concerns mobile ambients, a process calculus for mobile systems. We implement a model checker for finite-control mobile ambients. First, we propose a de bruijn notation for finite-control mobile ambients and moreover with its normal form, a lower-layer notation for the processes are contructed. The structure congruence realtion and reduction relation for the processes are both implemented. Based on the above results, we implement a model checking algorithm for finite-control mobile ambients which can deal with ambient logic with fixed-point opertors. It is the first such tool for model checking mobile ambients.
引文
[1] S.J. Ambler. A de bruijn notation for the n—calculus. Technical report, Endinbuerge University, 1990. 101
[2] H.R.Anderson. Model checking and boolean braphs. Theoretical Computer Science, 126:3-30, 1994. 22,99
[3] I. Avau B. Vergauwen, J. Lewi and A. Pote. Efficient computation of nested fix-points with applications to model checking. In Proc. of, volume 827 of LNCS, 1994. 99
[4] Hans Bekic. Programming Languages and Their Definition, chapter Definable operations in gernal algbras and the theory of automata and flow charts. Springer, 1984. 23, 39
[5] G.S Bhat and R. Cleaveland. Efficient model checking via the equational μ—calculus. In Proc. of 11th Annual Symposium on Logic in Computer Science, pages 304-312, July 1996. 59, 99
[6] G. Boudol. Asynchrony and the π—calculus. Technical Report Rapport de Recherche 1702, INRIA Sofia-Antipolis, 1992. 5
[7] J. Bradfield and C. Stirling. Hanbook of Process Algebra, chapter Modal Logics and mu-Calculus: An Introduction. Elsiver, 2001. 22,23,64,98
[8] Ramdal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transitions on Computers, 35(8):677-691, 1986. 10
[9] R. Focardi C. Braghin, A. Cortesi. Control flow analysis of mobile ambients with security boundaries. In Proc. of Fifth IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS'02), pages 197-212. Kluwer Academic Publisher, 2002. 102
[10] Luis Caires. Behavioral and spatial observations in a logic for the π—calculus. In Proc. of FOS-SACS'2004, 2004. 101
[11] Luis Caires and Luca Cardelli. A spatial logic for concurrency (part i). In Naoki Kobayashi and Benjamin C. Pierce, editors, TACS 2001, volume 2215 of LNCS. Springer, 2001. 99, 101
[12] Luis Caires and Luca Cardelli. A spatial logic for concurrency (part ii). In Proc. of CONCUR 2002, volume 2421 of LNCS. Springer, 2002. 99
[13] L. Cardelli and A.D. Gorden. Anytime, anywhere: Modal logics for mobile ambients. In Proceedings of the 27th ACM S1GPLAN-SIGACT on Principles of Programming Languages, 2000. 76, 77, 99, 101
[14] L. Cardelli and A.D. Gorden. Mobile ambient. Theoritical Computer Science, 2002. 1, 74, 95, 98
[15] Luca Cardelli and Giorgio Ghelli. A query language based on the ambient logic. In Proc. of ESOP 2001, volume 2028 of LNCS. Springer, 2001. 101
[16] Luca Cardelli and Andrew D. Gorden. Types for mobile ambient. In Proceeding of the 26th ACM SIGPLAN-SIGACT on Principles of Programming Languages, pages 79-92, San Antonio, TX, 1999. ACM Press. 102
[17] Luca Cardelli and Andrew D. Gorden. Logical properties of name restriction. In Samson Abramsky, editor, Proc. ofTLCA 2001, volume 2044 of LNCS. Springer, 2001. 77, 99, 101
[18] Michele Bugliesi Giuseppe Castagna and Sivlvia Crafa. Reasoning about security in mobile ambient. In Proc. of CONCUR 2001, volume 2154 of LNCS, pages 102-120. Springer, 2001. 102
[19] Witold Charatonik and Jean-Marc Talbot. the decidability of model checking mobile ambient. In Proc. ofCSL 2001, volume 2142 of LNCS. Springer, 2001. 76, 79, 80, 101
[20] E. Clarke and J. Wing. Formal method: State of the art and futrue directions. Technical Report CMU-CS-96-178, Computer Science Department, CMU, 1996. 6
[21] S.A. Smolka etc. C.R. Ramakrishnan, I.V. Ramakrishnan. Xmc: A logic-pragmming-based verfication toolset. In Proc. ofCAV'2000, 2000. 100
[22] E. Lozes D. Hirschkoff and D. Sangiorgi. Seperability, expressiveness, and decidability in the ambient logic. In Proc. of, 2002. 102
[23] E. Clarke S. Jha D. Long, A. Browne and W. Marrero. An improved algorithm for the evaluation of fixpoint expressions. In Proc. ofCAV'94, volume 818 of LNCS. Springer, 1994. 23
[24] Mads Dam. Model checking mobile processes. Information and Computation, 129(1):35-51, Augest 1996. 76,98,101
[25] Pascal Zimmer David Teller and Daniel Hirschkoff. Using ambients to control resources. In Proc. of CONCUR 2002,2002. 102
[26] E. A. Emerson E. M. Clarke and A. P. Sistla. Automatic verification of finite-state concurrenct systems using temporal logic specifications. ACM Transition on Programming Languages and Systems, 8(2):244-263, April 1986. 6
[27] K.L. McMillan E.M. Clarke, O. Grumberg and X. Zhao. Efficient generation of counterexamples and witnesses in symbolic model checking. In Proc. ofDAC'95, pages 427-432. ACM, 1995. 99
[28] O. Grumberg E.M. Clarke and D.A. Peled. Model Checking, the MIT Press, 1999. 6
[29] E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proc. 1st IEEE LICS, pages 267-278, 1986. 23
[30] I. Salvo F. Barbanera, M. Dezani-Ciancaglini and V. Sassone. A type inference algorithm for secure ambients. In Proc. ofTOSCA '01, volume 62 of ENTCS. Elsevier, 2001. 102
[31] P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design, 1993. 100
[32] P. Godefroid and P. Wolper. A partial approach to model checking. Information and Computation,1994. 100
[33] XuDong Guan. http://xdguan.freezope.org/wiki/ambientcalculionline. 102
[34] Robert Harper. Programming in standard ml. Departement of Computer Science, CMU. 93
[35] Matthew Hennwssy and X. Liu. A modal logic for message passing processes. Technical Report Roport 3/93, School of Cognitive and Computing Sciences, University of Sussex, 1993. 8, 31, 48, 98
[36] G. Holzmann and D. Peled. An improvement in formal verification. In FORTE 1994, pages 197-211,1995. 11
[37] G. J. Holzmann. The model checker spin. IEEE Transition on Software Engineering, 23(5):279-295, 1997. 11
[38] K. Honda and M. Tokoro. On asynchronous communication semantics. In Proceeding of International Conference on Object-Basded Concurrent Computing, volume 612 of LNCS, pages 21—51. Springer-Verlag, 1992. 5
[39] H.R.Anderson. Verification of Temporal Properties of Concurrent Sytetns. PhD thesis, Arahus, 1993. 23, 24, 99
[40] Anna Ingolfsdottir and Huimin Lin. Handbook of Process Algebra, chapter A Symbolic Approach to Value-Passing Processes. Elsiver, 2001. 1, 98
[41] A. Kerbrat etc. J-C Fernadez, H. Garavel. Cadp: A protocol validation and verification toolbox. In Proc. ofCAV'08, volume 1102 of LNCS, pages 437-440, 1996. 100
[42] K. L. McMillan D. L. Dill J. R. Burch, E. M. Clarke and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. ofLICS'90, pages 428-439. IEEE Computer Society, 1990. 10
[43] S. Katz and D. Peled. Verification of distributed programs using representative interleaving sequences. Distributed Computing, 6:107-120, 1992. 11
[44] A. Kick. Tableaux and witnesses for the μ-calculus. Technical Report D-76128, Faculty of Computer Science, University of Karlsruhe, Karlsruhe, Germany, October 1995. 100
[45] D. Kozen. Resules on the propositional mu-calculus. Theoretical Computer Science, 47:233-241,1983. 98
[46] F. Levi. Types for evolving communication in safe ambients. In Proceedings of VMCAI '03, 2003. 102
[47] Francesca Levi and Chiara Bodei. A control flow analysis for safe and boxed ambients. In Proc. of ESOP'04,2004. 102
[48] Francesca Levi and Sergio Maffeis. On abstract interpretation of mobile ambients. Information and Computation, 188(2): 179-240, January 2004. 102
[49] H. Lin. Symbolic transition graphs with assignment. In Proc. of CONCUR '96, volume 1119 of LNCS, pages 50-65, 1996. 3, 27, 98
[50] H. Lin. Model checking value-passing processes. In Proceeding of 8th Aisa-Pacific Software Engineering Conference, Macau, 2001. 13, 33, 53, 54, 98, 99, 101, 102
[51] H. Lin. A predicate μ—caculus for mobile ambients and model checking. In Proc. of IWFMS 2004, 2004. 13,77,79,81,99, 101
[52] X. Liu. Specification and Decomposition in Concurrency. PhD thesis, Alaborg University, 1992. 46
[53] A. Mader. Verification of Modal Properties Using Boolean Equation Systems. PhD thesis, TMU, 1997. 24,99
[54] R. Mateescu and M. Sighireanu. Efficient on-the-fiy model checking for regular alternation-free mu-calculus. In Proceeding of the 5th International Workshop on Formal Methods for Industrial Critical Systems, 2000. 65, 100
[55] R. Mattescu. Efficient diagnostirc generation for boolean equation systems. In Proc. ofTACAS'2000, volume 1785 of LNCS, pages 251-265, 2000. 65, 99, 100
[56] K. L. McMillan. Symbolic model checking: an approach to the state explosion problem. Technical report, Depprtment of Computer Science, Carnegie-Mellon University, 1992. 11
[57] M. Merro and M. Hennessy. Bisimulation congruences in safe ambients. In Proc. ofPOPL'02, 2002. 102
[58] Massimo Merro and Vladimiro Sassone. Typing and subtyping mobility in boxed ambients. In Proc. CONCUR'02, volume 2421 of LNCS. Springer, 2002. 102
[59] Robin Milner. Communication and Concurrency. Prentice Hall, 1989. 1,98
[60] Robin Milner. The polyadic π-calculus. Technical Report LFCS report ECS-LFCS-91-180, Laboratory for Foundations of Computer Science, Computer Science Department, University of Edinburgh, 1991. 98
[61] Robin Milner. Communicating and Mobile Systems: the π— Calculus. Cambridge University Press, 1999. 1, 14, 17, 18,98
[62] J. Parrow. Handbook of Process Algebra, chapter An Introduction to the π-Calculus. Elsiver, 2001. 1, 98
[63] Lawrence C. Paulson. ML for the Working Programmer. Press of Cambridge University, 1991. 93
[64] D. Peled. Combining partial order reduction with on-the fly model-checking. Formal Methods in System Design, 1996. 100
[65] Riccardo Pucella. Notes on progrmming standard ml of new jersey. Departement of Computer Science, Cornell University, 2001. 93,95
[66] J. Parrow R. Cleaveland and B. Steffen. The concurrency workbench: A semantic-based verification tool for the verification of concurrent systems. ACM Transitions on Programming Languages and Systems, 5(l):36-72, 1993. 11
[67] M. Klein R. Cleaveland and B. Steffen. Faster model checking for the modal mu-calculus. volume 663 of LNCS, 1992. 99
[68] W. Penczek R. Gerth, R. Kuiper and D. Peled. A partial order approach to branching time model checking. Information and Computation, 1997. 100
[69] Y.S. Ramakrishna and S.A. Smolka. Partial-order reduction in the weak modal mu-calculus. In CONCUR, 1997. 66,100
[70] C.R. Ramakrishnan. A model checker for value-passing mu-calculus using logic programming. In Proc. of CAV'2000, 2000. 100
[71] Julian Rathke. Symbolic Techniques for Value-passing Calculi. PhD thesis, University of Sussex, 1997.31,48,98
[72] Julian Rathke and Matthew Hennessy. Local model checking for a value-based modal μ—calculus. In Proc. ofTACAS'97, volume 1281 of LNCS. Springer, 1997. 98
[73] Joachim Parrow Robin Milner and David Walker. Modal logics for mobile processes. Theoretical Computer Science, 114:149-171,1993. 98
[74] Davide Sangiorgi. Extensionality and intensionality of the ambient logic. In Proc. of 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, January 2001. 102
[75] Dmitri Schamschurko. A specification of the corba communication layer in the ambient calculus. In Proc. WADT'99, pages 15-18, 1999. 102
[76] P. Stevens and C. Stirling. Practical model-checking using games. In Proc. ofTACAS'98, volume 1384 of LNCS, pages 85-101, 1998. 100
[77] C.Stirling. Bismulation, model checking and other games. In Proc. of Mathfit intstructional meeting on games and computation, Edinburgh, 1997. 23, 100
[78] C.Stirling. Mo dal and Temporal Logics. Springer, 2001. 23,46
[79] C. Stirling and D. Walker. Local model checking in the modal mu-calculus. Theoretical Computer Science, 89:161-177, 1991. 23, 59
[80] Colin Stirling. Modal and temporal logics for porcesses. In Logics for Concurrency, volume 1043 of LNCS. Springer, 1996. 20, 22, 98
[81] Colin Stirling. Modal and Templar Properties of Processes. Springer, 2001. 18, 20, 22, 98
[82] A. Tarski. A lattice-theoretical fixpoint theorem and its application. Pacific Journal of Mathematics, 1955. 20
[83] A. Vaimari. Error detection by reduced reachability graph detection. In Proc. 9th European Workshop on Application and Theory of Petri Nets, 1988. 100
[84] A. Valmari. A stubborn attack on state explosion. Formal Methods in System Design, 1992. 100
[85] B. Vergauwen and J. Lewi. Efficient local correctioness checking for single and alternating boolean equation systems. In Proc. of ICALP'94, volume 820 of LNCS, 1994. 24, 99
[86] Bjorn Victor. A verification tool for the polyadic π-calculus. Master's thesis, Department of Computer Sciences, Uppsala University, 1994. 101
[87] Bjorn Victor and Faron Moiler. The mobility workbench - a tool for the pi-calculus. In Proc. of CAV'94, volume 818 of LNCS. Springer, 1994. 101
[88] A.D. Gorden W. Chratonik and Jean-Marc Talbot. Finite-control mobile ambient. In ESOP, 2002. 9, 76, 77, 88, 89, 92, 95, 101,102
[89] B. Willems and P. Wolper. Partial-order methods for model checking: From linear time to brachking time. In E. M. Clarke, editor, Proc. of 11th Annual Symposium on Logic in Computer Science. Computer Society Press, 1996. 100
[90] Glynn Winskel. A note on model checking the modal nu-calculus. In ICALP, volume 372 of LNCS, 1989. 23, 80
[91] Andrew D. Gordon Supratik Mukhopadhyay Jean-Marc Talbot Witold Charatonik, Silvano Dal-Zilio. The complexity of model checking mobile ambients. In Proc. of FoSSaCS 2001, volume 2030 of LNCS. Springer, 2001. 76, 101
[92] C.R. Ramakrishnan X. Liu and S.A. Smolka. Fully local and efficient evaluation of alternating fixed points. In Proc. TACAS'98, volume 1384 of LNCS, 1998. 24, 54, 99, 102
[93] S. Dail Zilio. Fixed points in ambient logic, 2001. 101
[94] 方海.π演算模型检测系统的设计与实现.Master's thesis,中国科学院软件研究所,2000.101
[95] 林惠民.传值系统的互模拟与谓词等式系.计算机学报,21(2),1998.99
[96] 林惠民.嵌套谓词等式系与弱互模拟.软件学报,10(11),1998.99
[97] 林惠民.移动进程的空间逻辑.中国科学,2004.101
[98] 张文辉林惠民.模型检测:理论,方法与应用.电子学报,12(30),2002.7
[2] H.R.Anderson. Model checking and boolean braphs. Theoretical Computer Science, 126:3-30, 1994. 22,99
[3] I. Avau B. Vergauwen, J. Lewi and A. Pote. Efficient computation of nested fix-points with applications to model checking. In Proc. of, volume 827 of LNCS, 1994. 99
[4] Hans Bekic. Programming Languages and Their Definition, chapter Definable operations in gernal algbras and the theory of automata and flow charts. Springer, 1984. 23, 39
[5] G.S Bhat and R. Cleaveland. Efficient model checking via the equational μ—calculus. In Proc. of 11th Annual Symposium on Logic in Computer Science, pages 304-312, July 1996. 59, 99
[6] G. Boudol. Asynchrony and the π—calculus. Technical Report Rapport de Recherche 1702, INRIA Sofia-Antipolis, 1992. 5
[7] J. Bradfield and C. Stirling. Hanbook of Process Algebra, chapter Modal Logics and mu-Calculus: An Introduction. Elsiver, 2001. 22,23,64,98
[8] Ramdal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transitions on Computers, 35(8):677-691, 1986. 10
[9] R. Focardi C. Braghin, A. Cortesi. Control flow analysis of mobile ambients with security boundaries. In Proc. of Fifth IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS'02), pages 197-212. Kluwer Academic Publisher, 2002. 102
[10] Luis Caires. Behavioral and spatial observations in a logic for the π—calculus. In Proc. of FOS-SACS'2004, 2004. 101
[11] Luis Caires and Luca Cardelli. A spatial logic for concurrency (part i). In Naoki Kobayashi and Benjamin C. Pierce, editors, TACS 2001, volume 2215 of LNCS. Springer, 2001. 99, 101
[12] Luis Caires and Luca Cardelli. A spatial logic for concurrency (part ii). In Proc. of CONCUR 2002, volume 2421 of LNCS. Springer, 2002. 99
[13] L. Cardelli and A.D. Gorden. Anytime, anywhere: Modal logics for mobile ambients. In Proceedings of the 27th ACM S1GPLAN-SIGACT on Principles of Programming Languages, 2000. 76, 77, 99, 101
[14] L. Cardelli and A.D. Gorden. Mobile ambient. Theoritical Computer Science, 2002. 1, 74, 95, 98
[15] Luca Cardelli and Giorgio Ghelli. A query language based on the ambient logic. In Proc. of ESOP 2001, volume 2028 of LNCS. Springer, 2001. 101
[16] Luca Cardelli and Andrew D. Gorden. Types for mobile ambient. In Proceeding of the 26th ACM SIGPLAN-SIGACT on Principles of Programming Languages, pages 79-92, San Antonio, TX, 1999. ACM Press. 102
[17] Luca Cardelli and Andrew D. Gorden. Logical properties of name restriction. In Samson Abramsky, editor, Proc. ofTLCA 2001, volume 2044 of LNCS. Springer, 2001. 77, 99, 101
[18] Michele Bugliesi Giuseppe Castagna and Sivlvia Crafa. Reasoning about security in mobile ambient. In Proc. of CONCUR 2001, volume 2154 of LNCS, pages 102-120. Springer, 2001. 102
[19] Witold Charatonik and Jean-Marc Talbot. the decidability of model checking mobile ambient. In Proc. ofCSL 2001, volume 2142 of LNCS. Springer, 2001. 76, 79, 80, 101
[20] E. Clarke and J. Wing. Formal method: State of the art and futrue directions. Technical Report CMU-CS-96-178, Computer Science Department, CMU, 1996. 6
[21] S.A. Smolka etc. C.R. Ramakrishnan, I.V. Ramakrishnan. Xmc: A logic-pragmming-based verfication toolset. In Proc. ofCAV'2000, 2000. 100
[22] E. Lozes D. Hirschkoff and D. Sangiorgi. Seperability, expressiveness, and decidability in the ambient logic. In Proc. of, 2002. 102
[23] E. Clarke S. Jha D. Long, A. Browne and W. Marrero. An improved algorithm for the evaluation of fixpoint expressions. In Proc. ofCAV'94, volume 818 of LNCS. Springer, 1994. 23
[24] Mads Dam. Model checking mobile processes. Information and Computation, 129(1):35-51, Augest 1996. 76,98,101
[25] Pascal Zimmer David Teller and Daniel Hirschkoff. Using ambients to control resources. In Proc. of CONCUR 2002,2002. 102
[26] E. A. Emerson E. M. Clarke and A. P. Sistla. Automatic verification of finite-state concurrenct systems using temporal logic specifications. ACM Transition on Programming Languages and Systems, 8(2):244-263, April 1986. 6
[27] K.L. McMillan E.M. Clarke, O. Grumberg and X. Zhao. Efficient generation of counterexamples and witnesses in symbolic model checking. In Proc. ofDAC'95, pages 427-432. ACM, 1995. 99
[28] O. Grumberg E.M. Clarke and D.A. Peled. Model Checking, the MIT Press, 1999. 6
[29] E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proc. 1st IEEE LICS, pages 267-278, 1986. 23
[30] I. Salvo F. Barbanera, M. Dezani-Ciancaglini and V. Sassone. A type inference algorithm for secure ambients. In Proc. ofTOSCA '01, volume 62 of ENTCS. Elsevier, 2001. 102
[31] P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design, 1993. 100
[32] P. Godefroid and P. Wolper. A partial approach to model checking. Information and Computation,1994. 100
[33] XuDong Guan. http://xdguan.freezope.org/wiki/ambientcalculionline. 102
[34] Robert Harper. Programming in standard ml. Departement of Computer Science, CMU. 93
[35] Matthew Hennwssy and X. Liu. A modal logic for message passing processes. Technical Report Roport 3/93, School of Cognitive and Computing Sciences, University of Sussex, 1993. 8, 31, 48, 98
[36] G. Holzmann and D. Peled. An improvement in formal verification. In FORTE 1994, pages 197-211,1995. 11
[37] G. J. Holzmann. The model checker spin. IEEE Transition on Software Engineering, 23(5):279-295, 1997. 11
[38] K. Honda and M. Tokoro. On asynchronous communication semantics. In Proceeding of International Conference on Object-Basded Concurrent Computing, volume 612 of LNCS, pages 21—51. Springer-Verlag, 1992. 5
[39] H.R.Anderson. Verification of Temporal Properties of Concurrent Sytetns. PhD thesis, Arahus, 1993. 23, 24, 99
[40] Anna Ingolfsdottir and Huimin Lin. Handbook of Process Algebra, chapter A Symbolic Approach to Value-Passing Processes. Elsiver, 2001. 1, 98
[41] A. Kerbrat etc. J-C Fernadez, H. Garavel. Cadp: A protocol validation and verification toolbox. In Proc. ofCAV'08, volume 1102 of LNCS, pages 437-440, 1996. 100
[42] K. L. McMillan D. L. Dill J. R. Burch, E. M. Clarke and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. ofLICS'90, pages 428-439. IEEE Computer Society, 1990. 10
[43] S. Katz and D. Peled. Verification of distributed programs using representative interleaving sequences. Distributed Computing, 6:107-120, 1992. 11
[44] A. Kick. Tableaux and witnesses for the μ-calculus. Technical Report D-76128, Faculty of Computer Science, University of Karlsruhe, Karlsruhe, Germany, October 1995. 100
[45] D. Kozen. Resules on the propositional mu-calculus. Theoretical Computer Science, 47:233-241,1983. 98
[46] F. Levi. Types for evolving communication in safe ambients. In Proceedings of VMCAI '03, 2003. 102
[47] Francesca Levi and Chiara Bodei. A control flow analysis for safe and boxed ambients. In Proc. of ESOP'04,2004. 102
[48] Francesca Levi and Sergio Maffeis. On abstract interpretation of mobile ambients. Information and Computation, 188(2): 179-240, January 2004. 102
[49] H. Lin. Symbolic transition graphs with assignment. In Proc. of CONCUR '96, volume 1119 of LNCS, pages 50-65, 1996. 3, 27, 98
[50] H. Lin. Model checking value-passing processes. In Proceeding of 8th Aisa-Pacific Software Engineering Conference, Macau, 2001. 13, 33, 53, 54, 98, 99, 101, 102
[51] H. Lin. A predicate μ—caculus for mobile ambients and model checking. In Proc. of IWFMS 2004, 2004. 13,77,79,81,99, 101
[52] X. Liu. Specification and Decomposition in Concurrency. PhD thesis, Alaborg University, 1992. 46
[53] A. Mader. Verification of Modal Properties Using Boolean Equation Systems. PhD thesis, TMU, 1997. 24,99
[54] R. Mateescu and M. Sighireanu. Efficient on-the-fiy model checking for regular alternation-free mu-calculus. In Proceeding of the 5th International Workshop on Formal Methods for Industrial Critical Systems, 2000. 65, 100
[55] R. Mattescu. Efficient diagnostirc generation for boolean equation systems. In Proc. ofTACAS'2000, volume 1785 of LNCS, pages 251-265, 2000. 65, 99, 100
[56] K. L. McMillan. Symbolic model checking: an approach to the state explosion problem. Technical report, Depprtment of Computer Science, Carnegie-Mellon University, 1992. 11
[57] M. Merro and M. Hennessy. Bisimulation congruences in safe ambients. In Proc. ofPOPL'02, 2002. 102
[58] Massimo Merro and Vladimiro Sassone. Typing and subtyping mobility in boxed ambients. In Proc. CONCUR'02, volume 2421 of LNCS. Springer, 2002. 102
[59] Robin Milner. Communication and Concurrency. Prentice Hall, 1989. 1,98
[60] Robin Milner. The polyadic π-calculus. Technical Report LFCS report ECS-LFCS-91-180, Laboratory for Foundations of Computer Science, Computer Science Department, University of Edinburgh, 1991. 98
[61] Robin Milner. Communicating and Mobile Systems: the π— Calculus. Cambridge University Press, 1999. 1, 14, 17, 18,98
[62] J. Parrow. Handbook of Process Algebra, chapter An Introduction to the π-Calculus. Elsiver, 2001. 1, 98
[63] Lawrence C. Paulson. ML for the Working Programmer. Press of Cambridge University, 1991. 93
[64] D. Peled. Combining partial order reduction with on-the fly model-checking. Formal Methods in System Design, 1996. 100
[65] Riccardo Pucella. Notes on progrmming standard ml of new jersey. Departement of Computer Science, Cornell University, 2001. 93,95
[66] J. Parrow R. Cleaveland and B. Steffen. The concurrency workbench: A semantic-based verification tool for the verification of concurrent systems. ACM Transitions on Programming Languages and Systems, 5(l):36-72, 1993. 11
[67] M. Klein R. Cleaveland and B. Steffen. Faster model checking for the modal mu-calculus. volume 663 of LNCS, 1992. 99
[68] W. Penczek R. Gerth, R. Kuiper and D. Peled. A partial order approach to branching time model checking. Information and Computation, 1997. 100
[69] Y.S. Ramakrishna and S.A. Smolka. Partial-order reduction in the weak modal mu-calculus. In CONCUR, 1997. 66,100
[70] C.R. Ramakrishnan. A model checker for value-passing mu-calculus using logic programming. In Proc. of CAV'2000, 2000. 100
[71] Julian Rathke. Symbolic Techniques for Value-passing Calculi. PhD thesis, University of Sussex, 1997.31,48,98
[72] Julian Rathke and Matthew Hennessy. Local model checking for a value-based modal μ—calculus. In Proc. ofTACAS'97, volume 1281 of LNCS. Springer, 1997. 98
[73] Joachim Parrow Robin Milner and David Walker. Modal logics for mobile processes. Theoretical Computer Science, 114:149-171,1993. 98
[74] Davide Sangiorgi. Extensionality and intensionality of the ambient logic. In Proc. of 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, January 2001. 102
[75] Dmitri Schamschurko. A specification of the corba communication layer in the ambient calculus. In Proc. WADT'99, pages 15-18, 1999. 102
[76] P. Stevens and C. Stirling. Practical model-checking using games. In Proc. ofTACAS'98, volume 1384 of LNCS, pages 85-101, 1998. 100
[77] C.Stirling. Bismulation, model checking and other games. In Proc. of Mathfit intstructional meeting on games and computation, Edinburgh, 1997. 23, 100
[78] C.Stirling. Mo dal and Temporal Logics. Springer, 2001. 23,46
[79] C. Stirling and D. Walker. Local model checking in the modal mu-calculus. Theoretical Computer Science, 89:161-177, 1991. 23, 59
[80] Colin Stirling. Modal and temporal logics for porcesses. In Logics for Concurrency, volume 1043 of LNCS. Springer, 1996. 20, 22, 98
[81] Colin Stirling. Modal and Templar Properties of Processes. Springer, 2001. 18, 20, 22, 98
[82] A. Tarski. A lattice-theoretical fixpoint theorem and its application. Pacific Journal of Mathematics, 1955. 20
[83] A. Vaimari. Error detection by reduced reachability graph detection. In Proc. 9th European Workshop on Application and Theory of Petri Nets, 1988. 100
[84] A. Valmari. A stubborn attack on state explosion. Formal Methods in System Design, 1992. 100
[85] B. Vergauwen and J. Lewi. Efficient local correctioness checking for single and alternating boolean equation systems. In Proc. of ICALP'94, volume 820 of LNCS, 1994. 24, 99
[86] Bjorn Victor. A verification tool for the polyadic π-calculus. Master's thesis, Department of Computer Sciences, Uppsala University, 1994. 101
[87] Bjorn Victor and Faron Moiler. The mobility workbench - a tool for the pi-calculus. In Proc. of CAV'94, volume 818 of LNCS. Springer, 1994. 101
[88] A.D. Gorden W. Chratonik and Jean-Marc Talbot. Finite-control mobile ambient. In ESOP, 2002. 9, 76, 77, 88, 89, 92, 95, 101,102
[89] B. Willems and P. Wolper. Partial-order methods for model checking: From linear time to brachking time. In E. M. Clarke, editor, Proc. of 11th Annual Symposium on Logic in Computer Science. Computer Society Press, 1996. 100
[90] Glynn Winskel. A note on model checking the modal nu-calculus. In ICALP, volume 372 of LNCS, 1989. 23, 80
[91] Andrew D. Gordon Supratik Mukhopadhyay Jean-Marc Talbot Witold Charatonik, Silvano Dal-Zilio. The complexity of model checking mobile ambients. In Proc. of FoSSaCS 2001, volume 2030 of LNCS. Springer, 2001. 76, 101
[92] C.R. Ramakrishnan X. Liu and S.A. Smolka. Fully local and efficient evaluation of alternating fixed points. In Proc. TACAS'98, volume 1384 of LNCS, 1998. 24, 54, 99, 102
[93] S. Dail Zilio. Fixed points in ambient logic, 2001. 101
[94] 方海.π演算模型检测系统的设计与实现.Master's thesis,中国科学院软件研究所,2000.101
[95] 林惠民.传值系统的互模拟与谓词等式系.计算机学报,21(2),1998.99
[96] 林惠民.嵌套谓词等式系与弱互模拟.软件学报,10(11),1998.99
[97] 林惠民.移动进程的空间逻辑.中国科学,2004.101
[98] 张文辉林惠民.模型检测:理论,方法与应用.电子学报,12(30),2002.7