LTL-based Specifications for P4 Program Synthesis

Programmable networks enable us to define the behaviour of a network through software. This added freedom comes with added complexity because multiple switches need to coordinate and be programmed correctly. To ease this task, we focus on intent-based networking via program synthesis. In this paper, we explain how to leverage linear temporal logic to describe the desired behaviour of a program, how to verify a P4 program against that description, and how to use the formula describing the program's behaviour to reduce the search space of the program synthesiser.