Course Program

Transition systems and model checking.

Transition Systems, Fixpoint theory over transition systems, Checking Dynamics on Transition Systems. MuCalculus, CTL,

Reasoning about actions.

Models of world dynamics, Action theories, SitCalc, PDDL, Checking executability, Checking projection, Checking dynamic properties.

Planning in deterministic and nondeterministic domains.

Classical planning: Planning for reachability goals in deterministic domains, FONDunr: Planning for reachability goals in nondeteministic domains, Reachability (adversary) games, Solving reachability games, FONDfair: Planning for reachability goals in fair nondeterministic domains, Connection with MDPs, Fair reachability games, Solving fair reachability games.

Synthesis for LTLf and LDLf goals.

Linear-time Temporal Logic (LTL), LTLf and LDLf on finite traces, LTLf and LDLf goals, Connections to automata, Computing DFAs, Manipulating DFAs, Planning for LTLf and LDLf goals, Synthesis for LTLf and LDLf goals, MDPs with LTLf and LDLf goals and rewards, MDPs with LTLf and LDLf goals and rewards.

Multi behavior composition and coordination.

Behavior Composition, Coordinating multiple agents/devices/robots, Examples from services, manifacturing and cognitive robotics, Behavior Composition, Safety games, Solving safety games, Connections to Supervisory Control.