Top

Published in:

2016 | OriginalPaper | Chapter

Bounded Cycle Synthesis

Authors : Bernd Finkbeiner, Felix Klein

Published in: Computer Aided Verification

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Structural Synthesis for GXW Specifications

next chapter Fast, Flexible, and Minimal CTL Synthesis via SMT

Note that not every such edge needs to exist for a concrete given graph. However, in our worst-case analysis, every possible cycle is accounted for.

Our representation is open for many optimizations. However, they will not affect the overall complexity result. Thus, we ignore them for the sake of readability here.

Note that the tree property is enforced by Conditions 3–5.

Alur, R., La Torre, S.: Deterministic generators and games for LTL fragments. ACM Trans. Comput. Log. 5(1), 1–25 (2004). http://doi.acm.org/10.1145/963927.963928 MathSciNetCrossRef

ARM Ltd.: AMBA Specification (rev. 2) (1999). www.arm.com

Babiak, T., Křetínský, M., Řehák, V., Strejček, J.: LTL to Büchi automata translation: fast and more deterministic. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 95–109. Springer, Heidelberg (2012). http://dx.doi.org/10.1007/978-3-642-28756-5_8 CrossRef

Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140–156. Springer, Heidelberg (2009). http://dx.doi.org/10.1007/978-3-642-02658-4_14 CrossRef

Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004). http://dx.doi.org/10.1007/978-3-540-24605-3_37 CrossRef

Filiot, E., Jin, N., Raskin, J.: Antichains and compositional algorithms for LTL synthesis. Form. Methods Syst. Des. 39(3), 261–296 (2011). http://dx.doi.org/10.1007/s10703-011-0115-3 CrossRefMATH

Filiot, E., Jin, N., Raskin, J.: Exploiting structure in LTL synthesis. STTT 15(5–6), 541–561 (2013). http://dx.doi.org/10.1007/s10009-012-0222-5 CrossRef

Finkbeiner, B., Klein, F.: Bounded cycle synthesis. CoRR abs/1605.01511 (2016). http://arxiv.org/abs/1605.01511

Finkbeiner, B., Schewe, S.: Bounded synthesis. STTT 15(5–6), 519–539 (2013). http://dx.doi.org/10.1007/s10009-012-0228-z CrossRefMATH

10.

Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: clasp: a conflict-driven answer set solver. In: Baral, C., Brewka, G., Schlipf, J. (eds.) LPNMR 2007. LNCS (LNAI), vol. 4483, pp. 260–265. Springer, Heidelberg (2007). http://dx.doi.org/10.1007/978-3-540-72200-7_23 CrossRef

11.

Jacobs, S., Klein, F.: A high-level LTL synthesis format: TLSF v1.1 (Extended Version). CoRR abs/1604.02284 (2016). http://arxiv.org/abs/1604.02284

12.

Jobstmann, B.: Applications and optimizations for LTL synthesis. Ph.D. thesis, Graz University of Technology, March 2007

13.

Johnson, D.B.: Finding all the elementary circuits of a directed graph. SIAM J. Comput. 4(1), 77–84 (1975). http://dx.doi.org/10.1137/0204007 MathSciNetCrossRefMATH

14.

Kupferman, O.: Recent challenges and ideas in temporal synthesis. In: Bieliková, M., Friedrich, G., Gottlob, G., Katzenbeisser, S., Turán, G. (eds.) SOFSEM 2012. LNCS, vol. 7147, pp. 88–98. Springer, Heidelberg (2012). doi:10.1007/978-3-642-27660-6_8 CrossRef

15.

Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005), 23–25 October 2005, Pittsburgh, PA, USA, Proceedings, pp. 531–542. IEEE Computer Society (2005). http://dx.doi.org/10.1109/SFCS.2005.66

16.

Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3) (2007). http://dx.doi.org/10.2168/LMCS-3(3:5)2007

17.

Tiernan, J.C.: An efficient search algorithm to find the elementary circuits of a graph. Commun. ACM 13(12), 722–726 (1970). http://doi.acm.org/10.1145/362814.362819 MathSciNetCrossRefMATH

18.

Weinblatt, H.: A new search algorithm for finding the simple cycles of a finite directed graph. J. ACM 19(1), 43–56 (1972). http://doi.acm.org/10.1145/321679.321684 MathSciNetCrossRefMATH

Title: Bounded Cycle Synthesis
Authors: Bernd Finkbeiner
Felix Klein
Publisher: Springer International Publishing
Book: Computer Aided Verification
Print ISBN: 978-3-319-41527-7

Electronic ISBN: 978-3-319-41528-4

Copyright Year: 2016
DOI: https://doi.org/10.1007/978-3-319-41528-4_7

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner