# Petri Net Toolbox for Multi-Robot Planning under Uncertainty
## 3 Materials and Methods
### Policy Synthesis  
The _policy synthesis module_ provides algorithms to synthesize optimal policies that optimize team-level objectives. The diagram in Figure 5 shows the implementation of the policy synthesis method. This method takes as input the GSPNR model \(G^{\prime}\) built with the _design module_ and outputs the optimal policy \(\pi^{*}_{G^{\prime}}\). The optimal policy is defined as \(\pi^{*}_{G^{\prime}}:R(G)\to T_{I}\cup\{\bot,\top\}\). The \(\bot\) action represents all uncontrollable timed actions that in \(G^{\prime}\) are viewed as timed transitions. The \(\top\) action represents transitions with an uncertain outcome and selecting it means triggering the formed random switch. In the \(G^{\prime}\), these are viewed as uncontrollable immediate transitions. The policy \(\pi^{*}_{G^{\prime}}\) defines for each marking what is the optimal action to select. In a nutshell, the algorithm converts \(G^{\prime}\) into an equivalent MDP \(M_{G^{\prime}}\) and then applies value iteration. The obtained policy \(\pi^{*}_{M_{G^{\prime}}}\) is then mapped from the MDP states to the GSPNR markings, yielding the policy \(\pi^{*}_{G^{\prime}}\)[20]. The policy synthesis algorithm optimizes team-level objectives that are influenced by the defined reward functions and by the performance objective selected. This module implements two performance objectives: the total expected reward objective, defined as:  
\[I_{total}(\pi)=\mathbb{E}_{s\sim\rho,a\sim\pi}[r(s,a)] \tag{1}\]  
and the discounted expected reward given by:  
\[J_{discount}(\pi)=\mathbb{E}_{s\sim\rho,a\sim\pi}[\gamma^{t-1}r(s,a)], \tag{2}\]  
where \(\pi\) denotes the control policy, \(\rho\) the state distribution, \(r\) the reward function, \(t\) the time step and \(\gamma\) the discount factor. The \(I_{total}(\pi)\) objective takes into account the total reward value accumulated, however it is restricted to scenarios with finite horizons. The \(J_{discount}(\pi)\) converges even in infinite horizon scenarios, since it discounts future rewards, giving more weight to the rewards received in the initial markings. In order to find the optimal policy that optimizes such objectives the GSPNR model is converted to an equivalent MDP. Let \(G^{\prime}=\langle P,T,W^{+},W^{-},F,m_{0},r_{P},r_{T}\rangle\) be a GSPNR. Let \(E^{max}_{G^{\prime}}=max(\{Ex_{G^{\prime}}(m)\mid\text{ for all }m\in R_{T}(G^{\prime})\})\) be the maximum rate among all tangible markings and \(\eta>E^{max}_{G^{\prime}}\) be a normalization constant. The equivalent MDP obtained from \(G^{\prime}\) is defined as \(M_{G^{\prime}}=\langle S,s_{0},A,P,r\rangle\), where: \(S=R(G^{\prime})\), that is, the state space is comprised by all the reachable markings of \(G^{\prime}\); \(s_{0}=m_{0}\), that is, the initial state \(s_{0}\in S\) corresponds to the initial marking in \(G^{\prime}\); \(A=T^{c}_{I}\cup\{\bot,\top\}\), that is, the set of actions includes all controllable immediate transitions, plus the action \(\bot\) and the random switch \(\top\); the transition probability \(P:S\times A\times S\rightarrow[0,1]\) is given by:  
Figure 5: Diagram summarizing the policy synthesis algorithm. \[P(s,\alpha,s^{\prime})= \begin{cases}\frac{Fr(s,s^{\prime})}{\eta}&\text{for}\;s \in R_{T}(G^{\prime}),\,\alpha=\bot\text{ and }s^{\prime}\
eq s\\ 1-\frac{\operatorname{Er}(s)-Fr(s,s^{\prime})}{\eta}&\text{for}\;s\in R_{T}(G^ {\prime}),\,\alpha=\bot\text{ and }s^{\prime}=s\\ 1&\text{for}\;s\in R_{V}(G^{\prime}),\,\alpha\in A\setminus\{\bot,\top\}\text { and }s[t]s^{\prime}\\ \frac{F(t)}{\sum_{k\in A(k)}F(t_{k})}&\text{for}\;s\in R_{V}(G^{\prime}),\, \alpha=\top\text{ and }s[t_{i}]s^{\prime}.\end{cases} \]  
The reward function \(r:S\times A\to\mathbb{R}_{\geq 0}\) is defined as:  
\[r(s,\alpha)= \begin{cases}\sum_{p_{i}\in\mathbb{P}_{\geq 1}}\frac{r_{p}(p_{i})}{ \eta}&\text{if}\;s\in R_{T}(G^{\prime})\text{ and }\alpha=\bot\\ r_{T}(t)&\text{otherwise, with }t=\alpha\text{ and }\alpha\in A\setminus\{\bot\}, \end{cases}