The purpose of this work is to provide simulation-based support for making optimal (or near-optimal) decisions in situations where decision makers are faced with imperfect information. We develop several novel techniques and algorithms for simulation-based optimization and decision support and apply them to two categories of problems: (i) Unmanned Aerial Vehicle (UAV) path planning in search operations, and; (ii) optimization of business process models. Common features of these two problems for which analytical approaches are not available, are the presence of imperfect information and their inherent complexity. In the UAV path planning problem, the objective is to define the path of a UAV searching for a target on a known road network. It is assumed that the target is moving toward a goal and we have some uncertain information about the start point of the target, its velocity, and the final goal of the target. The target does not take evasive action to avoid being detected. The UAV is equipped with a sensor, which may detect the target once it is in the sensor’s scope. Nevertheless, the detection process is uncertain and the sensor is subject to both false-positive and false-negative errors. We propose three different solutions, two of which are simulation-based. The most promising solution is an on-line simulation-based method that estimates the location of the target by using a Sequential Monte Carlo (SMC) method. During the entire mission, different UAV paths are simulated and the one is chosen that most reduces the uncertainty about the location of the target. In the optimization of the business process models, several different but related problems are addressed: (i) we define a measure of performance for a business process model based on the value added by agents (employees) to the process; (ii) we use this model for optimization of the business process models. Different types of processes are distinguished and methods for finding the optimal or near-optimal solutions are provided; (iii) we propose a model for estimating the performance of collaborative agents. This model is used to solve a class of Assignment Problems (AP), where tasks are assigned to collaborative agents; (iv) we propose a model for team activity and the performance of a team of agents. We introduce different collaboration strategies between agents and a negotiation algorithm for resolving conflicts between agents. We compare the effect of different strategies on the output of the team. Most of the studied cases are complex problems for which no analytical solution is available. Simulation methods are successfully applied to these problems. They are shown to be more general than analytical models for handling uncertainty since they usually have fewer assumptions and impose no restrictions on the probability distributions involved. Our investigation confirms that simulation is a powerful tool for providing decision-making support. Moreover, our proposed algorithms and methods in the accompanying articles contribute to providing support for making optimal and in some cases near-optimal decisions: (i) our tests of the UAV simulation-based search methods on a simulator show that the on-line simulation method has generally a high performance and detects the target in a reasonable time. The performance of this method was compared with the detection time when the UAV had the exact information about the initial location of the target, its velocity, and its path (minimum detection time). This comparison indicated that the online simulation method in many cases achieved a near-optimal performance in the studied scenario; (ii) our business process optimization framework combines simulation with the Hungarian method and finds the optimal solution for all cases where the assignment of tasks does not change the workflow of the process. For the most general cases, where the assignment of tasks may change the workflow, we propose an algorithm that finds near-optimal solutions. In this algorithm, simulation, which deals with the uncertainty in the process, is combined with the Hungarian method and hill-climbing heuristics. In the study of assigning tasks to collaborative agents we suggest a Genetic Algorithm (GA) that finds near-optimal solutions with a high degree of accuracy, stability, scalability and robustness. While investigating the effect of different agent strategies on the output of a team, we find that the output of a team is near-optimal, when agents choose a collaboration strategy that follows the principle of least effort (Zipf’s law) and use our suggested algorithm for negotiation and resolving conflicts. / QC 20111202

We present a formal modeling approach for the design and simulation of Multi-Unmanned Aerial Vehicle (multi-UAV) inspection scenarios, where planning is based on model checking. As demonstration, we formalize and simulate a compositional UAV inspection system of a solar park using bigraphical reactive systems, which introduce the notion of time-varying bigraphs. Specifically, the UAV system is modeled as a process-algebraic expression, whose semantics is a bigraph state in a labeled transition system. The underlying Multi-Agent Path Finding problem is solved model-theoretically using Planning-by-Model-Checking. It solves the inherently connected collision-free path planning problem for multiple UAVs subject to contexts and local conditions. First, a bigraph is constructed algebraically, which can be decomposed systematically into separate parts with interfaces. The layered composite model accounts for location, navigation, UAVs, and contexts, which enables simple configuration and extension (changeability). Second, the executable operational semantics of our formal bigraph model are given by bigraphical reactive systems, where rules constitute the behavioral component of our model. Rules reconfigure the bigraph to simulate state changes, i.e., they allow to alter the conditions under which UAVs are permitted to move. Properties can be attached to nodes of the bigraph and evaluated in a simulation over the traces of the transition system according to some cost-based policies. In essence, the inherent multi-UAV path planning problem of our scenario is formulated as a reachability problem and solved by model checking the generated transition system. The bigraph-algebraic expression also allows us to reason about potential parallelization opportunities when moving UAVs. Moreover, we sketch how to directly simulate the bigraph specification in a ROS-based Gazebo simulation by examining the inspection and monitoring of a solar park as an application. The reactive system specification provides the blueprint for analysis, simulation, implementation and execution. Thus, the same algorithm used for verification is used as well for the simulation in ROS/Gazebo to execute plans.:1 Introduction 2 Overview: Scenario Description and Formal Modeling Approach 3 Background: Bigraphs and Model Checking 4 Construction of the UAV System via Composition 5 Making the Drones Fly: Executable Model Semantics 6 Collision-Free Path Planning Problem 7 Prototypical Implementation 8 Discussion 9 Related Work 10 Conclusion A UAV State Machine B Bigraphical Reactive Systems C RPO/IPO Semantic