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

DOI10.1016/j.tcs.2015.11.032zbMath1335.68042OpenAlexW2186142421MaRDI QIDQ5964014

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

expressive completenessatomic registersfinite-state concurrent programsstate-explosion

Mathematics Subject Classification ID

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

Related Items (2)

Synthesis of large dynamic concurrent programs from dynamic specifications ⋮ Finite-state concurrent programs can be expressed succinctly in triple normal form

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Synthesis of large dynamic concurrent programs from dynamic specifications
• Using branching time temporal logic to synthesize synchronization skeletons
• On interprocess communication. I: Basic formalism
• Optimality of wait-free atomic multiwriter variables
• Eventually-serializable data services
• Simple extensions of 1-writer atomic variable constructions to multiwriter ones
• The elusive atomic register
• Bounded Concurrent Time-Stamping
• How to share concurrent wait-free variables
• Optimal multi-writer multi-reader atomic register
• Software transactional memory
• Verification, Model Checking, and Abstract Interpretation

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