גרא וייס

Real life situations may require a drastic change in program (control), rather than an incremental update, e.g. changing a control in an airplane or in an atomic reactor that experience an unexpected disaster emergency scenario. We suggest a formal framework for automatic runtime control search. We present a catalog of control search algorithms for various settings of an execution environment. The considered environment properties are: (1) determinism—an environment can be either deterministic or probabilistic, (2) state reflection that allows observation of the current state of the environment, (3) state set that generalizes the reset capability, allowing setting the environment to a particular state, and (4) (static or dynamic) replication that allows instantiation of replicas for parallel execution of candidate controls. In deterministic environment settings, a control search algorithm creates all candidate programs, executes them in parallel on environment replicas, and returns a program that respects desired specifications. In probabilistic environment settings, a control search algorithm learns the environment probabilistic automaton, and then the control search algorithm is performed in run time, deciding on a next step based on a current state.