On the suitability of trace semantics for modular proofs of communicating processes

DOI10.1016/0304-3975(85)90130-6MaRDI QIDQ1060004zbMATH OpenOpenAlexFDO

Authors Ralph-Johan Back, Heikki Mannila

Publication date 1985

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(85)90130-6

zbMATH Keywords

communicating processesmodular proof systempartial correctness assertionssemantic model

Mathematics Subject Classification ID

Theory of operating systems (68N25)

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.

Cites work

• A calculus of communicating systems
• A calculus of total correctness for communicating processes
• A linear-history semantics for languages for distributed programming
• A Proof System for Communicating Sequential Processes
• A Theory of Communicating Sequential Processes
• An axiomatic basis for computer programming
• Deadlock absence proofs for networks of communicating processes
• scientific article; zbMATH DE number 3808928 (Why is no real title available?)
• scientific article; zbMATH DE number 3808929 (Why is no real title available?)
• scientific article; zbMATH DE number 3817014 (Why is no real title available?)
• scientific article; zbMATH DE number 3926215 (Why is no real title available?)
• scientific article; zbMATH DE number 3469994 (Why is no real title available?)
• scientific article; zbMATH DE number 795666 (Why is no real title available?)
• scientific article; zbMATH DE number 3419181 (Why is no real title available?)
• Processes and the denotational semantics of concurrency

Cited in

(5)

• A fully abstract trace model for dataflow and asynchronous networks
• scientific article; zbMATH DE number 3846840 (Why is no real title available?)
• scientific article; zbMATH DE number 1931943 (Why is no real title available?)
• Revisiting Semantics of Interactions for Trace Validity Analysis
• Towards a complete hierarchy of compositional dataflow models

This page was built for publication: On the suitability of trace semantics for modular proofs of communicating processes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1060004)