Abstract
Additional axioms and rules are needed for us to go beyond safety properties and be able to reason about properties specified by arbitrary Temporal Logic formulas. These axioms and inference rules of S-Temporal Logic are given in this chapter. We also discuss fairness assumptions for cobegin implementations, because satisfying a liveness property often requires making assumptions that specific processes will have opportunities to execute. Finally, we describe helpful actions and other techniques for proving eventualities.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer Science+Business Media New York
About this chapter
Cite this chapter
Schneider, F.B. (1997). Verifying Arbitrary Temporal Logic Properties. In: On Concurrent Programming. Graduate Texts in Computer Science. Springer, New York, NY. https://doi.org/10.1007/978-1-4612-1830-2_8
Download citation
DOI: https://doi.org/10.1007/978-1-4612-1830-2_8
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4612-7303-5
Online ISBN: 978-1-4612-1830-2
eBook Packages: Springer Book Archive