报告题目: Dependences in strategy logic
报 告 人：Patrick Gardy 博士 
主 持 人：邓玉欣 教授
报告时间：2018年6月20日 周三 10:00-11:00
报告地点：中北校区理科大楼B1102

报告人简介：

Patrick Gardy holds a PhD from Paris-Saclay University on temporal logics for multi-agent systems. He recently started a post-doctoral fellowship at ECNU. His main research interests are twofold: first in multi-agent systems, game theory, logic and formal verification; second on finite model theory and descriptive complexity.

报告摘要：

Strategy Logic (SL) is an expressive temporal logic for specifying and verifying game-theoretic properties of multi-agent systems. Since it enjoys a decidable (but non-elementary) model checking and high expressiveness, SL is a logic of choice for proving game-theoretic properties on a multi-agent systems (Nash equilibrium, rational synthesis, assume-admissible synthesis...).

    However, it has been noticed in recent works that the nice expressiveness of SL comes with unexpected phenomena. One such phenomenon concerns strategy dependencies: in a formula ∀α ∃β ξ, the existentially-quantified strategy β may depend on the whole strategy α, and not just on the choices of α on the current path. In other words, β depends globally on α. From this, two questions arise: can we get a compact representation of the data β needs from α ? And can we get a better model-checking algorithm when we limited dependencies? We present some of recent results in this area.