Register-Bounded Synthesis

Authors Ayrat Khalimov, Orna Kupferman



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.25.pdf
  • Filesize: 0.48 MB
  • 16 pages

Document Identifiers

Author Details

Ayrat Khalimov
  • School of Computer Science and Engineering, The Hebrew University, Jerusalem, Israel
Orna Kupferman
  • School of Computer Science and Engineering, The Hebrew University, Jerusalem, Israel

Cite AsGet BibTex

Ayrat Khalimov and Orna Kupferman. Register-Bounded Synthesis. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.25

Abstract

Traditional synthesis algorithms return, given a specification over finite sets of input and output Boolean variables, a finite-state transducer all whose computations satisfy the specification. Many real-life systems have an infinite state space. In particular, behaviors of systems with a finite control yet variables that range over infinite domains, are specified by automata with infinite alphabets. A register automaton has a finite set of registers, and its transitions are based on a comparison of the letters in the input with these stored in its registers. Unfortunately, reasoning about register automata is complex. In particular, the synthesis problem for specifications given by register automata, where the goal is to generate correct register transducers, is undecidable. We study the synthesis problem for systems with a bounded number of registers. Formally, the register-bounded realizability problem is to decide, given a specification register automaton A over infinite input and output alphabets and numbers k_s and k_e of registers, whether there is a system transducer T with at most k_s registers such that for all environment transducers T' with at most k_e registers, the computation T|T', generated by the interaction of T with T', satisfies the specification A. The register-bounded synthesis problem is to construct such a transducer T, if exists. The bounded setting captures better real-life scenarios where bounds on the systems and/or its environment are known. In addition, the bounds are the key to new synthesis algorithms, and, as recently shown in [A. Khalimov et al., 2018], they lead to decidability. Our contributions include a stronger specification formalism (universal register parity automata), simpler algorithms, which enable a clean complexity analysis, a study of settings in which both the system and the environment are bounded, and a study of the theoretical aspects of the setting; in particular, the differences among a fixed, finite, and infinite number of registers, and the determinacy of the corresponding games.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Synthesis
  • Register Automata
  • Register Transducers

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. R. Bloem, K. Chatterjee, and B. Jobstmann. Graph Games and Reactive Synthesis. In Handbook of Model Checking., pages 921-962. Springer, 2018. Google Scholar
  2. M. Bojańczyk, A. Muscholl, T. Schwentick, and L. Segoufin. Two-variable logic on data trees and XML reasoning. Journal of the ACM, 56(3):1-48, 2009. Google Scholar
  3. M. Bojanczyk, A. Muscholl, T. Schwentick, L. Segoufin, and C. David. Two-Variable Logic on Words with Data. In Proc. 21st IEEE Symp. on Logic in Computer Science, pages 7-16, 2006. Google Scholar
  4. A. Bouajjani, P. Habermehl, Y. Jurski, and M. Sighireanu. Rewriting systems with data. In FCT, pages 1-22, 2007. Google Scholar
  5. A. Bouajjani, P. Habermehl, and R R. Mayr. Automatic verification of recursive procedures with one integer parameter. Theoretical Computer Science, 295:85-106, 2003. Google Scholar
  6. M. Brambilla, S. Ceri, S. Comai, P. Fraternali, and I. Manolescu. Specification and Design of Workflow-Driven Hypertexts. J. Web Eng., 1(2):163-182, 2003. Google Scholar
  7. C.S. Calude, S. Jain, B. Khoussainov, W. Li, and F. Stephan. Deciding parity games in quasipolynomial time. In Proc. 49th ACM Symp. on Theory of Computing, pages 252-263, 2017. Google Scholar
  8. S. Ceri, P. Fraternali, A. Bongio, M. Brambilla, S. Comai, and M. Matera. Designing Data-Intensive Web Applications. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2002. Google Scholar
  9. K. Chatterjee, T. Henzinger, and B. Jobstmann. Environment Assumptions for Synthesis. In Proc. 19th Int. Conf. on Concurrency Theory, volume 5201 of Lecture Notes in Computer Science, pages 147-161. Springer, 2008. Google Scholar
  10. A. Church. Logic, arithmetics, and automata. In Proc. Int. Congress of Mathematicians, 1962, pages 23-35. Institut Mittag-Leffler, 1963. Google Scholar
  11. G. Delzanno, A. Sangnier, and R. Traverso. Parameterized Verification of Broadcast Networks of Register Automata. In P. A. Abdulla and I. Potapov, editors, Reachability Problems, pages 109-121, Berlin, Heidelberg, 2013. Springer. Google Scholar
  12. S. Demri and R. Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3):16:1-16:30, 2009. Google Scholar
  13. R. Ehlers. Symbolic bounded synthesis. In Proc. 22nd Int. Conf. on Computer Aided Verification, volume 6174 of Lecture Notes in Computer Science, pages 365-379. Springer, 2010. Google Scholar
  14. R. Ehlers, S. Seshia, and H. Kress-Gazit. Synthesis with Identifiers. In Proc. 15th Int. Conf. on Verification, Model Checking, and Abstract Interpretation, volume 8318 of Lecture Notes in Computer Science, pages 415-433. Springer, 2014. Google Scholar
  15. L. Exibard, E. Filiot, and P-A. Reynier. Synthesis of Data Word Transducers. In Proc. 30th Int. Conf. on Concurrency Theory, 2019. Google Scholar
  16. E. Filiot, N. Jin, and J.-F. Raskin. An Antichain Algorithm for LTL Realizability. In Proc. 21st Int. Conf. on Computer Aided Verification, volume 5643, pages 263-277, 2009. Google Scholar
  17. B. Finkbeiner, F. Klein, R. Piskac, and M. Santolucito. Temporal Stream Logic: Synthesis beyond the Bools. In Proc. 31st Int. Conf. on Computer Aided Verification, 2019. Google Scholar
  18. O. Grumberg, O. Kupferman, and S. Sheinvald. Variable Automata over Infinite Alphabets. In Proc. 4th Int. Conf. on Language and Automata Theory and Applications, volume 6031 of Lecture Notes in Computer Science, pages 561-572. Springer, 2010. Google Scholar
  19. O. Grumberg, O. Kupferman, and S. Sheinvald. An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications. In 11th Int. Symp. on Automated Technology for Verification and Analysis, pages 397-411, 2013. Google Scholar
  20. R. Hojati, D.L. Dill, and R.K. Brayton. Verifying linear temporal properties of data insensitive controllers using finite instantiations. In Hardware Description Languages and their Applications, pages 60-73. Springer, 1997. Google Scholar
  21. M. Kaminski and N. Francez. Finite-memory automata. Theoretical Computer Science, 134(2):329-363, 1994. Google Scholar
  22. M. Kaminski and D. Zeitlin. Extending finite-memory automata with non-deterministic reassignment. In AFL, pages 195-207, 2008. Google Scholar
  23. A. Khalimov and O. Kupferman. Register-bounded Synthesis, 2019. Full version, available on the author’s personal pages. Google Scholar
  24. A. Khalimov, B. Maderbacher, and R. Bloem. Bounded Synthesis of Register Transducers. In 16th Int. Symp. on Automated Technology for Verification and Analysis, volume 11138 of Lecture Notes in Computer Science, pages 494-510. Springer, 2018. Google Scholar
  25. O. Kupferman. Recent Challenges and Ideas in Temporal Synthesis. In Proc. 38th International Conference on Current Trends in Theory and Practice of Computer Science, volume 7147 of Lecture Notes in Computer Science, pages 88-98. Springer, 2012. Google Scholar
  26. O. Kupferman, Y. Lustig, M.Y. Vardi, and M. Yannakakis. Temporal Synthesis for Bounded Systems and Environments. In Proc. 28th Symp. on Theoretical Aspects of Computer Science, pages 615-626, 2011. Google Scholar
  27. R. Lazić and D. Nowak. A Unifying Approach to Data-Independence. In Proc. 11th Int. Conf. on Concurrency Theory, pages 581-596. Springer Berlin Heidelberg, 2000. Google Scholar
  28. F. Neven, T. Schwentick, and V. Vianu. Towards Regular Languages over Infinite Alphabets. In 26th Int. Symp. on Mathematical Foundations of Computer Science, pages 560-572. Springer-Verlag, 2001. Google Scholar
  29. N. Piterman. From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata. In Proc. 21st IEEE Symp. on Logic in Computer Science, pages 255-264. IEEE press, 2006. Google Scholar
  30. A. Pnueli and R. Rosner. On the Synthesis of a Reactive Module. In Proc. 16th ACM Symp. on Principles of Programming Languages, pages 179-190, 1989. Google Scholar
  31. S. Schewe and B. Finkbeiner. Bounded Synthesis. In 5th Int. Symp. on Automated Technology for Verification and Analysis, volume 4762 of Lecture Notes in Computer Science, pages 474-488. Springer, 2007. Google Scholar
  32. S. Schewe and T. Varghese. Determinising Parity Automata. In 39th Int. Symp. on Mathematical Foundations of Computer Science, volume 8634 of Lecture Notes in Computer Science, pages 486-498. Springer, 2014. Google Scholar
  33. Y. Shemesh and N.: Francez. Finite-state unification automata and relational languages. Information and Computation, 114:192-213, 1994. Google Scholar
  34. T. Tan. Pebble Automata for Data Languages: Separation, Decidability, and Undecidability. PhD thesis, Technion - Computer Science Department, 2009. Google Scholar
  35. N. Tzevelekos. Fresh-register Automata. In Proc. 38th ACM Symp. on Principles of Programming Languages, pages 295-306, New York, NY, USA, 2011. ACM. Google Scholar
  36. V. Vianu. Automatic verification of database-driven systems: a new frontier. In ICDT '09, pages 1-13, 2009. Google Scholar
  37. P. Wolper. Expressing Interesting Properties of Programs in Propositional Temporal Logic. In Proc. 13th ACM Symp. on Principles of Programming Languages, pages 184-192, 1986. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail