01750nas a2200157 4500008004100000245011500041210006900156300001200225520113700237653002101374653001301395100001901408700001501427700001601442856013401458 2007 eng d00aProbabilistic verification of decentralized multi-agent control strategies: a case study in conflict avoidance0 aProbabilistic verification of decentralized multiagent control s a170-1753 a
Many challenging verification problems arise from complex hybrid automata that model decentralized control systems. As an example, we will consider decentralized policies that steer multiple vehicles in a shared environment: properties of safety and liveness, such as collision avoidance and ultimate convergence of all vehicles to their goals, must be verified. To formally verify the behavior of proposed policies, it is desired to identify the broadest class of start and goal configurations, such that safety and liveness would be guaranteed. Simple conditions are proposed to identify such a class: ideally, a formal proof that such conditions are necessary and sufficient for safety and liveness is requested. Unfortunately, in decentralized control frameworks classical approaches are difficult to apply. Hence, probabilistic verification method can be applied to quantify the accuracy and the confidence of the veridicity of the desired predicate. The probabilistic verification method is applied to a recently proposed cooperative and completely decentralized collision avoidance policy for non-holonomic vehicles.
10aEmbedded Control10aRobotics1 aPallottino, L.1 aBicchi, A.1 aFrazzoli, E uhttp://www.centropiaggio.unipi.it/publications/probabilistic-verification-decentralized-multi-agent-control-strategies-case-study