Document Open Access Logo

The Complexity of Transducer Synthesis from Multi-Sequential Specifications

Authors Léo Exibard, Emmanuel Filiot, Ismaël Jecker

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2018.46.pdf
  • Filesize: 0.52 MB
  • 16 pages

Document Identifiers

Author Details

Léo Exibard
  • Aix-Marseille Université, Marseille, France , Université libre de Bruxelles, Brussels, Belgium
Emmanuel Filiot
  • Université libre de Bruxelles, Brussels, Belgium
Ismaël Jecker
  • Université libre de Bruxelles, Brussels, Belgium

Funding

  • Exibard, Léo: L. Exibard is a PhD student funded by a FRIA fellowship from the F.R.S.-FNRS.
  • Filiot, Emmanuel: E. Filiot is a research associate of F.R.S.- FNRS. He is supported by the ARC Project Transform Fédération Wallonie-Bruxelles and the FNRS CDR project J013116F.
  • Jecker, Ismaël: I. Jecker is an "aspirant FNRS" PhD student, funded by the F.R.S.-FNRS.

Cite AsGet BibTex

Léo Exibard, Emmanuel Filiot, and Ismaël Jecker. The Complexity of Transducer Synthesis from Multi-Sequential Specifications. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 46:1-46:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.MFCS.2018.46

Abstract

The transducer synthesis problem on finite words asks, given a specification S subseteq I x O, where I and O are sets of finite words, whether there exists an implementation f: I - > O which (1) fulfils the specification, i.e., (i,f(i))in S for all i in I, and (2) can be defined by some input-deterministic (aka sequential) transducer T_f. If such an implementation f exists, the procedure should also output T_f. The realisability problem is the corresponding decision problem. For specifications given by synchronous transducers (which read and write alternately one symbol), this is the finite variant of the classical synthesis problem on omega-words, solved by Büchi and Landweber in 1969, and the realisability problem is known to be ExpTime-c in both finite and omega-word settings. For specifications given by asynchronous transducers (which can write a batch of symbols, or none, in a single step), the realisability problem is known to be undecidable. We consider here the class of multi-sequential specifications, defined as finite unions of sequential transducers over possibly incomparable domains. We provide optimal decision procedures for the realisability problem in both the synchronous and asynchronous setting, showing that it is PSpace-c. Moreover, whenever the specification is realisable, we expose the construction of a sequential transducer that realises it and has a size that is doubly exponential, which we prove to be optimal.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Transducers
Keywords
  • Transducers
  • Multi-Sequentiality
  • Synthesis

Metrics

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

References

  1. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672-713, 2002. URL: http://dx.doi.org/10.1145/585265.585270.
  2. Marie-Pierre Béal, Olivier Carton, Christophe Prieur, and Jacques Sakarovitch. Squaring transducers: an efficient procedure for deciding functionality and sequentiality. Theoretical Computer Science, 292(1):45-63, 2003. Google Scholar
  3. Jean Berstel and Luc Boasson. Transductions and context-free languages. Ed. Teubner, pages 1-278, 1979. Google Scholar
  4. Arnaud Carayol and Christof Löding. Uniformization in Automata Theory. In Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science Nancy, July 19-26, 2011, pages 153-178, London, 2014. College Publications. Google Scholar
  5. Krishnendu Chatterjee, Thomas A. Henzinger, and Nir Piterman. Strategy logic. Information and Computation, 208(6):677-693, 2010. URL: http://dx.doi.org/10.1016/j.ic.2009.07.004.
  6. Christian Choffrut and Marcel Paul Schützenberger. Décomposition de fonctions rationnelles. In 2nd Annual Symposium on Theoretical Aspects of Computer Science, STACS, pages 213-226, 1986. Google Scholar
  7. Church, Alonzo. Logic, arithmetic and automata. In International Congress of Mathematics, pages 23-35, Stockholm, 1962. Google Scholar
  8. Laure Daviaud, Ismaël Jecker, Pierre-Alain Reynier, and Didier Villevalois. Degree of sequentiality of weighted automata. In Javier Esparza and Andrzej S. Murawski, editors, Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2017, Uppsala, Sweden, April 22-29, pages 215-230. Springer Berlin Heidelberg, 2017. URL: http://dx.doi.org/10.1007/978-3-662-54458-7_13.
  9. Luca de Alfaro, Thomas A. Henzinger, and Rupak Majumdar. Symbolic algorithms for infinite-state games. In Proceedings of the 12th International Conference in Concurrency Theory, CONCUR 2001, Aalborg, Denmark, August 20-25, pages 536-550, 2001. URL: http://dx.doi.org/10.1007/3-540-44685-0_36.
  10. Rüdiger Ehlers. Symbolic bounded synthesis. In Proceedings of the 22nd International Conference on Computer Aided Verification, CAV 2010, Edinburgh, UK, July 15-19, volume 6174 of Lecture Notes in Computer Science, pages 365-379. Springer, 2010. Google Scholar
  11. Samuel Eilenberg. Automata, Languages, and Machines. Academic Press, 1974. Google Scholar
  12. Emmanuel Filiot, Ismaël Jecker, Christof Löding, and Sarah Winter. On equivalence and uniformisation problems for finite transducers. In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, Rome, Italy, pages 125:1-125:14, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.125.
  13. Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin. Exploiting structure in LTL synthesis. International Journal on Software Tools for Technology Transfer, 2011. Google Scholar
  14. Emmanuel Filiot, Naiyong Jin, and Jean-François Raskin. Antichains and compositional algorithms for LTL synthesis. Formal Methods in System Design, 39(3):261-296, 2011. Google Scholar
  15. Wladimir Fridman, Christof Löding, and Martin Zimmermann. Degrees of lookahead in context-free infinite games. In Computer Science Logic, 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, September 12-15, 2011, Bergen, Norway, Proceedings, pages 264-276, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2011.264.
  16. Eitan M. Gurari and Oscar H. Ibarra. The complexity of decision problems for finite-turn multicounter machines. Journal of Computer and System Science, 22(2):220-229, 1981. URL: http://dx.doi.org/10.1016/0022-0000(81)90028-3.
  17. Michael Holtmann, Lukasz Kaiser, and Wolfgang Thomas. Degrees of lookahead in regular infinite games. In C.-H. Luke Ong, editor, Proceedings of the 13th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2010, Paphos, Cyprus, March 20-28, volume 6014 of Lecture Notes in Computer Science, pages 252-266. Springer, 2010. Google Scholar
  18. Swen Jacobs, Roderick Bloem, Romain Brenguier, Rüdiger Ehlers, Timotheus Hell, Robert Könighofer, Guillermo A. Pérez, Jean-François Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, and Adam Walker. The first reactive synthesis competition (SYNTCOMP 2014). STTT, 19(3):367-390, 2017. URL: http://dx.doi.org/10.1007/s10009-016-0416-3.
  19. Ismaël Jecker and Emmanuel Filiot. Multi-sequential word relations. In Proceedings of the 19th International Conference on Developments in Language Theory, DLT 2015, Liverpool, UK, July 27-30, pages 288-299, 2015. URL: http://dx.doi.org/10.1007/978-3-319-21500-6_23.
  20. B. Jobstmann, S. Galler, M. Weiglhofer, and R. Bloem. Anzu: A tool for property synthesis. In Computer Aided Verification, CAV, pages 258-262, 2007. Google Scholar
  21. J.R. Büchi and L.H. Landweber. Solving sequential conditions finite-state strategies. Transactions of the American Mathematical Society, 138:295-311, 1969. Google Scholar
  22. Felix Klein and Martin Zimmermann. How much lookahead is needed to win infinite games? Logical Methods in Computer Science, 12(3), 2016. URL: http://dx.doi.org/10.2168/LMCS-12(3:4)2016.
  23. Felix Klein and Martin Zimmermann. Prompt delay. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016, December 13-15, Chennai, India, pages 43:1-43:14, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2016.43.
  24. Kojiro Kobayashi. Classification of formal languages by functional binary transductions. Information and Control, 15(1):95-109, 1969. Google Scholar
  25. Dexter Kozen. Lower bounds for natural proof systems. In FOCS, pages 254-266. IEEE Computer Society, 1977. URL: http://dblp.uni-trier.de/db/conf/focs/focs77.html#Kozen77.
  26. Yoad Lustig and Moshe Y. Vardi. Synthesis from component libraries. STTT, 15(5-6):603-618, 2013. Google Scholar
  27. 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
  28. Sven Schewe and Bernd Finkbeiner. Bounded synthesis. In Automated Technology for Verification and Analysis, volume 4762 of Lecture Notes in Computer Science, pages 474-488. Springer Berlin Heidelberg, 2007. Google Scholar
  29. Wolfgang Thomas. Church’s problem and a tour through automata theory. In Pillars of Computer Science, Essays Dedicated to Boris (Boaz) Trakhtenbrot on the Occasion of His 85th Birthday, volume 4800 of Lecture Notes in Computer Science, pages 635-655. Springer, 2008. Google Scholar
  30. Martin Zimmermann. Delay games with WMSO+U winning conditions. RAIRO - Theoretical Informatics and Applications, 50(2):145-165, 2016. URL: http://dx.doi.org/10.1051/ita/2016018.
  31. Martin Zimmermann. Finite-state strategies in delay games. In Proceedings 8th International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2017, Roma, Italy, 20-22 September, pages 151-165, 2017. URL: http://dx.doi.org/10.4204/EPTCS.256.11.
  32. Martin Zimmermann. Games with costs and delays. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, pages 1-12, 2017. URL: http://dx.doi.org/10.1109/LICS.2017.8005125.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact