Intent
Terminate mission miss exactly at time m.
Template
PCTL
$
\mapping(\lit{end}\ \term{miss}\ \lit{exactly\_at}\ \terminal{m} )=
\LTLg^{[0,\terminal{m} )}(\mapping(\term{miss})) \wedge
\LTLg^{[\terminal{m} ,\infty]}(\neg\mapping(\term{miss}))
$
Variations
Examples and Known Uses
each demand needs to be serviced exactly T time units after its generation, by a vehicle present at the demand location [62]
Relationships
See the Pause, Timeout-deadline and Repeat patterns.