Abstract:

Model checking and decision problems, including discrete variables, are often modeled by transition systems and predicate logic. Combining these two frameworks results in a unified model based on modular Petri nets with shared variables. An incremental abstraction method is also introduced for complex temporal logic planning. Uncontrollable events, as well as mu-calculus, are then shown to be interesting alternatives to more common game formulations. Optimization of systems with discrete variables often integrates methods from AI and operation research. An interesting alternative is the model checker Z3, which now also includes optimization. For hybrid systems, a specific method is also presented for energy optimization of robot systems, resulting in up to 30% energy and 50% peak power reduction. Finally, a recent integration of temporal logic and reinforcement learning is discussed. To summarize, methods from model checking are shown to be very useful for AI planning, learning and optimization.

Bio:

Bengt Lennartson is a Professor of the Chair of Automation since 1999 at Chalmers University of Technology, Gothenburg, Sweden. He is Head of the Division of Systems and Control at the Department of Electrical Engineering, and he is IEEE Fellow for his contributions to hybrid and discrete event systems for automation and sustainable production. He has been Associate Editor for Automatica and IEEE Transaction on Automation Science and Engineering, General Chair of IEEE CASE 2015, WODES 2008 and Dean of Education at Chalmers. He is the (co)author of more than 300 peer reviewed international papers, and his research is currently focused on AI planning and learning, as well as sustainable production.   

欢迎广大老师和同学们参加！