Enabling Reactive Synthesis through Runtime Verification

Reactive synthesis – automatic production of plans from high levelspecification – is emerging as a viable tool for the development ofrobots.Reactive synthesis from temporal logic specification is now a wellknown technique in applications of robotics.However, to date, this type of synthesis has had little impact onother fields.Our view is that the restrictions on usage of synthesis both due tothe capacity of tools and due to the kind of specifications that canbe supported are a barrier to the further usage of synthesis.We will combine techniques of reactive synthesis withruntime verification.We will use two advantages of runtime verification to further promotereactive synthesis.First, the ability of runtime verification to express specificationsthat go much beyond discrete-time temporal logic and regularlanguages.Second, the efficiency of translating these specifications tomonitors.By using runtime verification techniques to handle parts of thespecifications we will enable more expressive specifications that willbe handled more efficiently.This project, supporting a PhD student, combines our existingexpertise in reactive synthesis (applicant) and runtime verification(co-applicant) as co-supervisors.Our results will enable the routine use of reactive synthesis in manyfields and further extend its usage in robotics.Thus, it will further push forward the revolution ofcorrect-by-construction design of systems from specifications.