Stochastic hybrid systems modeling and performance verification of behavior-based robots

Behavior-based robotics (BBR) has gained popularity because of its simplicity, flexibility and adaptability. However, lack of formalization from performance guarantee aspect has been a concern in BBR especially for safety critical applications. Motivated by this challenge, we propose a formal model for BBR using a discrete-time controlled stochastic hybrid system (dt-cSHS) framework. Uncertainties from sensors, actuators, and the environment are modeled by stochastic kernels in the dt-cSHS. For performance verification, safety and reachability specifications are considered; abstraction and model checking are carried on the hybrid system model. The modeling and verification procedures are illustrated by examples of BBR applications.