On Decidable Fragments of dL

Decidable fragments of differential dynamic logic (dL) are of interest to its proof theory, but also to the practice of verifying cyberphysical systems; for example, integration into KeYmaera X could improve usability by discharging or refuting “boilerplate” goals automatically. Here we do three things to contribute to the knowledge of the decidability of dL. For one, we work bottom-up and identify a few decidable fragments and describe their decision procedures. These include the strictly-polynomial star-free (i.e. asteratefree) fragment and certain simultaneously box-and-diamond fragments. We provide an implementation of a decision procedure for the former in OCaml (see our final project deliverables). For another, we work top-down and identify many undecidable fragments of dL. Many different approaches are considered, including restricting quantifiers, limiting the number of variables, bounding the domain of computation, and restricting arithmetical operators. This contributes in much the way Edison showed many ways to not make a lightbulb. Finally, we connect pieces in the middle to show inter-decidability of a few fragments. Should further decidability results come in the future, using these could immediately extend them.