Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up
Benjamin Aminof, Giuseppe De Giacomo, Sasha Rubin
Abstract
We study best-effort synthesis under environment assumptions specified in LTL, and show that this problem has exactly the same computational complexity of standard LTL synthesis: 2EXPTIME-complete. We provide optimal algorithms for computing best-effort strategies, both in the case of LTL over infinite traces and LTL over finite traces (i.e., LTLf). The latter are particularly well suited for implementation.
Topics & Concepts
Computer scienceBest practiceTheoretical computer scienceLinear temporal logicComputational complexity theoryAlgorithmManagementEconomicsFormal Methods in VerificationLogic, programming, and type systemsModel-Driven Software Engineering Techniques