// Maximum probability that the protocol terminates successfully
<<>>Pmax=? [ F t<=K & "terminated_successfully" ]
<<p1>>Pmax=? [ F t<=K & "terminated_successfully" ]
<<p2>>Pmax=? [ F t<=K & "terminated_successfully" ]
<<p1,p2>>Pmax=? [ F t<=K & "terminated_successfully" ]