Efficient Controller Synthesis For A Fragment Of Mtl0,Infinity

In this paper we offer an efficient controller synthesis algorithm for assume-guarantee specifications of the form . Here, are all safety-MTL properties, where the sub-formulas are supposed to specify assumptions of the environment and the sub-formulas are specifying requirements to be guaranteed by the controller. Our synthesis method exploits the engine of Uppaal-Tiga and the novel translation of safety- and co-safety-MTL properties into under-approximating, deterministic timed automata. Our approach avoids determinization of Buchi automata, which is the main obstacle for the practical applicability of controller synthesis for linear-time specifications. The experiments demonstrate that the chosen specification formalism is expressive enough to specify complex behaviors. The proposed approach is sound but not complete. However, it successfully produced solutions for all the experiments. Additionally we compared our tool with Acacia+ and Unbeast, state-of-the-art LTL synthesis tools; and our tool demonstrated better timing results, when we applied both tools to the analogous specifications.