A Translation of Weighted LTL Formulas to Weighted Buchi Automata over omega-valuation Monoids

Published in Volume XXXI, Issue 2, 2021, pages 223-292, doi: 10.7561/SACS.2021.2.223

Authors: E. Mandrali

Abstract

In this paper we introduce a weighted LTL over product omega-valuation monoids that satisfy specific properties. We also introduce weighted generalized Buchi automata with epsilon-transitions, as well as weighted Buchi automata with epsilon-transitions over product omega-valuation monoids and prove that these two models are expressively equivalent and also equivalent to weighted Buchi automata already introduced in the literature. We prove that every formula of a syntactic fragment of our logic can be effectively translated to a weighted generalized Buchi automaton with epsilon-transitions. For generalized product omega-valuation monoids that satisfy specific properties we define a weighted LTL, weighted generalized Buchi automata with epsilon-transitions, and weighted Buchi automata with epsilon-transitions, and we prove the aforementioned results for generalized product omega-valuation monoids as well. The translation of weighted LTL formulas to weighted generalized Buchi automata with epsilon-transitions is now obtained for a restricted syntactical fragment of the logic.

Full Text (PDF)

References

[1] Marianne Akian, Stephane Gaubert, and Alexander Guterman. Tropical and idempotent mathematics. In Grigorii Lazarevich Litvinov and Sergei Sergeev, editors, International Workshop Tropical-07, Tropical and Idempotent Mathematics,, volume 495 of Contemporary Mathematics, pages 1-38. American Mathematical Society, 2009. doi:10.1090/conm/495/09689.

[2] Shaull Almagor, Udi Boker, and Orna Kupferman. Discounting in LTL. In Erika Abraham and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems – 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, volume 8413 of Lecture Notes in Computer Science, pages 424-439. Springer, 2014. doi:10.1007/978-3-642-54862-8\_37.

[3] Arindam Chakrabarti, Krishnendu Chatterjee, Thomas A. Henzinger, Orna Kupferman, and Rupak Majumdar. Verifying quantitative properties using bound functions. In Dominique Borrione and Wolfgang J. Paul, editors, Correct Hardware Design and Verification Methods, 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, volume 3725 of Lecture Notes in Computer Science, pages 50-64. Springer, 2005. doi:10.1007/11560548\_7.

[4] Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, and Marielle Stoelinga. Resource interfaces. In Rajeev Alur and Insup Lee, editors, Embedded Software, Third International Conference, EMSOFT 2003, volume 2855 of Lecture Notes in Computer Science, pages 117-133. Springer, 2003. doi:10.1007/978-3-540-45212-6\_9.

[5] Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. In Michael Kaminski and Simone Martini, editors, Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, volume 5213 of Lecture Notes in Computer Science, pages 385-400. Springer, 2008. doi:10.1007/978-3-540-87531-4\_28.

[6] Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Alternating weighted automata. In Miroslaw Kutylowski, Witold Charatonik, and Maciej Gebala, editors, Fundamentals of Computation Theory, 17th International Symposium, FCT 2009, volume 5699 of Lecture Notes in Computer Science, pages 3-13. Springer, 2009. doi:10.1007/978-3-642-03409-1\_2.

[7] Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Probabilistic weighted automata. In Mario Bravetti and Gianluigi Zavattaro, editors, Concurrency Theory, 20th International Conference, CONCUR 2009, volume 5710 of Lecture Notes in Computer Science, pages 244-258. Springer, 2009. doi:10.1007/978-3-642-04081-8\_17.

[8] Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Expressiveness and closure properties for quantitative languages. Logical Methods in Computer Science, 6(3), 2010. doi:10.2168/lmcs-6(3:10)2010.

[9] Stephane Demri and Paul Gastin. Specification and verification using temporal logics. In Deepak D’Souza and Priti Shankar, editors, Modern Applications of Automata Theory, volume 2 of IISc Research Monographs Series, pages 457-494. World Scientic, 2012. doi:10.1142/9789814271059\_0015.

[10] Manfred Droste and Paul Gastin. Weighted automata and weighted logics. Theoretical Computer Science, 380(1-2):69-86, 2007. doi:10.1016/j.tcs.2007.02.055.

[11] Manfred Droste, Werner Kuich, and Heiko Vogler, editors. Handbook of Weighted Automata. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Berlin, Heidelberg, 2009. doi:10.1007/978-3-642-01492-5.

[12] Manfred Droste and Dietrich Kuske. Skew and infinitary formal power series. Theoretical Computer Science, 366(3):199-227, 2006. doi:10.1016/j.tcs.2006.08.024.

[13] Manfred Droste and Ingmar Meinecke. Weighted automata and weighted MSO logics for average and long-time behaviors. Information and Computation, 220:44-59, 2012. doi:10.1016/j.ic.2012.10.001.

[14] Manfred Droste and Heiko Vogler. Weighted automata and multi-valued logics over arbitrary bounded lattices. Theoretical Computer Science, 418:14-36, 2012. doi:10.1016/j.tcs.2011.11.008.

[15] Zoltan Esik and Werner Kuich. A semiring-semimodule generalization of omega-regular languages I. Journal of Automata, Languages and Combinatorics, 10(2/3):203-242, 2005. doi:10.25596/jalc-2005-203.

[16] Zoltan Esik and Werner Kuich. On iteration semiring-semimodule pairs. Semigroup Forum, 75:129-159, 2007. doi:10.1007/s00233-007-0709-7.

[17] Marco Faella, Axel Legay, and Marielle Stoelinga. Model checking quantitative linear time logic. Electronic Notes in Theoretical Computer Science, 220(3):61-77, 2008. doi:10.1016/j.entcs.2008.11.019.

[18] Jeremy Gunawardena. An introduction to idempotency, page 1-49. Publications of the Newton Institute. Cambridge University Press, 1998. doi:10.1017/CBO9780511662508.003.

[19] Orna Kupferman and Yoad Lustig. Lattice automata. In Byron Cook and Andreas Podelski, editors, Verification, Model Checking, and Abstract Interpretation, 8th International Conference, VMCAI 2007, volume 4349 of Lecture Notes in Computer Science, pages 199-213. Springer, 2007. doi:10.1007/978-3-540-69738-1\_14.

[20] Eleni Mandrali. Weighted LTL with discounting. In Nelma Moreira and Rogerio Reis, editors, Implementation and Application of Automata – 17th International Conference, CIAA 2012, volume 7381 of Lecture Notes in Computer Science, pages 353-360. Springer, 2012. doi:10. 1007/978-3-642-31606-7\_32.

[21] Eleni Mandrali. Weighted computability with discounting. Dissertation’s thesis, Aristotle University of Thessaloniki, 2013. doi:10.12681/eadd/35478.

[22] Eleni Mandrali and George Rahonis. On weighted first-order logics with discounting. Acta Informatica, 51(2):61-106, 2014. doi:10.1007/s00236-013-0193-3.

[23] Eleni Mandrali and George Rahonis. Weighted first-order logics over semirings. Acta Cybernetica, 22(2):435-483, 2015. doi:10.14232/actacyb.22.2.2015.13.

[24] Ingmar Meinecke. Valuations of weighted automata: Doing it in a rational way. In Werner Kuich and George Rahonis, editors, Algebraic Foundations in Computer Science – Essays Dedicated to Symeon Bozapalidis on the Occasion of His Retirement, volume 7020 of Lecture Notes in Computer Science, pages 309-346. Springer, 2011. doi: 10.1007/978-3-642-24897-9\_14.

[25] Gethin Norman and David Parker. Quantitative verification: Formal guarantees for timeliness, reliability and performance. Technical report, The London Mathematical Society and the Smith Institute, 2014.

[26] Marcel Paul Schutzenberger. On the definition of a family of automata. Information and Control, 4(2-3):245{270, 1961. doi:10.1016/S0019-9958(61)80020-X.

[27] Moshe Y. Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification (preliminary report). In Proceedings of the Symposium on Logic in Computer Science (LICS’86), pages 332-344. IEEE Computer Society, 1986.

[28] Moshe Y. Vardi and Pierre Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1-37, 1994. doi:10.1006/inco.1994.1092.

[29] Sigal Weiner, Matan Hasson, Orna Kupferman, Eyal Pery, and Zohar Shevach. Weighted safety. In Dang Van Hung and Mizuhito Ogawa, editors, Automated Technology for Verification and Analysis – 11th International Symposium, ATVA 2013, volume 8172 of Lecture Notes in Computer Science, pages 133-147. Springer, 2013. doi:10.1007/978-3-319-02444-8\_11.

[30] Pierre Wolper. Constructing automata from temporal logic formulas: A tutorial. In Ed Brinksma, Holger Hermanns, and Joost-Pieter Katoen, editors, Lectures on Formal Methods and Performance Analysis, First EEF/Euro Summer School on Trends in Computer Science, volume 2090 of Lecture Notes in Computer Science, pages 261-277. Springer, 2000. doi:10.1007/3-540-44667-2\_7.

[31] Hao Ying, Feng Lin, Rodger D. MacArthur, Jonathan A. Cohn, Daniel C. Barth-Jones, Hong Ye, and Lawrence R. Crane. A fuzzy discrete event system approach to determining optimal HIV/AIDS treatment regimens. IEEE Transactions on Information Technology in Biomedicine, 10(4):663-676, 2006. doi:10.1109/TITB.2006.874200.

[32] Hao Ying, Feng Lin, Rodger D. MacArthur, Jonathan A. Cohn, Daniel C. Barth-Jones, Hong Ye, and Lawrence R. Crane. A self-learning fuzzy discrete event system for HIV/AIDS treatment regimen selection. IEEE Transactions on Systems, Man, and Cybernetics: Part B Cybernetics, 37:966-979, 2007. doi:10.1109/tsmcb.2007.895360.

Bibtex

@article{sacscuza:mandrali21atwlfwbam,
  title={A Translation of Weighted LTL Formulas to Weighted Buchi Automata over omega-valuation Monoids},
  author={E. Mandrali},
  journal={Scientific Annals of Computer Science},
  volume={31},
  number={2},
  organization={Alexandru Ioan Cuza University, Ia\c si, Rom\^ania},
  year={2021},
  pages={223-292},
  publisher={Alexandru Ioan Cuza University Press, Ia\c si},
  doi={10.7561/SACS.2021.2.223}
}