Verified Unsolvability of Temporal Planning

Add to your list(s) Download to your calendar using vCal

• David Wang (King's College London)
• Thursday 20 March 2025, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

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

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.