Mode estimation Mode reconfiguration Select a most likely set of Select a least cost set of component modes that are commandable component consistent with the model and modes that entail the current observations goal, and are consistent System Model State estimates Tracks Tracks least likel cost goal states plant states arg min P(Y Obs) rg max R(Y) s.t. P(X,Y)AO(m)is consistent s.t.P(X,Y) entails G(X,Y) ons PI S.t. Y(X, Y) is consistent RMPL Model-b/OpSat I-based Executive Control pro arg min f(x) s.t. C(x)is satisfiable get goal states D(x)is unsatisfiable state estimates Asserts (hic System Model State estiman State goals Track Tracks least likely cost goal states plant state arg min P(Y Obs) arg max R(Y) s.t. P(X,Y)AO(m)is consistent s.t.Y(X,Y) entails G(X,Y) ons Pl s.t. Y(.Y) is consistentSystem Model Control Program RMPL Model-based Program Control Sequencer Deductive Controller Observations Commands Plant Titan Model-based Executive State estimates State goals Mode Estimation Mode Reconfiguration Tracks likely plant states Tracks least cost goal states z Executes concurrently z Preempts z Queries (hidden) states z Asserts (hidden) state Closed Valve Open Stuck open Stuck closed Open Close 0. 01 0. 01 0.01 0.01 inflow = outflow = 0 Generates target goal states conditioned on state estimates Mode Reconfiguration: Select a least cost set of commandable component modes that entail the current goal, and are consistent Mode Estimation: Select a most likely set of component modes that are consistent with the model and observations arg min Pt (Y| Obs) s.t. Ȍ(X,Y) š O(m’) is consistent arg max Rt (Y) s.t. Ȍ(X,Y) entails G(X,Y) s.t. Ȍ(X,Y) is consistent System Model Control Program RMPL Model-based Program Control Sequencer Deductive Controller Observations Commands Plant Titan Model-based Executive State estimates State goals Mode Estimation Mode Reconfiguration Tracks likely plant states Tracks least cost goal states z Executes concurrently z Preempts z Queries (hidden) states z Asserts (hidden) state Closed Valve Open Stuck open Stuck closed Open Close 0. 01 0. 01 0.01 0.01 inflow = outflow = 0 Generates target goal states conditioned on state estimates arg min Pt (Y| Obs) s.t. Ȍ(X,Y) š O(m’) is consistent arg max Rt (Y) s.t. Ȍ(X,Y) entails G(X,Y) s.t. Ȍ(X,Y) is consistent OpSat: arg min f(x) s.t. C(x) is satisfiable D(x) is unsatisfiable