Two normal form theorems for CSP programs
type: Item
instance of: scholarly article
title: Two normal form theorems for CSP programs
zbMATH Open document ID: 0631.68026
DOI: 10.1016/0020-0190(87)90001-9
author: Luc Bougé
author: Ph. Clermont
author: Krzysztof R. Apt
published in: Information Processing Letters
publication date: 1987-01-01T00:00:00Z
full work available at URL: https://ir.cwi.nl/pub/10291
review text: We define two normal forms for CSP programs. In the first normal form, each process contains only one I/O repetitive command and all its I/O commands appear as guards of this command. In the second normal form, all guards of this I/O repetitive command are I/O guards. We describe an inductive method that transforms any CSP program into an equivalent program in first or second normal form. The notion of equivalence is discussed. It is shown that no transformation into second normal form can preserve deadlock freedom.
Mathematics Subject Classification ID: 68N25
zbMATH DE Number: 4026812
zbMATH Keywords: partially interpreted computation
zbMATH Keywords: syntactic equivalence
zbMATH Keywords: deadlock freedom
describes a project that uses: CESAR
MaRDI profile type: Publication
OpenAlex ID: W1976295241
cites work: Correctness proofs of distributed termination algorithms
cites work: Q3681912
cites work: Distributed Termination
cites work: Q3929024
cites work: Closed Covers: To Verify Progress for Communicating Finite State Machines
cites work: On folk theorems
cites work: Communicating sequential processes
cites work: Some Properties of Predicate Transformers
cites work: Q3657409
cites work: Q3940830
cites work: Normalform-Transformationen für CSP-Programme. (Normal form transformations for CSP-programs)
description: scientific article; zbMATH DE number 4026812