## 4 Discussion  
In this paper, we presented an algorithm to verify multi-agent system models based on tracking bigraphical reactive systems. Our algorithm can detect incorrectness of a model and unfulfillment of non-functional requirements. The algorithm considers a model to be incorrect if activities planned to be executed in parallel are not independent of each other. In this article, we presented two examples of utilizing the algorithm to check if a behavior policy meets non-functional requirements regarding time and safety of task execution. We also demonstrated how to generate successive states of a scenario, which is a task realization using a selected behavior policy, based on the the behavior policy. Finally, we discussed memory complexity of operations essential to behavior policies generation and proposed a few ways to reduce it. One of the suggested methods is to limit results to a certain number of the best ones. We gave an example of an evaluation function that allows ranking partial results (in our case, these are behavior policies that when executed do not meet functional requirements). The evaluation function is applicable to tasks of any kind and size. \begin{table}
\begin{tabular}{c c c c} \hline \hline
**Strategy** & **MNoR** & **Pros** & **Cons** \\ \hline All first found & Unlimited & Perfect for assuring correctness of the model as this strategy gives all existing walks to the desired destination state. & Unfeasible for anything but small systems due to large memory consumption. \\ First N found & N & The fastest of all strategies since it does not sort results and can shrink an output of convolution operation. Perfect when the quality of a result is not important or when all results are expected to have similar quality. & Does not care about quality of returned results at all. \\ First N best found & N & With a good evaluation function this strategy can return the best results. Perfect when model has already been validated and the developer is looking for a behavior policy of a certain quality. & Only for tiny systems. This is the most memory consuming strategy because it not only returns all found results but the search is continued until results have specified length. & Does not care about the quality of returned results at all. \\ First N up to a certain length & \(N\times L\) & Allow for insight into how the length of a result impacts the way a mission is executed. Very fast as it is an extension of _first N found_. & It is slower than _first N found up to a certain length_ strategy due to sorting of results. \\ Best N up to a certain length & \(N\times L\) & It gives good insight how the quality of results varies with the length of a walk. Perfect when the developer is looking for a behavior policy that he or she has no expectations about. & It is slower than _first N found up to a certain length_ strategy due to sorting of results. \\ \hline \hline \end{tabular}
\end{table} 
Table 22: Summary of the proposed strategies for finding walks in a state space. The second column denoted as MNoR stands for Maximum Number of Results. The value of \(N\) is equal to a number of results of the same length. The value of \(L\) is equal to the maximum length of a result. This work complements our previous publication, which focused solely on designing multi-agent systems with tracking bigraphs. The methodology enables the design of a broad range of systems from warehouse robots to drone swarms performing a task without human intervention. One can also consider designing software systems where programs act as agents and operations performed by these programs could represent transition functions. The functional programming paradigm intuitively fits this kind of design. The main drawback of our methodology is the lack of adaptability of behavior policies. This means there can be no deviation from scheduled actions when executing a behavior policy. It also means that agents in a modeled system have to be fully controllable in the real world.