Counterexample-guided inference of controller logic from execution traces and temporal formulas
Чивилихин Даниил Сергеевич, Igor Buzhinsky, Vladimir I. Ulyantsev, Andrey Stankevich, Anatoly Abramovich Shalyto, Valeriy V. Vyatkin · 2018
We developed an algorithm for inferring controller logic for cyber-physical systems (CPS) in the form of a state machine from given execution traces and linear temporal logic formulas. The algorithm implements an iterative counterexample-guided strategy: constraint programming is employed for constructing a minimal state machine from positive and negative traces (counterexamples) while formal verification is used for discovering new counterexamples. The proposed approach extends previous work by (1) considering a more intrinsic model of a state machine making the algorithm applicable to synthesizing CPS controller logic, and (2) using closed-loop verification which allows considering more expressive temporal properties.