@shachaf I think (part of) the source of my confusion is that the definition of a linear time property isn't made for a particular model, it's for all models with a given set of atomic propositions on states. It's not restricting the prefix extensions in the definition of liveness property to correspond to valid transitions for a particular transition system. If you want to constrain the stepwise property changes, you have to do that separately (with safety properties).
=> More informations about this toot | View the thread | More toots from pervognsen@mastodon.social
text/geminiThis content has been proxied by September (ba2dc).