Verifying concurrent processes using temporal logic
From MaRDI portal
Publication:1159976
zbMath0476.68015MaRDI QIDQ1159976
Publication date: 1982
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Modal logic (including the logic of norms) (03B45) Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Theory of operating systems (68N25)
Related Items
Specification and verification of database dynamics ⋮ Control problems in a temporal logic framework ⋮ Towards a foundation for semantics in complete metric spaces ⋮ Search strategies for resolution in temporal logics ⋮ Removing irrelevant information in temporal resolution proofs ⋮ The sliding-window protocol revisited ⋮ \(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments ⋮ A generalized nexttime operator in temporal logic ⋮ Exposure to deadlock for communicating processes is hard to detect ⋮ Expressibility of output equals input. Negative and positive results