RMPL Model-based program Titan Model-based Executive Control Program Control Sequencer Execut s concurrently Generates goal, states Preer Ass ' d queries states conditioned on stat\ estimates ed on reward State estimates State goals Model ode Orbitlnsert(0∷ tImation: MAINTAIN(EAR OR EBR) (do-watching(EngineA=Firing) OR (EngineB= Firing) cks likel EAS (EngineA =Standby) States (Engine=Standby) (EngineB= Standby) (Camera= Off) ons MAINTAIN (EAF) SAND CO) (do-watching(EngineA=Failed) Plant (when-donext((EngineA= Standby) AND EAS AND co W (Camera=Off)) Engine=Firing))) (EAF AND EBS AND CO) (when-donext((EngineA=Failed) AND +6 EAF AND EBS (Engine B= Standby) AND (Camera=Off)) hierarchical constraint = Firing) automata on state sControl 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