Technical reports
A complete proof system for SCCS with model assertions
September 1985, 23 pages
DOI: 10.48456/tr-78
Abstract
This paper presents a proof system for Robin Milner’s Synchronous Calculus of Communicating Systems (SCCS) with modal assertions. The language of assertions is a fragment of dynamic logic, sometimes called Hennessy-Milner logic after they brought it to attention; while rather weak from a practical point of view, its assertions are expressive enough to characterise observation equivalence, central to the work of Milner et al. on CCS and SCCS. The paper includes a completeness result and a proof of equivalence between an operational and denotational semantics for SCCS. Its emphasis is on the theoretical issues involved in the construction of proof systems for parallel programming langauges.
Full text
PDF (1.0 MB)
BibTeX record
@TechReport{UCAM-CL-TR-78, author = {Winskel, Glynn}, title = {{A complete proof system for SCCS with model assertions}}, year = 1985, month = sep, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-78.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-78}, number = {UCAM-CL-TR-78} }