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)


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.


  1. 1.
    Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016).
  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). 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). 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). 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). 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). 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). Scholar
  10. 10.
    Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329–363 (1994). 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). 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).
  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).

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