Bidirectional Nested Weighted Automata

Authors Krishnendu Chatterjee, Thomas A. Henzinger, Jan Otop



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.5.pdf
  • Filesize: 0.54 MB
  • 16 pages

Document Identifiers

Author Details

Krishnendu Chatterjee
Thomas A. Henzinger
Jan Otop

Cite AsGet BibTex

Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Bidirectional Nested Weighted Automata. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CONCUR.2017.5

Abstract

Nested weighted automata (NWA) present a robust and convenient automata-theoretic formalism for quantitative specifications. Previous works have considered NWA that processed input words only in the forward direction. It is natural to allow the automata to process input words backwards as well, for example, to measure the maximal or average time between a response and the preceding request. We therefore introduce and study bidirectional NWA that can process input words in both directions. First, we show that bidirectional NWA can express interesting quantitative properties that are not expressible by forward-only NWA. Second, for the fundamental decision problems of emptiness and universality, we establish decidability and complexity results for the new framework which match the best-known results for the special case of forward-only NWA. Thus, for NWA, the increased expressiveness of bidirectionality is achieved at no additional computational complexity. This is in stark contrast to the unweighted case, where bidirectional finite automata are no more expressive but exponentially more succinct than their forward-only counterparts.
Keywords
  • weighted automata
  • nested weighted automata
  • complexity
  • bidirectional

Metrics

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

References

  1. Shaull Almagor, Udi Boker, and Orna Kupferman. Discounting in LTL. In TACAS, 2014, pages 424-439, 2014. Google Scholar
  2. Shaull Almagor, Udi Boker, and Orna Kupferman. Formally reasoning about quality. J. ACM, 63(3):24:1-24:56, 2016. URL: http://dx.doi.org/10.1145/2875421.
  3. Rajeev Alur, Loris D'Antoni, Jyotirmoy V. Deshmukh, Mukund Raghothaman, and Yifei Yuan. Regular functions and cost register automata. In LICS 2013, pages 13-22, 2013. Google Scholar
  4. Mikołaj Bojańczyk and Thomas Colcombet. Bounds in w-regularity. In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 285-296, 2006. URL: http://dx.doi.org/10.1109/LICS.2006.17.
  5. Udi Boker, Krishnendu Chatterjee, Thomas A. Henzinger, and Orna Kupferman. Temporal specifications with accumulative values. ACM TOCL, 15(4):27:1-27:25, 2014. Google Scholar
  6. Benedikt Bollig, Paul Gastin, Benjamin Monmege, and Marc Zeitoun. Pebble weighted automata and transitive closure logics. In ICALP 2010, Part II, pages 587-598. Springer, 2010. Google Scholar
  7. Patricia Bouyer, Nicolas Markey, and Raj Mohan Matteplackel. Averaging in LTL. In CONCUR 2014, pages 266-280, 2014. Google Scholar
  8. Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim Guldstrand Larsen, and Simon Laursen. Average-energy games. In GandALF 2015., pages 1-15, 2015. URL: http://dx.doi.org/10.4204/EPTCS.193.1.
  9. Krishnendu Chatterjee, Laurent Doyen, Herbert Edelsbrunner, Thomas A. Henzinger, and Philippe Rannou. Mean-payoff automaton expressions. In CONCUR, pages 269-283, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15375-4_19.
  10. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Alternating weighted automata. In FCT'09, pages 3-13. Springer, 2009. Google Scholar
  11. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Expressiveness and closure properties for quantitative languages. LMCS, 6(3), 2010. Google Scholar
  12. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. ACM TOCL, 11(4):23, 2010. Google Scholar
  13. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Nested weighted automata. In LICS 2015, pages 725-737, 2015. Google Scholar
  14. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Nested weighted limit-average automata of bounded width. In MFCS 2016, pages 24:1-24:14, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.MFCS.2016.24.
  15. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Quantitative automata under probabilistic semantics. In LICS 2016, pages 76-85, 2016. URL: http://dx.doi.org/10.1145/2933575.2933588.
  16. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Quantitative monitor automata. In SAS 2016, pages 23-38, 2016. URL: http://dx.doi.org/10.1007/978-3-662-53413-7_2.
  17. Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Bidirectional nested weighted automata. CoRR, abs/1706.08316, 2017. URL: http://arxiv.org/abs/1706.08316.
  18. Krishnendu Chatterjee and Vinayak S. Prabhu. Quantitative temporal simulation and refinement distances for timed systems. IEEE Trans. Automat. Contr., 60(9):2291-2306, 2015. URL: http://dx.doi.org/10.1109/TAC.2015.2404612.
  19. Manfred Droste, Werner Kuich, and Heiko Vogler. Handbook of Weighted Automata. Springer, 1st edition, 2009. Google Scholar
  20. Manfred Droste and George Rahonis. Weighted automata and weighted logics on infinite words. In DLT 2006, pages 49-58, 2006. Google Scholar
  21. Filip Mazowiecki and Cristian Riveros. Copyless cost-register automata: Structure, expressiveness, and closure properties. In STACS, 2016, pages 53:1-53:13, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2016.53.
  22. Mehryar Mohri. Semiring frameworks and algorithms for shortest-distance problems. J. Aut. Lang. &Comb., 7(3):321-350, 2002. 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