Bounded Cycle Synthesis

DOI10.1007/978-3-319-41528-4_7MaRDI QIDQ4633529zbMATH OpenOpenAlexFDO

Authors Bernd Finkbeiner, Felix Klein

Publication date 3 May 2019

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1605.01511

Mathematics Subject Classification ID

Temporal logic (03B44) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

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.

Recommendations

• Bounded Synthesis
• Symbolic bounded synthesis
• Iterative bounded synthesis for efficient cycle detection in parametric timed automata
• Encodings of bounded synthesis
• Register-bounded synthesis
• The network synthesis problem in a cycle
• The bounded cycle-cover problem
• scientific article; zbMATH DE number 4212104
• Bounded synthesis of register transducers

Cited in

(4)

• Encodings of bounded synthesis
• Bounded Synthesis
• scientific article; zbMATH DE number 2104638 (Why is no real title available?)
• Tableaux for realizability of safety specifications

This page was built for publication: Bounded Cycle Synthesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4633529)