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?

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.