A semi-Markov decision process (SMDP) is a continuous-time dynamic system [1]}, [2]}, [3]} modeled by a tuple \(\mathcal {SM} = (S, A, T, D, s^I, AP, L)\) , where \(S\)  is the finite set of sates, \(A\)  is the finite set of actions, \(T : S \times S \times A \rightarrow [0,1]\)  is the state transition probability, \(D : S \times A \times S \rightarrow \mathcal {D}(\mathbb {R}_{\ge 0})\)  is the dwell time probability function, \(s^I \in S\)  is the initial state, \(AP\)  is the finite set of atomic propositions, and \(L : S \rightarrow 2^{AP}\)  is the labeling function [4]}. Let \(A(s) = \lbrace  a \in A \;|\; \exists s^{\prime } \in S \mbox{ s.t. } T(s^{\prime } \;|\; s,a) > 0 \rbrace \) . Note that \(\sum _{s^{\prime } \in S}T(s^{\prime } \;|\; s,a) = 1\)  for any \(s \in S\)  and any \(a \in A(s)\) . We sometimes denote \(D(\cdot \;|\; s,a,s^{\prime })\)  instead of \(D(s,a,s^{\prime })(\cdot )\)  for any \((s,a,s^{\prime }) \in S \times A \times S\) .
