Correct-by-construction distributed control for multi-vehicle transport systems

In this work we deal with a system of autonomous mobile vehicles with limited communication range and consider the problem of the formally correct distributed control, i.e., the design of the local control for each particular agent so that it ensures globally correct behavior of the system. A particular problem is the fact that the knowledge about the system state possessed by the agents is partial and never accurate, as during the time of information acquisition (by querying other agents) the state of the agents can change. The paper capitalizes on the results of [1] and contributes with: 1) further development of the theoretical idea toward the distributed supervisory control and the concept of robustness, 2) application of the results in the design of a transport agent, and 3) development of a demonstrator, i.e., a computer application that enables the user to specify a considered transport system and its tasks, creates a virtual environment, where each particular vehicle is represented by a particular software agent implementing the control model of (2), and allows observation of the agents concurrent operation and quantitative assessment of the system performance.