Course Program

Introduction. Motivations and aims of the course

Reasoning about Actions. SitCalc, Reiter's Basic Action Theories, Reasoning by regression in SitCalc, Finite Transitions Systems induced by Propositional Basic Action Theories.

Planning. Planning in deterministic domains. Transition System induced by a deterministic planning domain. Planning as search. Planning as fixpoint computation over a transition system. Planning in nondeterministic domains. Transition System, or game arena, induced by a nondeterministic planning domain. Planning as fixpoint computation over a game arena.

Transition system and fixpoints. Reactive/interactive programs (finite state), transition systems, reachability, bisimulation. Fixpoints, Knaster-Tarski theorem on least and greatest fixpoint, approximates for least and greatest fixpoint. 

Linear Temporal Logics. Linear Temporal Logic on infinite traces from Formal Methods. Linear Temporal Logics on finite traces. LTLf to Automata. Reasoning in LTLf, verification in LTLf. Pure Past LTL (PPLTL) and Automata

Program synthesis. Automated program synthesis, synthesis from specifications in Linear Temporal Logic on finite traces, game-theoretic view, arena and objective, adversarial reachability. Synthesis under environment specifications. Planning for LTLf goals in nondeterministic domains as synthesis under environment specifications.