[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Nondeterminism and equivalence

Hi Ron,

your claim that all of the three specifications admit the same single behavior is true only because you ignore stuttering. The TLA+ specification

x ∈ Nat ∧ t = 1 ∧ ☐[t’ = t + 1 ∧ x’ = x + 1 ∧ t = 100 ⇒ x = 100]_<<x,t>>

has behaviors where x initially holds an arbitrary natural number, and t and x get incremented until t hits 100, at which point only stuttering is possible. So it cannot be equivalent to the TLA+ specification

    x = 1 ∧ t = 1 ∧ ☐[t’ = t + 1 ∧ x’ = x + 1]_<<t,x>>

A similar observation holds for (the TLA+ version of) the third specification

    x = 1 ∧ t = 1 ∧ ☐[t’ = t + 1 ∧ ((t < 100 ∧ x’ = x - 1) ∨ x’ = x + 1) ∧ (t = 100 ⇒ x = 100)]_<<x,t>>

You can force the equivalence of the specifications by adding the conjunct

    ⬦(t > 100)

and this observation shows that liveness conditions may sometimes constrain the safety part of the specifications. Such specifications are known as "not machine-closed" [1], and are hard to reason about. (You'd have to prove the invariant ☐(x=t), but this requires temporal logic reasoning since you must appeal to the liveness condition to show that the execution would be blocked when t hits 100.)

The standard form of TLA+ specifications where liveness conditions are conjunctions of (weak or strong) fairness conditions on sub-actions of the specification (essentially, disjuncts of the next-state relation) ensures that specifications are machine closed, and all safety properties can be proved just from the initial condition and the next-state relation.

Best regards,

[1] M. Abadi, L. Lamport. The existence of refinement mappings. TCS 81(2), 1991. See also section 8.9.2 of Specifying Systems.

On 19 Nov 2016, at 07:21, Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx> wrote:

My question concerns the more theoretical aspects of TLA.

Consider the following three specifications, assuming we have `VARIABLES t, x` (for simplicity of notation, I’ll drop the stuttering invariant actions):

    x = 1 ∧ t = 1 ∧ ☐(t’ = t + 1 ∧ x’ = x + 1)

    x ∈ Nat ∧ t = 1 ∧ ☐(t’ = t + 1 ∧ x’ = x + 1 ∧ t = 100 ⇒ x = 100)

    x = 1 ∧ t = 1 ∧ ☐(t’ = t + 1 ∧ ((t < 100 ∧ x’ = x - 1) ∨ x’ = x + 1) ∧ t = 100 ⇒ x = 100)

Each of these specifications admits exactly the same set of behaviors (which happens to contain just a single one). By taking the formulas apart we can see that the second is different from the first by looking at the initial condition, and we can see that the third is different from the first by examining their next-state relations. But can we tell them apart without breaking the formulas open (perhaps by conjuncting them with another formula)? Are they equivalent?

If they are, are the algorithms they describe “really” equivalent? Obviously, for the sake of abstraction-refinement relations, it makes sense to ignore internal nondeterminism, but on the other hand, we know that an algorithm that employs nondeterminism can have significantly different complexity than one that does not, so shouldn’t there be a way to tell them apart?


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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.