In this section, we describe our synergistic offline-online control synthesis framework, which consists of two modules. The offline module constructs an IMDP abstraction for Process (REF ) and generates the baseline control strategy with a lower-bound guarantee on the probably of satisfying \(\varphi \) . The online module uses the offline abstraction and lower-bound probabilities to refine the control strategy and abstraction, which results in monotonic improvements to the guarantees.
We first briefly describe the offline module, which is based on previous work [1]}, and then detail the online module, which is the main contribution of this work.
