Automated analysis of mutual exclusion algorithms using CCS

DOI10.1007/BF01887209zbMath0696.68039MaRDI QIDQ911263

Daniel J. Walker

Publication date: 1989

Published in: Formal Aspects of Computing (Search for Journal in Brave)

zbMATH Keywords

mutual exclusion algorithms; concurrency workbench; Calculus of Communicating Systems

Mathematics Subject Classification ID

68N25: Theory of operating systems

68W99: Algorithms in computer science

Related Items

Trapping mutual exclusion in the box calculus, Symbolic bisimulations, Liveness of a mutex algorithm in a fair process algebra, A note on model checking the modal \(\nu\)-calculus, Local model checking in the modal mu-calculus, Deciding bisimilarity is P-complete, CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus, Efficiency of asynchronous systems, read arcs, and the MUTEX-problem, Proof systems for message-passing process algebras, CCS: it's not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions, ACTLW -- an action-based computation tree logic with unless operator, Time and Fairness in a Process Algebra with Non-blocking Reading

Uses Software

• CESAR

Cites Work

• Results on the propositional \(\mu\)-calculus
• Calculi for synchrony and asynchrony
• A calculus of communicating systems
• Local model checking in the modal mu-calculus
• Deciding bisimulation equivalences for a class of non-finite-state programs
• Modalities for model checking: Branching time logic strikes back
• The mutual exclusion problem
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item