On the suitability of trace semantics for modular proofs of communicating processes
type: Item
instance of: scholarly article
title: On the suitability of trace semantics for modular proofs of communicating processes
zbMATH Open document ID: 0567.68018
DOI: 10.1016/0304-3975(85)90130-6
published in: Theoretical Computer Science
publication date: 1985-01-01T00:00:00Z
review text: The question of whether a semantic model is suitable for the construction of a modular proof system is studied in detail. The notion of one semantic model being a (full) abstraction of another semantic model with respect to a given class of properties is introduced, and is used in analyzing different semantic models for communicating processes. A trace model for communicating processes is described and shown to be suitable for the construction of a modular proof system in which partial correctness assertions about communicating processes can be expressed.
Mathematics Subject Classification ID: 68N25
zbMATH DE Number: 3905837
zbMATH Keywords: modular proof system
zbMATH Keywords: semantic model
zbMATH Keywords: partial correctness assertions
zbMATH Keywords: communicating processes
author: Ralph-Johan Back
author: Heikki Mannila
MaRDI profile type: Publication
full work available at URL: 0304-3975(85)90130-6
OpenAlex ID: W2009408666
cites work: A Proof System for Communicating Sequential Processes
cites work: Processes and the denotational semantics of concurrency
cites work: Q3657410
cites work: A linear-history semantics for languages for distributed programming
cites work: Q4845486
cites work: A calculus of total correctness for communicating processes
cites work: An axiomatic basis for computer programming
cites work: A Theory of Communicating Sequential Processes
cites work: Q4054644
cites work: Q5682023
cites work: A calculus of communicating systems
cites work: Deadlock absence proofs for networks of communicating processes
cites work: Q3700806
cites work: Q3657409
cites work: Q3664405
description: scientific article; zbMATH DE number 3905837