Automated analysis of mutual exclusion algorithms using CCS

DOI10.1007/BF01887209MaRDI QIDQ911263zbMATHOpenAlexFDO

Authors 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

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

Recommendations

• Analysing mutual exclusion using process algebra with signals
• scientific article; zbMATH DE number 7317251
• scientific article; zbMATH DE number 1860625
• The mutual exclusion problem
• The mutual exclusion problem. I: A theory of interprocess communication

Cites work

• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 4035115 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 43081 (Why is no real title available?)
• scientific article; zbMATH DE number 4119600 (Why is no real title available?)
• scientific article; zbMATH DE number 4119603 (Why is no real title available?)
• scientific article; zbMATH DE number 4119617 (Why is no real title available?)
• A calculus of communicating systems
• Calculi for synchrony and asynchrony
• Deciding bisimulation equivalences for a class of non-finite-state programs
• Local model checking in the modal mu-calculus
• Modalities for model checking: Branching time logic strikes back
• Results on the propositional \(\mu\)-calculus
• The mutual exclusion problem

Cited in

(24)

• Symbolic bisimulations
• Equivalence checking 40 years after: a review of bisimulation tools
• A monotone framework for CCS
• scientific article; zbMATH DE number 1860625 (Why is no real title available?)
• CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
• Off-the-shelf automated analysis of liveness properties for just paths (extended abstract)
• Exposing latent mutual exclusion by work automata
• Time and Fairness in a Process Algebra with Non-blocking Reading
• Deciding bisimilarity is P-complete
• Efficiency of asynchronous systems, read arcs, and the MUTEX-problem
• Analysing mutual exclusion using process algebra with signals
• Proof systems for message-passing process algebras
• Local model checking in the modal mu-calculus
• A CCS-based investigation of deadlock in a multi-process electronic mail system
• Modelling mutual exclusion in a process algebra with time-outs
• scientific article; zbMATH DE number 7317251 (Why is no real title available?)
• ACTLW -- an action-based computation tree logic with unless operator
• A note on model checking the modal \(\nu\)-calculus
• CCS: it's not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions
• Static Livelock Analysis in CSP
• Liveness of a mutex algorithm in a fair process algebra
• Automatic Mutual Exclusion and Atomicity Checks
• Modal and temporal logics for processes
• Trapping mutual exclusion in the box calculus

Describes a project that uses

Uses Software

• CESAR

This page was built for publication: Automated analysis of mutual exclusion algorithms using CCS

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