Intent
Execute miss. Stop the the execution when the timeout m is reached.
Template
PCTL
$
\mapping(\lit{timeout-deadline}\ \terminal{m} \ \term{miss})=
\LTLg^{[\terminal{m} ,\infty]}(\neg\mapping(\term{miss}))
$
Variations
Examples and Known Uses
each robot is given the same time budget to collect samples and return home [65]
Relationships
See the Pause, End and Repeat patterns.