pctl is really an extension of ctl but in the case where the syntax is not split into state formulas and path formulas. Otherwise, it's not straightforward or obvious to see if we can get A Phi alone. Although PCTL is an exntesion of CTL, the A (all) cannot be obtained using P >= 1 [.] alone

adding information on state-value functions in MRP and MDPs, optimal policy, worst policy. Also renamed a few things such as the Property Verification section becoming Results section