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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Fri, 18 Nov 2016 22:21:18 -0800 (PST)

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?

Ron

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?

Ron

**Follow-Ups**:**Re: Nondeterminism and equivalence***From:*Leslie Lamport

**Re: [tlaplus] Nondeterminism and equivalence***From:*Stephan Merz

**Re: Nondeterminism and equivalence***From:*Ioannis Filippidis

- Prev by Date:
**Re: TLA+ Video Course** - Next by Date:
**Re: Nondeterminism and equivalence** - Previous by thread:
**Re: [tlaplus] Eventual action** - Next by thread:
**Re: Nondeterminism and equivalence** - Index(es):