Meet- and join-closure of CTL operators

Abstract

The set of all reachable states of a distributed computation forms a lattice under a certain partial order relation. A property is said to exhibit meet-closure if the set of reachable states satisfying it is closed under the lattice meet operation, and join-closure if the set is closed under the lattice join operation. Techniques that apply lattice-theoretic concepts to the verification of distributed computations have largely leveraged the principles of meet- and join-closure of the properties to be verified. It has been shown that exploiting such closure properties allows for the development of verification algorithms that have time and space complexity that is polynomial in the number of events in the computation. Since the number of reachable states in a computation is usually exponential in the number of events, these algorithms significantly alleviate the problem of state space explosion in formal verification.

The temporal logic CTL is popularly used to specify the properties to be verified on a distributed computation. It is thus desirable to study whether various CTL operators preserve the properties of meet- and join-closure. Some CTL operators were previously studied by Sen and Garg [Sen&Garg'03]. In this paper, we extend on their work, and identify additional CTL operators that preserve these closure properties. We also revisit some of the operators which were shown not to preserve meet-closure in [Sen & Garg '03], and identify some conditions under which they  do preserve meet-closure.