Finite-state concurrent programs can be expressed in pairwise normal form

DOI10.1016/J.TCS.2015.11.032MaRDI QIDQ5964014zbMATH OpenOpenAlexFDO

Authors Paul C. Attie

Publication date 26 February 2016

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

Full work available at URL https://doi.org/10.1016/j.tcs.2015.11.032

zbMATH Keywords

atomic registersexpressive completenessfinite-state concurrent programsstate-explosion

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Finite-state concurrent programs can be expressed succinctly in triple normal form
• Two normal form theorems for CSP programs
• scientific article; zbMATH DE number 3892585
• On transformations of concurrent-object programs
• Normalform-Transformationen für CSP-Programme. (Normal form transformations for CSP-programs)

Cites work

• Bounded Concurrent Time-Stamping
• Eventually-serializable data services
• How to share concurrent wait-free variables
• scientific article; zbMATH DE number 996442 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 4110131 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1361120 (Why is no real title available?)
• scientific article; zbMATH DE number 1142326 (Why is no real title available?)
• On interprocess communication. I: Basic formalism
• Optimal multi-writer multi-reader atomic register
• Optimality of wait-free atomic multiwriter variables
• Simple extensions of 1-writer atomic variable constructions to multiwriter ones
• Software transactional memory
• Synthesis of large dynamic concurrent programs from dynamic specifications
• The elusive atomic register
• Using branching time temporal logic to synthesize synchronization skeletons
• Verification, Model Checking, and Abstract Interpretation

Cited in

(3)

• Two normal form theorems for CSP programs
• Synthesis of large dynamic concurrent programs from dynamic specifications
• Finite-state concurrent programs can be expressed succinctly in triple normal form

This page was built for publication: Finite-state concurrent programs can be expressed in pairwise normal form

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