Bounded Cycle Synthesis
Bernd Finkbeiner and Felix Klein
We introduce a new approach for the synthesis of Mealy machines from specifications in linear-time temporal logic (LTL), where the number of cycles in the state graph of the implementation is limited by a given bound. Bounding the number of cycles leads to implementations that are structurally simpler and easier to understand. We solve the synthesis problem via an extension of SAT-based bounded synthesis, where we additionally construct a witness structure that limits the number of cycles. We also establish a triple-exponential upper and lower bound for the potential blow-up between the length of the LTL formula and the number of cycles in the state graph.
28th International Conference on Computer Aided Verification, (CAV 2016).
Copyright by Springer Verlag. The original publication is available at www.springerlink.com.