BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verified Unsolvability of Temporal Planning - David Wang (King's C
 ollege London)
DTSTART:20250320T170000Z
DTEND:20250320T180000Z
UID:TALK225322@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:The project aims to implement a verified reduction from Tempor
 al Planning to Timed Automata\, targeting a model checker which was verifi
 ed in Isabelle/HOL. The model checker can output and check certificates fo
 r unsatisfied reachability properties. This results in a checkable claim t
 hat a state corresponding to the goal of a planning problem is unreachable
  and the problem is therefore unsolvable. Strong correctness guarantees wi
 ll be provided by proving the correctness of the reduction in Isabelle/HOL
 .\n\nAs the project itself is incomplete\, I will introduce the topics\, e
 xplain how they relate\, and show some formalization methodology where app
 licable and relevant.\n\nAutomated 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 con
 cerned with scheduling concurrent actions on a continuous timeline. Planni
 ng languages\, like the Planning Domain Definition Language (PDDL)\, can b
 e given formal semantics using abstract formalisms\, like Temporal Proposi
 tional Planning. The latter is an abstract formalism which restricts plann
 ing to a set-theoretic characterization of the world.\n\nA timed automaton
  is an abstract formalism to describe a transition system with discrete st
 ates and continuous time. Temporal Propositional Planning can be re-examin
 ed from an automata-theoretic perspective using Timed Automata. Timed Auto
 mata are targets for Model Checking\, an automated technique to ensure tha
 t models of computer systems satisfy properties over (possibly infinite) s
 equences of actions. \n\n=== Hybrid talk ===\n\nJoin Zoom Meeting https://
 cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1\n\nMe
 eting ID: 871 4336 5195\n\nPasscode: 541180
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR