Game Solving for Industrial Automation and Control – Models,Algorithms, and Tools

Title:Game Solving for Industrial Automation and Control – Models,Algorithms, and Tools
Speaker:Chih-Hong Cheng (Fortiss, Technical University Munich, Germany)
Time: 2:30pm, October 18th (Tuesday), 2011.
Venue:Lecture Room, Level 3, Building No. 5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

Abstract: An ongoing effort within the community of verification and program analysis is to raise the level of abstraction in programming by automatic synthesis. In this talk, we demonstrate how we approach this goal by three perspectives: appropriate models, faster algorithms, and tools. For models, we reinterpret planning domain definition language (PDDL) as a design contract to model two-player games played between control and environment, such that users can describe (i) basic abilities of hardware components, including sensors (as environment moves) and actuators (as control moves),(ii) topology how components are interconnected, and (iii) desired specification under a restricted class of linear temporal logic.

For algorithms, we view and adapt program optimization techniques as the key weapon for solving games locally, obtaining drastic performance gain. Lastly for tools, we present MGSyn, an opensource framework which tightly integrates game-based synthesis (GAVS+ solver library) into model-driven development (Eclipse Modeling Framework) under the application of industrial automation.When time permitted, we report our preliminary case study for the design of FESTO modular production systems.

Bibliography:
Chih-Hong Cheng received his master degree from National Taiwan University. He pursued his doctoral degree in Technical University Munich and had recently submitted his thesis (under review). Since July 2011, he joined fortiss GmbH (An Software Institute of Technical University Munich) as a staff researcher, leading the subgroup of formal methods in cyber-physical systems. His research interest includes formal methods and embedded systems, with special focus in game-based synthesis.