Validating the correctness of reactive systems specifications through systematic exploration
Dor Ma’ayan, Shahar Maoz, Roey Rozi · 2022
Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from its temporal logic specification. While the synthesized system is guaranteed to be correct w.r.t. the specification, the specification itself may be incorrect w.r.t. the engineers' intention or w.r.t. the requirements or the environment in which the system should execute in. It thus requires validation.