Eliminating disjunctions of leads-to properties

DOI10.1016/0020-0190(94)90010-8zbMath0802.68081OpenAlexW1964726517MaRDI QIDQ1318740

Ken Calvert

Publication date: 5 April 1994

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0020-0190(94)90010-8

zbMATH Keywords

formal semanticsspecification languagestemporal logicconcurrencyUNITYformal specificationspredicate transformer

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• UNITY

Cites Work

• Unnamed Item
• A simple proof of a completeness result for \(leads\)-\(to\) in the UNITY logic
• Specifying Concurrent Program Modules

This page was built for publication: Eliminating disjunctions of leads-to properties