1
$\begingroup$

I am reading the PBFT Correctness Proof Paper and I cannot make completely sense of the Invariant 4.7 and its proof: enter image description here

Here are my concerns:

  1. I assume that the symbol $\Leftrightarrow$ is used with the usual meaning of double implication.
  2. $n\mbox{-}faulty$ is defined (Definition 4.3) as the number of faulty replicas, so I do not understand how it can be used as a predicate in Invariant 4.7.
    When is $n\mbox{-}faulty$ true of false?
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.