[dan-robertson]

I wonder to what extent this is a problem from the global timesteps of LTL. They seem to require global transformations to work around and the result of the transformations seems to be harder to reason about. I wonder if some alternative logic would work better (eg one where time is more continuous and so there is no such thing as the X operator, or maybe one where time is partially ordered in some way but I’m not sure what that would look like).

I don’t really know how to talk about the problem of the shared variable coupling the two processes too tightly. It seems like the logic is too relaxed in allowing any variable to change at any time forcing specifications to lock down variables and therefore be too brittle to connect.