In this paper, we study how to make software controller synthesis more efficient and easy to use for engineers. In order to simplify specifying a system, we believe that existing methodologies in synthesis of reactive systems from Linear Temporal Logic (LTL) need to be extended with parameterized propositions. Therefore, we proposed to use the behavioral description language PDDL and reinterpret it under game concepts. Although the use of such high-level language eases modeling and results in understandable code, the size of the created game can be excessively large. Our main contribution is to view and adapt program optimization techniques as the key weapon for solving games locally, obtaining drastic performance gain. Results are implemented as an extension to the GAVS+ tool. In our evaluation, we have synthesized a control strategy for a demonstrator of FESTO's modular production system and translated the strategy into executable control code running on the production system.
Under review of VMCAI'12. Technical report can be found in
Videos of actual execution can be found in http://www6.in.tum.de/~chengch/gavs/simbesyn.html