Investigate CEGAR techniques to improve goal search efficiency
Discussed with Sophie and Théo @ x-TMatri Abstraction Refinement (CEGAR) could be used to improve efficiency of the search of reachable Witness. (https://link.springer.com/article/10.1007/s10817-019-09535-x)
Need to define the algo.
Can be applied:
-
at the ABS level (ie. work at the class level . Possibly less precise but faster ?) -
at the gal level (ie. Work at the instance level. Possibly more precise but more difficult to explain/implement ?)
Edited by Vojtisek Didier