Advertisement

Bounded Synthesis of Register Transducers

  • Ayrat KhalimovEmail author
  • Benedikt Maderbacher
  • Roderick Bloem
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)

Abstract

Reactive synthesis aims at automatic construction of systems from their behavioural specifications. The research mostly focuses on synthesis of systems dealing with Boolean signals. But real-life systems are often described using bit-vectors, integers, etc. Bit-blasting would make such systems unreadable, hit synthesis scalability, and is not possible for infinite data-domains. One step closer to real-life systems are register transducers [10]: they can store data-input into registers and later output the content of a register, but they do not directly depend on the data-input, only on its comparison with the registers. Previously [5] it was proven that synthesis of register transducers from register automata is undecidable, but there the authors considered transducers equipped with the unbounded queue of registers. First, we prove the problem becomes decidable if bound the number of registers in transducers, by reducing the problem to standard synthesis of Boolean systems. Second, we show how to use quantified temporal logic, instead of automata, for specifications.

References

  1. 1.
    Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). www.SMT-LIB.org
  2. 2.
    Church, A.: Logic, arithmetic, and automata. In: International Congress of Mathematicians (Stockholm, 1962), pp. 23–35. Institute Mittag-Leffler, Djursholm (1963)Google Scholar
  3. 3.
    Demri, S., D’Souza, D., Gascon, R.: Temporal logics of repeating values. J. Log. Comput. 22(5), 1059–1096 (2012).  https://doi.org/10.1093/logcom/exr013MathSciNetCrossRefGoogle Scholar
  4. 4.
    Demri, S., Lazić, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3), 16:1–16:30 (2009).  https://doi.org/10.1145/1507244.1507246MathSciNetCrossRefGoogle Scholar
  5. 5.
    Ehlers, R., Seshia, S.A., Kress-Gazit, H.: Synthesis with identifiers. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 415–433. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54013-4_23CrossRefGoogle Scholar
  6. 6.
    Finkbeiner, B., Schewe, S.: Bounded synthesis. STTT 15(5–6), 519–539 (2013)CrossRefGoogle Scholar
  7. 7.
    Frenkel, H., Grumberg, O., Sheinvald, S.: An automata-theoretic approach to modeling systems and specifications over infinite data. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 1–18. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-57288-8_1CrossRefGoogle Scholar
  8. 8.
    Grumberg, O., Kupferman, O., Sheinvald, S.: Variable automata over infinite alphabets. In: Dediu, A.-H., Fernau, H., Martín-Vide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 561–572. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-13089-2_47CrossRefzbMATHGoogle Scholar
  9. 9.
    Grumberg, O., Kupferman, O., Sheinvald, S.: Model checking systems and specifications with parameterized atomic propositions. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, pp. 122–136. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-33386-6_11CrossRefzbMATHGoogle Scholar
  10. 10.
    Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329–363 (1994). http://www.sciencedirect.com/science/article/pii/0304397594902429MathSciNetCrossRefGoogle Scholar
  11. 11.
    Kupferman, O., Vardi, M.: Synthesis with incomplete informatio. In: 2nd International Conference on Temporal Logic, pp. 91–106. Manchester (1997)Google Scholar
  12. 12.
    Lazić, R., Nowak, D.: A unifying approach to data-independence. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 581–596. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-44618-4_41CrossRefGoogle Scholar
  13. 13.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, pp. 179–190. ACM Press, Austin, Texas, USA, January 11–13 (1989).  https://doi.org/10.1145/75277.75293
  14. 14.
    Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. In: Proceedings of the 13th POPL, pp. 184–193. ACM, New York, NY, USA (1986).  https://doi.org/10.1145/512644.512661

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Ayrat Khalimov
    • 1
    Email author
  • Benedikt Maderbacher
    • 2
  • Roderick Bloem
    • 2
  1. 1.The Hebrew UniversityJerusalemIsrael
  2. 2.Graz University of TechnologyGrazAustria

Personalised recommendations