基于符号模型检测若干问题的研究及应用
摘要
在计算机科学中,博弈理论与逻辑的一个非常显著的应用领域是并发系统理论,本文主要围绕模型检测在博弈领域中的应用及形式化逻辑与博弈理论的内部联系展开研究,主要工作有:
1.首先介绍了符号模型检测技术,包括模型检测技术的原理、过程和算法实现。因为符号模型检测的提出最初是为了解决状态爆炸问题,这里我们还介绍了几种解决状态爆炸问题的方法。
2.研究了符号模型检测在博弈游戏中的应用,在符号模型检测方法的理论框架下将两个典型的博弈游戏进行形式化分析。并在符号模型检测工具NuSMV基础上进行修改,加入算法实现了博弈游戏的形式化验证。实验结果证明符号模型检测为解决博弈游戏问题提供了可行的方法。
3.为了减小经典的形式化逻辑和博弈之间的差距,本文从内部进行探索,给出CTL*框架下Kripke结构基础上的2-player博弈,给出了一种博弈规则,并考察了其正确性。博弈模型检测方法的优势在于为公式及公式所表示的属性提供了直观清晰的便于理解的框架。
Model checking is a formal verification technology for limited states concurrent systems. There are many advantages over simulation and theorem provers in verification. In model checking technology,it captures the behavior of reactive systems by a type of state transition graph called Kripke structure , and describes the specification by temporal logic such as computation tree logic (CTL*). The procedure of model checking is to verify whether the system satisfies the specification. In initial years, the state space was explicit expressed and model checking suffered from the state space explosion and the size of the system. Mcmillan dealt with the problem by OBDD and fixpoint theory ofμ?calculus, this method is called symbolic model checking. The advantage of symbolic model checking is that it is able to verify the system properties on the large space of states, which means, it has the ability to search on huge space of states. Recent years, model checking is not only outstanding in the verification of circuits, security protocol, and softwares, but also has played an important role in AI regions such as planning and muti-agent systems.
Game theory has been one of the main areas of the artificial intelligence. In the two-player games, verifying whether there exists winning strategies has not been solved properly, since it refers to the exhaust searches of the finite states space. That is to say no matter how the opponent to move, the player is always able to win. From the point of search technology, it will require exhaustive searches of the states, so the heuristic search technology is not the good methods to solve this problem. But from the point of formal methods, the problem can be summed up a problem of formal verification in the model system. Though the theoretical complexity of solving various games in the literature is well understood, there has been relatively less effort spent in identifying how the powerful symbolic techniques used in model checking fare in solving games with large state-spaces. In formal verification, games have several applications in verifying reactive systems where the agents comprising the system are viewed as players of a game: in modular verification, in compatibility checking of formal interface for modules, in approached to compositional verification. In the paper, games have been used to solve model checking, which is called model checking games.
At the beginning, we put focus on the introduction of basic knowledge of symbolic model checking, including the principles, processes, and algorithms. The main work can be summarized as two points; we first discuss its applications in games, and then explore the relation between model checking and game theory which is called model checking game.
Firstly, we solved two classical games with the method of formulization under the framework of the model checking. The Tic-Tac-Toe game is modeled as a transition system. We designed a game strategy based on winning state and describe the strategy under different frameworks which provides reference methods under these frameworks, and then we gave the corresponding algorithms. And finally we solved the formalized model checking problem using a model checker. Here we solved two classical games, Tic-Tac-Toe and Nim. The two players of the former game both have no winning strategy; while one of the two players in the latter must have winning strategy. We obtain the same results as the literature about Tic-Tac-Toe games and the results is consistent with the actual analysis of Nim. Hence we have reached a conclusion that the symbolic model checking techniques offered a new and significative method for solving games. It also expounds the application areas of the symbolic model checking.
Secondly,we put focus on the model checking games. Model checking games played by two players on the system and the formula provide such features. Answering the question about the property being fulfilled turns out to be equivalent to finding a winning strategy for one of the players. However, verification of traditional model checking is often combined with specification expressed properties with the temporal logic. In fact, regarding aspects of internal structure, the gap between classical formal logics and game-oriented language is very large. We address the question of relating classical formal logics and game logics with regard to their fine-structure, and try to bridge the gap between these in a specific setting concerning the CTL* based on the Kripke structure. Here, we solve model checking problem by the method of games. We defined CTL * model checking games, and we gave the rules under the framework of the game, then the conditions when a play ends and the definition of victory in the model checking games. Then we can apply these rules to play games and look for a winning strategy to answer the question about the property being fulfilled. In this paper, we cited an example and have given a detailed explanation. Finally, we showed the connectedness of the model checking games.
The bottleneck of symbolic model checking is the memory space occupied by BDDs, and it’s impossible to carry on verifications directly using the techniques of symbolic model checking for the games with complex rules and large state-spaces. The regularly used min-max search is a good method in games, in which a sophisticated evaluates states. However, model checking winning state is much significative in this case because knowing which states are winning states can be helpful in evaluating the states in min-max search.
In contrast to automata-theoretic approached it is not necessary to take a detour via satisfiability checking first. The main advantage of games in logics is to provide a clear understanding of formulas and the properties they express. There are various models for the concurrent system and the model checking for CTL* was an early one. As being introduced in chapter 2, CTL* subsumes other temporal logics like LTL and CTL, and thus the results on the games for CTL* easily carry over to these other logics as well.
1.首先介绍了符号模型检测技术,包括模型检测技术的原理、过程和算法实现。因为符号模型检测的提出最初是为了解决状态爆炸问题,这里我们还介绍了几种解决状态爆炸问题的方法。
2.研究了符号模型检测在博弈游戏中的应用,在符号模型检测方法的理论框架下将两个典型的博弈游戏进行形式化分析。并在符号模型检测工具NuSMV基础上进行修改,加入算法实现了博弈游戏的形式化验证。实验结果证明符号模型检测为解决博弈游戏问题提供了可行的方法。
3.为了减小经典的形式化逻辑和博弈之间的差距,本文从内部进行探索,给出CTL*框架下Kripke结构基础上的2-player博弈,给出了一种博弈规则,并考察了其正确性。博弈模型检测方法的优势在于为公式及公式所表示的属性提供了直观清晰的便于理解的框架。
Model checking is a formal verification technology for limited states concurrent systems. There are many advantages over simulation and theorem provers in verification. In model checking technology,it captures the behavior of reactive systems by a type of state transition graph called Kripke structure , and describes the specification by temporal logic such as computation tree logic (CTL*). The procedure of model checking is to verify whether the system satisfies the specification. In initial years, the state space was explicit expressed and model checking suffered from the state space explosion and the size of the system. Mcmillan dealt with the problem by OBDD and fixpoint theory ofμ?calculus, this method is called symbolic model checking. The advantage of symbolic model checking is that it is able to verify the system properties on the large space of states, which means, it has the ability to search on huge space of states. Recent years, model checking is not only outstanding in the verification of circuits, security protocol, and softwares, but also has played an important role in AI regions such as planning and muti-agent systems.
Game theory has been one of the main areas of the artificial intelligence. In the two-player games, verifying whether there exists winning strategies has not been solved properly, since it refers to the exhaust searches of the finite states space. That is to say no matter how the opponent to move, the player is always able to win. From the point of search technology, it will require exhaustive searches of the states, so the heuristic search technology is not the good methods to solve this problem. But from the point of formal methods, the problem can be summed up a problem of formal verification in the model system. Though the theoretical complexity of solving various games in the literature is well understood, there has been relatively less effort spent in identifying how the powerful symbolic techniques used in model checking fare in solving games with large state-spaces. In formal verification, games have several applications in verifying reactive systems where the agents comprising the system are viewed as players of a game: in modular verification, in compatibility checking of formal interface for modules, in approached to compositional verification. In the paper, games have been used to solve model checking, which is called model checking games.
At the beginning, we put focus on the introduction of basic knowledge of symbolic model checking, including the principles, processes, and algorithms. The main work can be summarized as two points; we first discuss its applications in games, and then explore the relation between model checking and game theory which is called model checking game.
Firstly, we solved two classical games with the method of formulization under the framework of the model checking. The Tic-Tac-Toe game is modeled as a transition system. We designed a game strategy based on winning state and describe the strategy under different frameworks which provides reference methods under these frameworks, and then we gave the corresponding algorithms. And finally we solved the formalized model checking problem using a model checker. Here we solved two classical games, Tic-Tac-Toe and Nim. The two players of the former game both have no winning strategy; while one of the two players in the latter must have winning strategy. We obtain the same results as the literature about Tic-Tac-Toe games and the results is consistent with the actual analysis of Nim. Hence we have reached a conclusion that the symbolic model checking techniques offered a new and significative method for solving games. It also expounds the application areas of the symbolic model checking.
Secondly,we put focus on the model checking games. Model checking games played by two players on the system and the formula provide such features. Answering the question about the property being fulfilled turns out to be equivalent to finding a winning strategy for one of the players. However, verification of traditional model checking is often combined with specification expressed properties with the temporal logic. In fact, regarding aspects of internal structure, the gap between classical formal logics and game-oriented language is very large. We address the question of relating classical formal logics and game logics with regard to their fine-structure, and try to bridge the gap between these in a specific setting concerning the CTL* based on the Kripke structure. Here, we solve model checking problem by the method of games. We defined CTL * model checking games, and we gave the rules under the framework of the game, then the conditions when a play ends and the definition of victory in the model checking games. Then we can apply these rules to play games and look for a winning strategy to answer the question about the property being fulfilled. In this paper, we cited an example and have given a detailed explanation. Finally, we showed the connectedness of the model checking games.
The bottleneck of symbolic model checking is the memory space occupied by BDDs, and it’s impossible to carry on verifications directly using the techniques of symbolic model checking for the games with complex rules and large state-spaces. The regularly used min-max search is a good method in games, in which a sophisticated evaluates states. However, model checking winning state is much significative in this case because knowing which states are winning states can be helpful in evaluating the states in min-max search.
In contrast to automata-theoretic approached it is not necessary to take a detour via satisfiability checking first. The main advantage of games in logics is to provide a clear understanding of formulas and the properties they express. There are various models for the concurrent system and the model checking for CTL* was an early one. As being introduced in chapter 2, CTL* subsumes other temporal logics like LTL and CTL, and thus the results on the games for CTL* easily carry over to these other logics as well.
引文
[1] O.Grumberg, E.M.Clarke and D.A.Peled. Model Checking. The MIT Press, Cambridge, MA, 2000, 37-96.
[2] G.Holzmann. The spin model checker. IEEE Transaction on Software Engineering, 1997, 23:279-295.
[3] E.M.Clarke, E.A.Emerson, and A.Prasad Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In Proc. 10th Annual ACM Symposium on Principles of Programming Language, Austin, Texas, 1983, 117-126,
[4] A.Biere, A.Cimatti, E.Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. TACAS, 1999, Volume 1579 of LNCS, 193-207.
[5] J.R.Burch, E.M.Clarke, K.L.McMillan, D.L.Dill and L.J.Hwang. Symbolic model checking: 1020 states and beyond, In Proc. Symposium on Logic in Computer Science, 1990, IEEE, 428-439.
[6] R.E.Bryant. Graph-based algorithms for boolean function manipulation. In Proc.IEEE Transactions on Computers, 1986, C-35(8), 224-296.
[7] A.Cimatti, E.Clarke, E.Giunchiglia, F.Giunchiglia, M. Pistore, M. Roveri, R.Sebastiani, and A. Tacchella. NuSMV Version 2: An Open Source Tool for Symbolic Model Checking. In Proc. International Conference on Computer-Aided Verification (CAV 2002), July 2002, LNCS 2404, 156-188.
[8] Stefan Edelkamp. Symbolic exploration in two-player games: Preliminary results. In The International Conference on AI Planning & Scheduling (AIPS), Workshop on Model Checking, Toulouse, France, 2002. 40-48.
[9] E.M.Clarke and E.A.Emerson. Design and synthesis of synchronizationskeletons using branching time temporal logic. In Proc. Logic of Programs: Workshop, Yorktown Heights, 1981, LNCS 131, 245-269.
[10] E.M.Clarke, E.A.Emerson, and A.P.Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. In Proc. ACM Transactions on Programming Languages and Systems, 1986, 8(2), 244-263.
[11] Randal E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 1992. 24(3):293- 318.
[12] Z.Mamma and A.Pnuell, Temporal Verification of Reactive Systems: Specification, Springer-Verlag, 1992.
[13] E.A.Emerson.and C-L.Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proc. ACM Transactions on Programming Languages and Systems, 2002, 21(6), 244-263.
[14] R. Alur, T.A. Henzinger, O.Kupferman. Alternating-time Temporal Logic, 38th IEEE Symposium on Foundations of Computer Science, 1997, 100-109.
[15] R. Alur, T.A. Henzinger, F.Y.C. Mang, S.Qadeer, S.K.Rajamani, and S. Tasiran, MOCHA: Modularity in model checking. In Proc. of the 10th Int’l Conf. on Computer-aided Verification, Springer-Verlag, 1998, LNCS 1427, 521-525.
[16] V.Antti. A stubborn attack on state explosion. Formal Methods in System Design, 1992, 1(4):297-322.
[17] S.Katz, D.Peled. Verification of distributed programs using representative interleaving sequences [J]. Distributed Computing, 1992, 6:107-120.
[18] J.Gerard Holzmann, Doron Peled. An improvement in formal verification[A]. 7th IFIP WG6. International Conference on Formal Description Techniques VII(FORTE 1994)[C]. London: Chapman andHall, 1995, 197-211.
[19] G.J.Holzmann. Design and Validation of Computers Protocols [M]. New Jersey: Prentice Hall, 1991.
[20] E.A.Emenson, A.P.Sistla. Symmetry and model checking[A]. Lecture Notes in Computer Science 697-5th International Conference on Computer Aided Verification [C]. Berlin: Springer-Verlag, 1993, 463-478.
[21] E.M.Clarke, O.Grumberg, D E Long, Model checking and abstraction [J]. ACM Transactions on Programming Languages and Systems, 1994, 16(5): 1512-1542.
[22] J.R.Burch, E.M.Clarke, D.E.Long. Symbolic model checking with partitioned transition relations. Proceedings of the International Conference on Very Large Scale Integration, Edinburgh, Scotland, 1991, 49-58.
[23] E.M. Clarke, O. Grumberg, D. Long. Verification tools for finite estate concurrent system. In A Decade of Concurrency–Reflections and Perspectives, 1993, LNCS 803, 124-175.
[24] W.Visser and H.Barringer. Practical CTL model checking: Should SPIN be extended? International Journal on Software Tools for Technology Transfer, 2000, 2, 350–365.
[25] A.Church. Logic, arithmetics, and automata. In Proc. of the International Congress of Mathematicians, 1962, 23-35, Institute Mittag-Leffler, 1963.
[26] P.J.G. Ra, adge, and W.M. Wonham. The control of discrete event systems. Proc. of the IEEE, 1989, 77:88-98.
[27] W.Thomas. Infinite games and verification. In Proc. of the 14th Int’l Conf. on Computer-Aided Verifications, Springer-Verlag, 2002, LNCS 2404, 58-64.
[28] Michael Baldamus, Klaus Schneider, Michael Wenz, and Roberto Ziller.Can American Checkers be solved by means of symbolic model checking? In Howard Bowman, editor, Formal Methods Elsewhere, volume 43 of Electronic Notes in Theoretical Computer Science. Elsevier, 2001.
[29] P.Madhusudan, W.Nam, R. Alur. Symbolic computation techniques for solving games, Working shop on Bounded Model Checking, 2003.
[30] D. Berwanger, Games and logical expressiveness. PhD thesis, RWTH Aachen, 2005.
[31] R.J.Aumann, What is game theory trying to accomplish? in Frontiers of Economics, K. Arrow and S. Honkapohja, eds., Basil Blackwell, 1985.
[32] L.Henkin, Some remarks on infinitely long formulas, in Proceedings of the Symposium on Foundations of Mathematics: Infinitistic Methods, Polish Scientific Publishers, 1961, 167–183.
[33] J.Hintikka, Language-games for quantifiers, in Studies in Logical Theory, N.Rescher, ed., vol. f American Philosophical Quarterly Monograph Series, Basil Blackwell, 1968, 46–72.
[34] A.Ehrenfeucht, An application of games to the completeness problem for formalized theories, Fundamental Mathematics, 1961,49, 129–141.
[35] Dexter Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333–354, December 1983.
[36] C.Stirling. Games for bisimulation and model checking, June 1997. Notes for Mathfit instructional meeting on games and computation, Edinburgh http://www.dcs.ed.ac.uk/home/cps/mathfit.ps.
[37] C.Stirling. Local model checking games. In Proceedings of the 6th International Conference on Concurrency Theory, CONCUR’95, I. Lee and S. A. Smolka, eds, volume 962 of Lecture Notes in Computer Science, Springer, 1995, 1–11.
[38] M. Lange and C.Stirling. Focus games for satisfiability and completeness of temporal logic. In Proceedings of the 16th AnnualIEEE Symposium on Logic in Computer Science, LICS’01. IEEE Computer Society Press, 2001.
[39] Berlekamp, Conway, Guy, Winning Ways. BERLEKAMP, E., CONWAY, J.H., GUY, R.K. Academic Press, London 1982.
[2] G.Holzmann. The spin model checker. IEEE Transaction on Software Engineering, 1997, 23:279-295.
[3] E.M.Clarke, E.A.Emerson, and A.Prasad Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. In Proc. 10th Annual ACM Symposium on Principles of Programming Language, Austin, Texas, 1983, 117-126,
[4] A.Biere, A.Cimatti, E.Clarke, and Y. Zhu. Symbolic model checking without BDDs. In Proc. TACAS, 1999, Volume 1579 of LNCS, 193-207.
[5] J.R.Burch, E.M.Clarke, K.L.McMillan, D.L.Dill and L.J.Hwang. Symbolic model checking: 1020 states and beyond, In Proc. Symposium on Logic in Computer Science, 1990, IEEE, 428-439.
[6] R.E.Bryant. Graph-based algorithms for boolean function manipulation. In Proc.IEEE Transactions on Computers, 1986, C-35(8), 224-296.
[7] A.Cimatti, E.Clarke, E.Giunchiglia, F.Giunchiglia, M. Pistore, M. Roveri, R.Sebastiani, and A. Tacchella. NuSMV Version 2: An Open Source Tool for Symbolic Model Checking. In Proc. International Conference on Computer-Aided Verification (CAV 2002), July 2002, LNCS 2404, 156-188.
[8] Stefan Edelkamp. Symbolic exploration in two-player games: Preliminary results. In The International Conference on AI Planning & Scheduling (AIPS), Workshop on Model Checking, Toulouse, France, 2002. 40-48.
[9] E.M.Clarke and E.A.Emerson. Design and synthesis of synchronizationskeletons using branching time temporal logic. In Proc. Logic of Programs: Workshop, Yorktown Heights, 1981, LNCS 131, 245-269.
[10] E.M.Clarke, E.A.Emerson, and A.P.Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. In Proc. ACM Transactions on Programming Languages and Systems, 1986, 8(2), 244-263.
[11] Randal E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 1992. 24(3):293- 318.
[12] Z.Mamma and A.Pnuell, Temporal Verification of Reactive Systems: Specification, Springer-Verlag, 1992.
[13] E.A.Emerson.and C-L.Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proc. ACM Transactions on Programming Languages and Systems, 2002, 21(6), 244-263.
[14] R. Alur, T.A. Henzinger, O.Kupferman. Alternating-time Temporal Logic, 38th IEEE Symposium on Foundations of Computer Science, 1997, 100-109.
[15] R. Alur, T.A. Henzinger, F.Y.C. Mang, S.Qadeer, S.K.Rajamani, and S. Tasiran, MOCHA: Modularity in model checking. In Proc. of the 10th Int’l Conf. on Computer-aided Verification, Springer-Verlag, 1998, LNCS 1427, 521-525.
[16] V.Antti. A stubborn attack on state explosion. Formal Methods in System Design, 1992, 1(4):297-322.
[17] S.Katz, D.Peled. Verification of distributed programs using representative interleaving sequences [J]. Distributed Computing, 1992, 6:107-120.
[18] J.Gerard Holzmann, Doron Peled. An improvement in formal verification[A]. 7th IFIP WG6. International Conference on Formal Description Techniques VII(FORTE 1994)[C]. London: Chapman andHall, 1995, 197-211.
[19] G.J.Holzmann. Design and Validation of Computers Protocols [M]. New Jersey: Prentice Hall, 1991.
[20] E.A.Emenson, A.P.Sistla. Symmetry and model checking[A]. Lecture Notes in Computer Science 697-5th International Conference on Computer Aided Verification [C]. Berlin: Springer-Verlag, 1993, 463-478.
[21] E.M.Clarke, O.Grumberg, D E Long, Model checking and abstraction [J]. ACM Transactions on Programming Languages and Systems, 1994, 16(5): 1512-1542.
[22] J.R.Burch, E.M.Clarke, D.E.Long. Symbolic model checking with partitioned transition relations. Proceedings of the International Conference on Very Large Scale Integration, Edinburgh, Scotland, 1991, 49-58.
[23] E.M. Clarke, O. Grumberg, D. Long. Verification tools for finite estate concurrent system. In A Decade of Concurrency–Reflections and Perspectives, 1993, LNCS 803, 124-175.
[24] W.Visser and H.Barringer. Practical CTL model checking: Should SPIN be extended? International Journal on Software Tools for Technology Transfer, 2000, 2, 350–365.
[25] A.Church. Logic, arithmetics, and automata. In Proc. of the International Congress of Mathematicians, 1962, 23-35, Institute Mittag-Leffler, 1963.
[26] P.J.G. Ra, adge, and W.M. Wonham. The control of discrete event systems. Proc. of the IEEE, 1989, 77:88-98.
[27] W.Thomas. Infinite games and verification. In Proc. of the 14th Int’l Conf. on Computer-Aided Verifications, Springer-Verlag, 2002, LNCS 2404, 58-64.
[28] Michael Baldamus, Klaus Schneider, Michael Wenz, and Roberto Ziller.Can American Checkers be solved by means of symbolic model checking? In Howard Bowman, editor, Formal Methods Elsewhere, volume 43 of Electronic Notes in Theoretical Computer Science. Elsevier, 2001.
[29] P.Madhusudan, W.Nam, R. Alur. Symbolic computation techniques for solving games, Working shop on Bounded Model Checking, 2003.
[30] D. Berwanger, Games and logical expressiveness. PhD thesis, RWTH Aachen, 2005.
[31] R.J.Aumann, What is game theory trying to accomplish? in Frontiers of Economics, K. Arrow and S. Honkapohja, eds., Basil Blackwell, 1985.
[32] L.Henkin, Some remarks on infinitely long formulas, in Proceedings of the Symposium on Foundations of Mathematics: Infinitistic Methods, Polish Scientific Publishers, 1961, 167–183.
[33] J.Hintikka, Language-games for quantifiers, in Studies in Logical Theory, N.Rescher, ed., vol. f American Philosophical Quarterly Monograph Series, Basil Blackwell, 1968, 46–72.
[34] A.Ehrenfeucht, An application of games to the completeness problem for formalized theories, Fundamental Mathematics, 1961,49, 129–141.
[35] Dexter Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333–354, December 1983.
[36] C.Stirling. Games for bisimulation and model checking, June 1997. Notes for Mathfit instructional meeting on games and computation, Edinburgh http://www.dcs.ed.ac.uk/home/cps/mathfit.ps.
[37] C.Stirling. Local model checking games. In Proceedings of the 6th International Conference on Concurrency Theory, CONCUR’95, I. Lee and S. A. Smolka, eds, volume 962 of Lecture Notes in Computer Science, Springer, 1995, 1–11.
[38] M. Lange and C.Stirling. Focus games for satisfiability and completeness of temporal logic. In Proceedings of the 16th AnnualIEEE Symposium on Logic in Computer Science, LICS’01. IEEE Computer Society Press, 2001.
[39] Berlekamp, Conway, Guy, Winning Ways. BERLEKAMP, E., CONWAY, J.H., GUY, R.K. Academic Press, London 1982.