Trapping mutual exclusion in the box calculus

DOI10.1016/0304-3975(95)00119-0MaRDI QIDQ672869zbMATH OpenOpenAlexWikidataFDO

Authors Javier Esparza, Glenn Bruns

Publication date 28 February 1997

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

Full work available at URL https://doi.org/10.1016/0304-3975(95)00119-0

zbMATH Keywords

verificationprocess algebrabox calculusmutual exclusion algorithmsPetri net semanticstranslation of parallel programs

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Compositional process semantics of Petri Boxes
• The box algebra = Petri nets + process expressions
• scientific article; zbMATH DE number 1501606
• scientific article; zbMATH DE number 2064221
• Analysing mutual exclusion using process algebra with signals

Cites work

• scientific article; zbMATH DE number 3825182 (Why is no real title available?)
• scientific article; zbMATH DE number 3926231 (Why is no real title available?)
• scientific article; zbMATH DE number 4037225 (Why is no real title available?)
• scientific article; zbMATH DE number 4045165 (Why is no real title available?)
• scientific article; zbMATH DE number 3735115 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 176124 (Why is no real title available?)
• scientific article; zbMATH DE number 193318 (Why is no real title available?)
• scientific article; zbMATH DE number 512822 (Why is no real title available?)
• scientific article; zbMATH DE number 4119603 (Why is no real title available?)
• scientific article; zbMATH DE number 4119615 (Why is no real title available?)
• A distributed operational semantics of CCS based on condition/event systems
• Advances in Petri nets 1992
• Automated analysis of mutual exclusion algorithms using CCS
• Deadlocks and traps in Petri nets as Horn-satisfiability solutions and some related polynomially solvable problems
• Local model checking in the modal mu-calculus
• Structure matrices for Petri nets and their applications

Cited in

(7)

• Model checking LTL using constraint programming
• Mutex needs fairness
• Analysing mutual exclusion using process algebra with signals
• Modelling mutual exclusion in a process algebra with time-outs
• The mutex paradigm of concurrency
• CCS: it's not fair! Fair schedulers cannot be implemented in CCS-like languages even under progress and certain fairness assumptions
• Hume box calculus: Robust system development through software transformation

This page was built for publication: Trapping mutual exclusion in the box calculus

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