A PVS Theory of Symbolic Transition Systems

Citation

Maharaj S (2001) A PVS Theory of Symbolic Transition Systems. In: Boulton R & Jackson P (eds.) Theorem Proving in Higher Order Logics, 2001, Supplemental Proceedings. Theorem Proving in Higher Order Logics: 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, 03.09.2001-06.09.2001. Edinburgh, Scotland: Division of Informatics, University of Edinburgh, pp. 255-266. http://www.inf.ed.ac.uk/publications/online/0046/

Abstract
This paper describes some work carried out in the context of a project aimed at developing tools for reasoning about the formal description technique Full LOTOS. One of the tasks within this project was the development of a theory of symbolic transition systems for Full LOTOS, and of a corresponding modal logic. This task was carried out with the help of the PVS theorem prover, which served as a convenient vehicle for experimenting with alternative definitions of the concepts being developed. The proof of correctness of the modal logic was also partially carried out within PVS. Our main conclusion is that the discipline imposed by use of the fully formal PVS notation provided valuable help with the detection and correction of errors and omissions in our experimental definitions, thereby making it easier to arrive at a correct set of definitions.