Model Checking : Safety and Liveness properties

Question

I know what Safety and Liveness properties are and the relation between Safety and Badprefixes of an LT property. I wanted to understand about the closure properties and why the closure of a safety property is the property itself. The image is for reference. Can someone explain me the concepts that can be used that will enable me to answer the questions, it would be really helpful.

Answer 1

We are considering languages of infinite traces.

As you hinted, a language L is defined to be a safety property if for every trace not in L, there exists a bad prefix, that is, a finite prefix such all infinite continuations of the prefix are not in L. So intuitively, a safety property is about some bad event not happening.

For a given language L, the language closure(L) is defined to consist of all traces where every finite prefix is also prefix of a trace in L.

The standard example for taking the closure would be for L = a*b^omega = { bbb..., abbb..., aabbb..., aaabbb... }. The language L contains all traces with a finite prefix of a's and then infinitely many b's. Then closure(L) = a*b^omega + a^omega = L U {aaa...}. The trace of infinitely many a's is not contained in L, but every finite prefix of a^omega is also prefix of a trace in L. Therefore a^omega is contained in the closure of L.

Now your question is why for a safety property L, it holds that L = closure(L).

Let L be a safety property. We have to show that every trace in L is contained in closure(L) and vice versa that every trace in closure(L) is contained in L.

1. Every trace in L is contained in closure(L): Consider a trace sigma in L. Then every finite prefix of sigma is a prefix of sigma. Therefore every finite prefix of sigma is the prefix of a trace in L. By definition of closure(L), it follows that sigma is in closure(L).

2. Every trace in closure(L) is contained in L: Let sigma be in closure(L). Assume sigma is not in L. By definition of safety properties, sigma has a finite prefix w, such that no infinite continuation of w is in L. But then w cannot be a prefix of a word in L. But by definition of closure(L), every finite prefix of sigma has to be in L. Contradiction. Since the assumption that sigma is not in L leads to a contradiction, it follows that sigma is in L.

Sidenote A: Note that for 1. we didn't use that L is a safety property. The property that L is a subset of closure(L) holds in general, not just for safety properties.

Sidenote B: In the example for the closure we noted that for L = a*b^omega, we have closure(L) = a*b^omega + a^omega. Therefore L is unequal to closure(L), so L cannot be a safety property. We can see this from the trace a^omega, which is not in L, but does not have a bad prefix, as every finite prefix of a^omega is of the form a* and can be continued to a trace of the form a*b^omega in L.

Sidenote C: We could also ask the reverse question, when L = closure(L), is L a safety property? The answer is yes. Let L be a language with L = closure(L). Consider a trace sigma that is not in L. We have to show that sigma has a bad prefix. By L = closure(L), we have sigma is not in closure(L). By definition of closure(L), if all finite prefixes of sigma are in L, we would have sigma in closure(L). Thus, from sigma not in closure(L), it follows that there is some finite prefix w of sigma, such that all traces sigma' in L do not have w as a prefix. In other words, every infinite continuation of w cannot be a trace in L. Therefore w is a bad prefix. In conclusion, every trace sigma that is not in L has a bad prefix thus L is a safety property.

Sidenote D: From your original question and Sidenote C we can conclude that L is a safety property if and only if L = closure(L). This improves our understanding of what is means to take the closure of L: Adding all traces that do not have a bad prefix. Further, you could verify that taking the closure of the closure does not add any new traces, so for any L, it holds that closure(L) = closure(closure(L)). Therefore for any L, it holds that closure(L) is a safety property.

Sidenote E: To answer your comment question for an example of a language that is equal to its closure: Based on Sidenote D, we could take any safety property: Consider the language L over the alphabet {a,b,c} that is L = { sigma in {a,b,c}^omega | sigma has no c }. So the bad prefixes would be all finite words that have a c (if you think of the trace as modelling the execution of some program, maybe c could mean "the program has a crash" and does random things after that). We can verify that L = closure(L): We already know that L subset closure(L), based on 1. above. For the other direction, consider a trace sigma in closure(L). By definition of closure(L), every finite prefix w of sigma has to be a prefix of a trace sigma' in L. Since by definition of L, sigma' cannot contain a c, it follows that w cannot contain a c. When every finite prefix w of sigma cannot contain c, it follows that sigma cannot contain c. Therefore sigma is in L. We conclude L = closure(L).