Bounded PCTL Model Checking of Large Language Model Outputs