Abstract

The project aims to implement a verified reduction from Temporal Planning to Timed Automata, targeting a model checker which was verified in Isabelle/HOL. The model checker can output and check certificates for unsatisfied reachability properties. This results in a checkable claim that a state corresponding to the goal of a planning problem is unreachable and the problem is therefore unsolvable. Strong correctness guarantees will be provided by proving the correctness of the reduction in Isabelle/HOL.

As the project itself is incomplete, I will introduce the topics, explain how they relate, and show some formalization methodology where applicable and relevant.

Automated Planning is an area of computer science concerned with symbolic representation of problems and symbolic reasoning to solve problems. Temporal Planning is an area of automated planning concerned with scheduling concurrent actions on a continuous timeline. Planning languages, like the Planning Domain Definition Language (PDDL), can be given formal semantics using abstract formalisms, like Temporal Propositional Planning. The latter is an abstract formalism which restricts planning to a set-theoretic characterization of the world.

A timed automaton is an abstract formalism to describe a transition system with discrete states and continuous time. Temporal Propositional Planning can be re-examined from an automata-theoretic perspective using Timed Automata. Timed Automata are targets for Model Checking, an automated technique to ensure that models of computer systems satisfy properties over (possibly infinite) sequences of actions.

=== Hybrid talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1

Meeting ID: 871 4336 5195

Passcode: 541180