Playing with Synthesis
Satisfiability, Realisability, and Synthesis
Temporal logic is a popular language to write specifications of programs. A temporal logic formula is evaluated over traces (of programs) and is either true or false for a given trace. Normally, a very important property is that of satisfiability - the existence of a trace that satisfies a property. Clearly, if a formula is unsatisfiable it is not very interesting to check whether a given trace satisfies it or not as the answer is always no.
Accordingly, temporal logic is used to write specifications of programs and, for example, a program can be model checked to ensure that all its traces satisfy the property or a program can be monitored during runtime to ensure that the produced trace satisfies the property.
In recent years, temporal logic is used also for automatically producing programs that are ensured to satisfy the specifications. The events that the formula relates to are partitioned to input and output and the requirement is for a machine that will receive inputs and reply with outputs in a way that satisfies the specification. For example, here this technique is used to produce a plan for a robot from a high level specification of its desired behavior.
In this context the relevant questions are those of realisability - does there exist an open system (can receive all inputs) that sets the outputs so that the specification holds - and synthesis - the actual production of such a system.
The idea of this project is to play practically with synthesis and synthesis tools and improve them. Concrete ideas for example:
- Create your own synthesis tool to participate in the synthesis competition.
- Change synthesis algorithms implemented in existing tools and benchmark them to compare with previous implementations.
- Add algorithms that explore synthesis imposibility and help users debug their specifications.
For the theoretical part - after getting to understand the involved issues - the student will turn to implementation and experimentation.
Related Courses: Finite automata theory and formal languages, Formal Methods in Software Development
Prerequisites: Programming (Java, Python, …), automata theory, logic.
Desired: Temporal logics and formal verification, formal modelling and verification tools
Contact: Nir Piterman (firstname.lastname@example.org)