A Logic for Concurrent Programming: Safety
Jayadev Misra · 2003
The UNITY-logic is a fragment of linear temporal logic. It was designed to specify safety and and progress properties of reactive systems. Experience gained in applying this logic in practice has led us to modify some of its operators. In particular, we had adopted unless as the primary operator for expressing safety properties for many years. We suggest a new operator, co, to take its place. Our experience suggests that the simplicity of formal manipulations is at least as important as the expressive power of an operator. Theoretically, unless and co are equally expressive, while the latter has more pleasing derived rules that allow simpler manipulations. This research is presented in two papers. We study safety properties in the first paper and progress properties in the second paper. We use a small amount of theory to introduce the co operator. The major portion of the paper is devoted to applying the theory in practice: showing how various safety properties can be expressed and manipulated using co.