[tlaplus] Safety Liveness Decomposition and Machine Closure

[Willy Schultz <will62794@xxxxxxxxx>]

In Alpern and Schneider's paper Defining Liveness they show that any system property P can be expressed as the conjunction of a safety and liveness property. I am wondering whether this decomposition always produces a safety property S and liveness property L such that (S, L) is machine closed. In a later Schneider paper, Decomposing Properties into Safety and Liveness using Predicate Logic, they explicitly define the safety property for the safety-liveness decomposition as S = (P ∪ Mp), where Mp is defined as the set of all behaviors B such that for every behavior b ∈ B, all prefixes of b have an extension that satisfies P.

It would seem that, by construction, the safety property of this decomposition is machine closed with respect to L, since any prefix in the safety property has an extension that satisfies P = S ∧ L, according to the definition of machine closure from Chapter 8 of Specifying Systems. 

If this is the case, does it also mean that we can use this decomposition to transform a non machine closed spec into a machine closed one? For example, if we originally express our system as a conjunction S' ∧ L' such that (S', L') is not machine closed, can we then decompose the property S' ∧ L'  into an alternate safety property S and liveness property L according to Schneider's technique to get a machine closed spec (S, L). 

I believe this may be touched upon already in the related paper Safety and liveness from a methodological point of view [1] but it wasn't entirely clear to me.

[1] https://dl.acm.org/doi/10.1016/0020-0190%2890%2990181-V

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5df28190-1201-4668-992f-fbd8fa902216n%40googlegroups.com.