01.10.2021 –, KI: Room John McCarthy
Sprache: English
A central topic in AI is building autonomous agents that act intelligently. Reactive Synthesis, Planning in Nondeterministic Domains and Reinforcement Learning are all about automatically synthesizing an agent behavior/strategy/policy to accomplish a task in a partially controllable (nondeterministic) world. In this context, it is important to sharply distinguish between the world model (the domain) and the task specification (the goal), to take into account the fact that model of world seldom change, while the tasks that the agent has to accomplish in it change unceasingly as the agent operates. As a result, the agent will work for a task only for finite amount of time (before switching to the next), while the world continues to exist when the task is over. In this talk we discuss these issues, and consider various forms of synthesis, where the world and the agent tasks are expressed in Liner Temporal Logic, LTL, the formalism most commonly used in Formal Methods for specifying dynamic properties, as well as in its finite-trace variant, LTLf, which is particularly useful for specifying intelligent agent tasks.