Re: [tlaplus] Modelling "eventually, with probability 1"

[Igor Konnov <igor.konnov@xxxxxxxxx>]

Hi Karolis,

I agree, your reasoning looks circular to me. Basically, the theorem states that <>[]done should hold by assuming <>done in Live.

However, it’s a nice idea to reduce a probabilistic argument to a non-probabilistic one. We did something similar for the Ben-Or’s algorithm in the paper that is not related to TLA+. However, the reduction argument required a hand-written proof to reason about adversaries and limits, see Section 7 in [1]. I am not sure about how much of it could be mechanized.

[1]: https://drops.dagstuhl.de/opus/volltexte/2019/10935/


Best regards,
Igor

> On 04.05.2021, at 23:28, Karolis Petrauskas <k.petrauskas@xxxxxxxxx> wrote:
> 
> I'm trying to model a consensus algorithm, in which a common coin (a distributed random number) is used to overcome the FLP impossibility.
> An example of such an algorithm is presented in https://eprint.iacr.org/2016/199.pdf, Figure 11.
> 
> The termination of the algorithm is based on the fact that by repeating the coin flips we will get the needed value eventually (because of the uniform randomness, as I understand).
> The below spec does not model the entire algorithm, just the part with the common coin.
> 
> Does it look reasonable to model that "eventual" with <>done as a fairness assumption?
> I'm not sure. It sounds a bit like assuming the conclusion, but on the other hand I'm not trying to prove that probabilistic property, just use it.
> In this example Decides looks similar to Live, but in the final spec the Decides property would be different.
> 
> ------------- MODULE CommonCoinConverges --------------
> EXTENDS TLAPS
> VARIABLE val
> VARIABLE done
> vars == <<val, done>>
> Round == /\ ~done
>          /\ \E newCoin \in BOOLEAN :     \* Take a new random number.
>               /\ done' = (newCoin = val) \* Check, if the value is lucky.
>               /\ val'  = newCoin 
> Terminated == done /\ UNCHANGED vars \* Just to avoid a deadlock in a proof bellow.
> Init == /\ val \in BOOLEAN
>         /\ done = FALSE 
> Next == Round \/ Terminated
> Live == <>done
> Spec == Init /\ [][Next]_vars /\ Live
> ---------------------------------------------------------
> TypeOK == /\ val  \in BOOLEAN
>           /\ done \in BOOLEAN
> Decides == <>[]done
> THEOREM Spec => []TypeOK /\ Decides
> =========================================================
> 
> 
> As a side note, I managed to prove the above theorem in TLAPS from the updated_enabled_cdot branch by looking
> at https://github.com/tlaplus/tlapm/blob/updated_enabled_cdot/examples-draft/SimpleExampleWF.tla.
> Although I'm still not sure if I would be able to do that again :) The proof tactics for temporal operators are not clear to me.
> Maybe there is a paper or a book on such tactics that I should read before trying to prove something like this? :)
> 
> THEOREM Spec => []TypeOK /\ Decides
>   <1>1. Spec => []TypeOK
>         <2>1. Init => TypeOK BY DEF Init, TypeOK
>         <2>2. TypeOK /\ [Next]_vars => TypeOK'
>               <3> SUFFICES ASSUME TypeOK, Next PROVE TypeOK' BY DEF vars, TypeOK
>               <3> CASE Round BY DEF Round, TypeOK
>               <3> CASE Terminated BY DEF Terminated, TypeOK, vars
>               <3>q. QED BY DEF TypeOK, Next, Round, Terminated
>         <2>q. QED BY <2>1, <2>2, PTL DEF Spec
>   <1>2. Spec => Decides
>         <2>x. TypeOK /\ Spec => [] (~done \/ []done)
>               <3>1. ASSUME TypeOK /\ [Next]_vars PROVE ~done \/ done'
>                     <4> SUFFICES ASSUME TypeOK, Next PROVE ~done \/ (done') BY <3>1 DEF vars
>                     <4> CASE Round BY DEF Round
>                     <4> CASE Terminated BY DEF Terminated, vars
>                     <4> QED BY DEF Next
>               <3>q. QED BY <3>1, <1>1, PTL DEF Spec
>         <2>q. QED BY <1>1, <2>x, PTL DEF Spec, Live, Decides
>   <1>q. QED BY <1>1, <1>2
> 
> Sincerely,
> Karolis Petrauskas
> 
> -- 
> 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/CAFteovKBZYaJtoRsYKPG7rsQOVqNxu3d%3Dp5n4bfigxvSqS0o%3DQ%40mail.gmail.com.

-- 
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/E25C481E-0232-4281-AF35-4D0DE8748165%40gmail.com.