Probabilistic Safety Analysis of Sensor-DrivenHybrid AutomataJulia M. B. Braman and Richard M. MurrayDept. of Mechanical Engineering, California Institute of [email protected]. The control programs of complex autonomous systems thathave conditional branching can be modeled as linear hybrid systems.When the state knowledge is perfect, linear hybrid systems with state-based transition conditions can be verified against a specified unsafe setusing existing model checking software. This paper introduces a formalmethod for calculating the failure probability due to state estimationuncertainty of these sensor-driven hybrid systems. Problem complexityis described and some reduction techniques for the failure probabilitycalculation are given. An example goal-based control program is givenand the failure probability for that system is calculated.1 IntroductionAutonomous robotic missions generally have complex, fault tolerant control sys -tems. There are several ways to incorporate the necessary fault tolerance in acontrol architecture. One way is to create a flexible control system that can re-configure itself based on the state of the system and environment in the presenceof faults. However, if the control system cannot be analyzed for safety in the pres-ence of e stimator error, the added complexity of the system’s reconfigurabilitycould reduce the system’s effective fault tolerance.One particularly useful way to model a fault tolerant control system is as ahybrid system. When the continuous dynamics of these systems are sufficientlysimple, it is possible to verify that the execution of the hybrid control system willnot fall into an unsafe regime [1]. There are several software packages that canbe used for this analysis, including HyTech [2], UPPAAL [3], and PHAVer [4],all of which are symbolic model checkers. PHAVer in particular is able to exactlyverify linear hybrid systems with piecewise constant bounds on continuous statederivatives. Safety verification for fault tolerant hybrid control systems ensuresthat the occurrence of certain faults will not cause the system to reach an unsafestate.However, these verification software packages cannot handle uncertainty inthe estimated state variables involved in mode transition logic. For autonomoussystems, none of the state variables used in the control system are known per-fectly, and these uncertainties can affect the safety of the system. Stochastichybrid systems include uncertainty in the transitions of the hybrid autom atonSubmitted, 2009 Hybrid Systems: Computation and Control (HSCC)http://www.cds.caltech.edu/~murray/papers/2008s_hm09-hscc.htmlas probabilistic transition conditions. Many pape rs have been written on the ver-ification of stochastic hybrid systems. For example, Prajna et al [5] use barriercertificates to bound the upper limit of the probability of failure of the stochastichybrid system and Kwiatkowska et al [6] discuss a probabilistic symbolic modelchecking software called PRISM. However, purely probabilistic transition con-ditions do not model estimation uncertainty in the constrained state variableswell; deterministic transitions with probabilistic components may be a bettermodel.In this paper, a formal method for determining the failure probability due toestimation uncertainty of a verifiable hybrid system with sensor-driven, state -based transitions, which builds on the work in [7], is given. These particular hy-brid systems are derived from goal-based control programs called goal networks.Mission Data System (MDS), a goal-based control architecture developed at theJet Propulsion Laboratory, is the basis for the design of these goal networks[8]. The goal networks are then converted using a bisimulation to linear hybridautomata and verified against an unsafe set using existing symbolic model check-ing software such as PHAVer [9]. The discrete mode transitions in the hybridautomata are then based on the state variables of the system estimated fromsensor values.As an illustration of the type of tasks analyzed, consider the sensor-basedplanning problem shown in Fig. 1. This rover, which must safely follow thepath to the specified end point, has three main sensor systems: GPS, LADAR,and an inertial measurement unit (IMU). The speed limit along the path isdependent on the combined health of these sensors. Each sensor degrades orfails in a specified way. The GPS can experience periods of reduced accuracy(e.g. satellite dropouts) or failure (electrical or structural signal interference),and these can both be modeled as recoverable stochastic events. The LADARhealth depends on the location of the sun in the sky and whether the robot is industy conditions; however it will also be modeled as degrading and recoveringstochastically. Finally, the IMU health is dependent on the temperature of thedevice. If the temperature of the IMU is to o low, a heater can be used to heatthe sensor. If the IMU temperature gets too high, the unit must b e powered off.For the safety of the system, it is important to verify the goal networks for thisproblem against the following unsafe set:1. The rover is not stopped when the IMU is off and the GPS is degraded.2. The rover moves forward when the LADAR unit is compromised.The methods described in this paper allow the analysis of the safety of thecontrol program against the given unsafe set when the estimation of the sensorhealth values is not perfect. If these states were known exactly, a traditionalhybrid system verification would b e a sufficient test of the safety of this system.However, a full analysis of this system must include the calculation of the failureprobability due to estimation uncertainty, for which a method is introduced here.The paper is organized as follows. A summary of goal network specificationsand the conversion procedure can be found in Section 2. Section 3 is the mainFig. 1. A depiction of the example task where the rover must traverse a path and reachthe end point, which is marked with a star, and the goal network associated with it.contribution of this paper, the failure probability calculation for the convertedlinear hybrid systems, which formalizes and extends the process developed in[7]. Section 4 describes the complexity of this calculation and lists some reduc-tion techniques. Section 5 is the failure probability calculation for the exampleintroduced above, and Section 6 summarizes the contributions and describesdirections for future work.2