Has Executive Manipulates Hidden State MERS CSAIL States not directly observable or controllable Given observations (thrust zero) AND(power in nominal and command history last command issued ="standby-cmd Mode estimation infers →( Engine= Standby) “ hidden state Given state goals (ValveA= Open and estimated state (DriverA =off) AND(ValveA =closed) Mode reconfiguration =Turn on DriverA: [Open ValveA Inters commands Thinking in terms of hidden states"abstracts away complexity of robustly observing and controlling state Model-based executive raises assurance of software by correctly inferring and controlling states RMPL Model-based Program Titan Model-based Executive Control Program Control Sequencer Executes concurrently Generates goal states Pre Asserts and queries states conditioned on stay\ estimates Chooses based on reward State estimates State goals Model Mode lode Estima Tracks likely (do-watching ((EngineAs Firing) State Observations AF) (EASANDCO (do-watching(Eng neA= Fa led) Plant mera=O) EngineA s Firing》) EAF ANDEBS AND CO) twhen-donext((EngineAs Failed)AND Engine= Firing)))) hierarchical constraint utomata on state s
Given observations… and command history… Mode estimation infers “hidden state” Executive Manipulates Hidden State • States not DIRECTLY observable or controllable… (thrust = zero) AND (power_in = nominal) last command issued = “standby last command issued = “standby-cmd” ⇒ (EngineA = Standby) Given state goals … and estimated state … Mode reconfiguration infers “commands” ⇒ [Turn on DriverA]; [Open ValveA] • Thinking in terms of “hidden states” abstracts away complexity of robustly observing and controlling state. • Model-based executive raises assurance of software by correctly inferring and controlling states. (ValveA = Open) (DriverA = off) AND (ValveA = closed) Control Sequencer Deductive Controller System Model Commands Observations Control Program Plant RMPL Model-based Program Titan Model-based Executive State estimates State goals Control Sequencer: Generates goal states conditioned on state estimates Mode Estimation: Tracks likely States Mode Reconfiguration: Tracks least-cost state goals z Executes concurrently z Preempts z Asserts and queries states z Chooses based on reward OrbitInsert():: (do-watching ((EngineA = Firing) OR (EngineB = Firing)) (parallel (EngineA = Standby) (EngineB = Standby) (Camera = Off) (do-watching (EngineA = Failed) (when-donext ( (EngineA = Standby) AND (Camera = Off) ) (EngineA = Firing))) (when-donext ( (EngineA = Failed) AND (EngineB = Standby) AND (Camera = Off) ) (EngineB = Firing)))) MAINTAIN (EAR OR EBR) EBS CO LEGEND: EAS (EngineA = Standby) EAF (EngineA = Failed) EAR (EngineA = Firing) EBS (EngineB = Standby) EBF (EngineB = Failed) EBR (EngineB = Firing) CO (Camera = Off) MAINTAIN (EAF) EAS (EAS AND CO) EAR EAS AND CO (EAF AND EBS AND CO) EBR EAF AND EBS AND CO hierarchical constraint automata on state s
RMPL Model-based Program Titan Model-based executive Control Program Control Sequencer Executes concurrently Generates goal states Preempts conditioned on state estimates Asserts and queries states Chooses based on reward State estimates State goals ystem Model Mod Estimation Reconfiguration Tracks likely Tracks least-cost 空2 Command Valve fails Pla stuck closed Fire backup least cost reachable Current belief State First Action goal state Modeling Complex Behaviors through Probabilistic constraint automata Engine Model Camera model standby (= zerDAN Standby (power in= nominal) os Firing( Complex. discrete behaviors modeled through concurrency, hierarchy and timed transitions Anomalies and uncertainty modeled by probabilistic transitions Physical interactions modeled by discrete and continuous constraints
Control Sequencer Deductive Controller System Model Commands Observations Control Program Plant RMPL Model-based Program Titan Model-based Executive State estimates State goals Control Sequencer: Generates goal states conditioned on state estimates Mode Estimation: Tracks likely States Mode Reconfiguration: Tracks least-cost state goals z Executes concurrently z Preempts z Asserts and queries states z Chooses based on reward Fire backup engine Valve fails stuck closed S T X0 X1 XN-1 XN S T X0 X1 XN-1 XN least cost reachable Current Belief State First Action goal state Modeling Complex Behaviors through Probabilistic Constraint Automata • Complex, discrete behaviors • modeled through concurrency, hierarchy and timed transitions. • Anomalies and uncertainty • modeled by probabilistic transitions • Physical interactions • modeled by discrete and continuous constraints Standby Engine Model Engine Model Off Failed offcmd standbycmd 0.01 (thrust = full) AND (power_in = nominal) Firing 0.01 standbycmd firecmd (thrust = zero) AND (power_in = zero) (thrust = zero) AND (power_in = nominal) On Camera Model Camera Model Off turnoffcmd turnoncmd (power_in = zero) AND (shutter = closed) (power_in = nominal) AND (shutter = open) 0 v 2 kv 2 kv 0 v 0 v 20 v 0.01 0.01 0 v