const int k; // number of tokens const int K; // number of steps // labels label "k_tokens" = num_tokens=k; // configurations with k tokens // From any configuration, a stable configuration is reached with probability 1 filter(forall, "init" => P>=1 [ F "stable" ]) // Maximum expected time to reach a stable configuration (for all configurations) R=? [ F "stable" {"init"}{max} ] // Maximum/minimum expected time to reach a stable configuration (for all k-token configurations) R=? [ F "stable" {"k_tokens"}{max} ] R=? [ F "stable" {"k_tokens"}{min} ]