Nondeterministic modeling and verification of networked robotic systems
Eric Klavins, John-Michael McNew · 2008
The advent and integration of wide-scale networking capabilities into the technological fabric of our society has spurred interest in the control of large scale networked multi-agent systems. The applications include air-traffic control, automated highway systems, and coordinated search and reconnaissance. The scale of these applications requires a distributed control methodology, and their potential integration with daily life requires proofs of safety, ease in programming and program distribution, self-organizing and self-stabilizing behaviors, and a general plug-and-play capability. Designing distributed control is challenging because communicating subsystems (cars, planes, etc.) are spatially distributed, and the flow of information among the subsystems is the result of complex interactions between their software, geometry, environment and operational modes. In supporting these developing needs, the main contributions of this thesis are the following: (1) A unified, graph-centric, local model of networked multi-agent systems called embedded graph grammars that abstracts away variables associated with message passing and considers all nondeterrninistic trajectories corresponding to different communication timings, communication orderings and program structures; (2) A design process which (in conjunction with the noncieterministic behavior of the embedded graph grammar model) provides an abstract control program that is portable across platforms; (3) Efficient (eventually automated) methods of reasoning about these systems and models, in particular Lexicographic Lyapunov Functions.