Automated analysis of mutual exclusion algorithms using CCS

DOI10.1007/BF01887209zbMath0696.68039OpenAlexW2063510765MaRDI QIDQ911263

Daniel J. Walker

Publication date: 1989

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

Full work available at URL: https://doi.org/10.1007/bf01887209

zbMATH Keywords

mutual exclusion algorithmsconcurrency workbenchCalculus of Communicating Systems

Mathematics Subject Classification ID

Theory of operating systems (68N25) Algorithms in computer science (68W99)

Related Items

CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus ⋮ Modelling mutual exclusion in a process algebra with time-outs ⋮ Equivalence checking 40 years after: a review of bisimulation tools ⋮ Unnamed Item ⋮ A note on model checking the modal \(\nu\)-calculus ⋮ Local model checking in the modal mu-calculus ⋮ Trapping mutual exclusion in the box calculus ⋮ Symbolic bisimulations ⋮ ACTLW -- an action-based computation tree logic with unless operator ⋮ Deciding bisimilarity is P-complete ⋮ Time and Fairness in a Process Algebra with Non-blocking Reading ⋮ Liveness of a mutex algorithm in a fair process algebra ⋮ 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 ⋮ Efficiency of asynchronous systems, read arcs, and the MUTEX-problem

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