Synthesis of Data Word Transducers

Authors Léo Exibard, Emmanuel Filiot, Pierre-Alain Reynier



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.24.pdf
  • Filesize: 0.53 MB
  • 15 pages

Document Identifiers

Author Details

Léo Exibard
  • Aix Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France
  • Université libre de Bruxelles, Brussels, Belgium
Emmanuel Filiot
  • Université libre de Bruxelles, Brussels, Belgium
Pierre-Alain Reynier
  • Aix Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France

Acknowledgements

We would like to thank Ayrat Khalimov for his remarks and suggestions, which helped improve the quality of the paper.

Cite AsGet BibTex

Léo Exibard, Emmanuel Filiot, and Pierre-Alain Reynier. Synthesis of Data Word Transducers. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.24

Abstract

In reactive synthesis, the goal is to automatically generate an implementation from a specification of the reactive and non-terminating input/output behaviours of a system. Specifications are usually modelled as logical formulae or automata over infinite sequences of signals (omega-words), while implementations are represented as transducers. In the classical setting, the set of signals is assumed to be finite. In this paper, we consider data omega-words instead, i.e., words over an infinite alphabet. In this context, we study specifications and implementations respectively given as automata and transducers extended with a finite set of registers. We consider different instances, depending on whether the specification is nondeterministic, universal or deterministic, and depending on whether the number of registers of the implementation is given or not. In the unbounded setting, we show undecidability for both universal and non-deterministic specifications, while decidability is recovered in the deterministic case. In the bounded setting, undecidability still holds for non-deterministic specifications, but can be recovered by disallowing tests over input data. The generic technique we use to show the latter result allows us to reprove some known result, namely decidability of bounded synthesis for universal specifications.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Transducers
Keywords
  • Register Automata
  • Synthesis
  • Data words
  • Transducers

Metrics

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

References

  1. Roderick Bloem, Krishnendu Chatterjee, and Barbara Jobstmann. Graph Games and Reactive Synthesis, pages 921-962. Springer International Publishing, Cham, 2018. Google Scholar
  2. Mikołaj Bojańczyk, Anca Muscholl, Thomas Schwentick, Luc Segoufin, and Claire David. Two-Variable Logic on Words with Data. In Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), pages 7-16. ACM, 2006. URL: https://doi.org/10.1109/LICS.2006.51.
  3. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding Parity Games in Quasipolynomial Time. In Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing (STOC 2017), pages 252-263. ACM, 2017. URL: https://doi.org/10.1145/3055399.3055409.
  4. Luc Dartois, Emmanuel Filiot, and Nathan Lhote. Logics for Word Transductions with Synthesis. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), pages 295-304. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209181.
  5. Antoine Durand-Gasselin and Peter Habermehl. Regular Transformations of Data Words Through Origin Information. In Proceedings of the 19th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2016), volume 9634 of Lecture Notes in Computer Science, pages 285-300. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_17.
  6. Rüdiger Ehlers, Sanjit A. Seshia, and Hadas Kress-Gazit. Synthesis with Identifiers. In Proceedings of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2014), volume 8318 of Lecture Notes in Computer Science, pages 415-433. Springer, 2014. URL: https://doi.org/10.1007/978-3-642-54013-4_23.
  7. Léo Exibard, Emmanuel Filiot, and Pierre-Alain Reynier. Synthesis of Data Word Transducers. CoRR, abs/1905.03538, 2019. URL: http://arxiv.org/abs/1905.03538.
  8. Diego Figueira and M. Praveen. Playing with Repetitions in Data Words Using Energy Games. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), pages 404-413. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209154.
  9. J.R. Büchi and L.H. Landweber. Solving Sequential Conditions by Finite-State Strategies. Transactions of the American Mathematical Society, 138:295-311, 1969. Google Scholar
  10. Michael Kaminski and Nissim Francez. Finite-memory Automata. Theor. Comput. Sci., 134(2):329-363, 1994. URL: https://doi.org/10.1016/0304-3975(94)90242-9.
  11. Ayrat Khalimov and Orna Kupferman. Register Bounded Synthesis. In Proceedings of the 30th International Conference on Concurrency Theory (CONCUR 2019), 2019. To appear. Google Scholar
  12. Ayrat Khalimov, Benedikt Maderbacher, and Roderick Bloem. Bounded Synthesis of Register Transducers. In Proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018), volume 11138 of Lecture Notes in Computer Science, pages 494-510. Springer, 2018. Google Scholar
  13. Andrzej S. Murawski, Steven J. Ramsay, and Nikos Tzevelekos. Bisimilarity in Fresh-Register Automata. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015), pages 156-167. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.24.
  14. Frank Neven, Thomas Schwentick, and Victor Vianu. Finite State Machines for Strings over Infinite Alphabets. ACM Trans. Comput. Logic, 5(3):403-435, 2004. URL: https://doi.org/10.1145/1013560.1013562.
  15. Nir Piterman. From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata. Logical Methods in Computer Science, 3(3), 2007. Google Scholar
  16. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In ACM Symposium on Principles of Programming Languages, POPL. ACM, 1989. Google Scholar
  17. Thomas Schwentick and Thomas Zeume. Two-Variable Logic with Two Order Relations. Logical Methods in Computer Science, 8(1), 2012. URL: https://doi.org/10.2168/LMCS-8(1:15)2012.
  18. Luc Segoufin. Automata and Logics for Words and Trees over an Infinite Alphabet. In Proceedings of the 15th Annual Conference of the EACSL on Computer Science Logic (CSL 2006), volume 4207 of Lecture Notes in Computer Science, pages 41-57. Springer, 2006. URL: https://doi.org/10.1007/11874683_3.
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