The present Thesis addresses the problem of specification and verification of communicating systems with value passing. We assume that such systems are described
in the well-known Calculus of Communicating Systems, or rather, in its value passing
version. As a specification language we propose an extension of the Modal μ-Calculus,
a poly-modal first-order logic with recursion. For this logic we develop a proof system
for verifying judgements of the form b ⊢ Ε : Φ where E is a sequential CCS term
and b is a Boolean assumption about the value variables occurring free in E and Φ.
Proofs conducted in this proof system follow the structure of the process term
and the formula. This syntactic approach makes proofs easier to comprehend and
machine assist. To avoid the introduction of global proof rules we adopt a technique
of tagging fixpoint formulae with all relevant information needed for the discharge
of reoccurring sequents. We provide such tagged formulae with a suitable semantics.
The resulting proof system is shown to be sound in general and complete (relative
to external reasoning about values) for a large class of sequential processes and logic
formulae. We explore the idea of using tags to three different settings: value passing,
extended sequents. and negative tagging. / Graduate
| Identifer | oai:union.ndltd.org:uvic.ca/oai:dspace.library.uvic.ca:1828/8287 |
| Date | 16 June 2017 |
| Creators | Gurov, Dilian Borissov |
| Contributors | Kapron, Bruce M., Müller, Hausi A. |
| Source Sets | University of Victoria |
| Language | English, English |
| Detected Language | English |
| Type | Thesis |
| Rights | Available to the World Wide Web |
Page generated in 0.0029 seconds