A master thesis from Aalborg University
Operational and Denotational Properties of a Modal Process Logic
Author(s)
Term
4. term
Education
Publication year
2012
Submitted on
2012-02-14
Abstract
This report develops the theory of a modal process logic first introduced by Kim Larsen and Bent Thomsen. The logic can be seen as an extension of CCS and has an operational semantics upon which a preorder on formulae in the logic is defined. A denotational description originally put forward by Kim Larsen and Bent Thomsen is examined, and it is shown to what extent the refinement ordering explains the ordering introduced by this kind of semantic description. In particular it is shown how the modal process logic semantically subsumes the language of partial specifications also introduced by Kim Larsen and Bent Thomsen. The static constructs of CCS are added to the logic, and a new `observational'' preorder is introduced and used on three examples. Finally, sound and complete proof systems are given for the strong refinement ordering and the equality defined by the denotational semantics.
Documents
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.