Bounded Cycle Synthesis
Bernd Finkbeiner, Felix Klein

TL;DR
This paper presents a novel bounded cycle synthesis approach for Mealy machines from LTL specifications, resulting in simpler, more understandable implementations by limiting the number of cycles in the state graph.
Contribution
It introduces a SAT-based bounded synthesis method that incorporates cycle bounds and establishes bounds on the complexity of the cycle blow-up.
Findings
Bounded cycle synthesis produces simpler Mealy machines.
The approach effectively limits the number of cycles in implementations.
A triple-exponential bound relates LTL formula size to cycle count.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Model-Driven Software Engineering Techniques · Embedded Systems Design Techniques
