Published in Volume XXXIII, Issue 2, 2023, pages 93-157, doi: 10.7561/SACS.2023.2.93
Authors: E. Mandrali
Abstract
We define the notion of k-safe infinitary series over idempotent ordered totally generalized product omega-valuation monoids that satisfy specific properties. For each element k of the underlying structure (different from the neutral elements of the additive, and the multiplicative operation) we determine two syntactic fragments of the weighted LTL with the property that the semantics of the formulas in these fragments are k-safe infinitary series. For specific idempotent ordered totally generalized product omega-valuation monoids we provide algorithms that given a weighted Büchi automaton and a weighted LTL formula in these fragments, decide whether the behavior of the automaton coincides with the semantics of the formula.
Full Text (PDF)References
[1] Marianne Akian, Stéphane Gaubert, and Alexander Guterman. Linear independence over tropical semirings and beyond. In Grigory L. Litvinov and Sergei N. Sergeev, editors, Tropical and Idempotent Mathematics, volume 495 of Contemporary Mathematics, pages 1-38. American Mathematical Society, 2009. doi:10.48550/arXiv.0812.3496.
[2] Shaull Almagor, Udi Boker, and Orna Kupferman. Formally reasoning about quality. Journal of the ACM, 63(3):24:1-24:56, 2016. doi:10.1145/2875421.
[3] Bowen Alpern and Fred B. Schneider. Recognizing safety and liveness. Distributed Computing, 2(3):117-126, 1987. doi:10.1007/BF01782772.
[4] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
[5] Udi Boker, Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç. Safety and liveness of quantitative automata. In Guillermo A. Pérez and Jean-François Raskin, editors, 34th International Conference on Concurrency Theory, CONCUR 2023, volume 279 of LIPIcs, pages 17:1-17:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPICS.CONCUR.2023.17.
[6] Patricia Bouyer, Nicolas Markey, and Raj Mohan Matteplackel. Averaging in LTL. In Paolo Baldan and Daniele Gorla, editors, 25th International Conference on Concurrency Theory, CONCUR 2014, volume 8704 of Lecture Notes in Computer Science, pages 266-280. Springer, 2014. doi:10.1007/978-3-662-44584-6\_19.
[7] Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. In Michael Kaminski and Simone Martini, editors, 22nd International Workshop on Computer Science Logic, CSL 2008, volume 5213 of Lecture Notes in Computer Science, pages 385-400. Springer, 2008. doi:10.1007/978-3-540-87531-4\_28.
[8] Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Alternating weighted automata. In Miroslaw Kutylowski, Witold Charatonik, and Maciej Gebala, editors, 17th International Symposium on Fundamentals of Computation Theory, FCT 2009, volume 5699 of Lecture Notes in Computer Science, pages 3-13. Springer, 2009. doi:10.1007/978-3-642-03409-1\_2.
[9] Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Expressiveness and closure properties for quantitative languages. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, pages 199-208. IEEE Computer Society, 2009. doi:10.1109/LICS.2009.16.
[10] Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Probabilistic weighted automata. In Mario Bravetti and Gianluigi Zavattaro, editors, 20th International Conference on Concurrency Theory, CONCUR 2009, volume 5710 of Lecture Notes in Computer Science, pages 244-258. Springer, 2009. doi:10.1007/978-3-642-04081-8\_17.
[11] 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.
[12] Manfred Droste, Werner Kuich, and Heiko Vogler, editors. Handbook of Weighted Automata. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2009. doi:10.1007/978-3-642-01492-5.
[13] Manfred Droste and Ingmar Meinecke. Describing average- and longtime-behavior by weighted MSO logics. In Petr Hlinený and Antonı́n Kucera, editors, 35th International Symposium on Mathematical Foundations of Computer Science, MFCS 2010, volume 6281 of Lecture Notes in Computer Science, pages 537-548. Springer, 2010. doi:10.1007/978-3-642-15155-2\_47.
[14] 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.
[15] Jasmin Fisher and Nir Piterman. Model checking in biology. In Vishwesh V. Kulkarni, Guy-Bart Stan, and Karthik Raman, editors, A Systems Theoretic Approach to Systems and Synthetic Biology I: Models and System Characterizations, pages 255-279. Springer Netherlands, Dordrecht, 2014. doi:10.1007/978-94-017-9041-3_10.
[16] Jeremy Gunawardena. An introduction to idempotency. In Jeremy Gunawardena, editor, Idempotency, Publications of the Newton Institute, pages 1–-49. Cambridge University Press, 1998. doi:10.1017/CBO9780511662508.003.
[17] Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç. Quantitative safety and liveness. In Orna Kupferman and Pawel Sobocinski, editors, 26th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, volume 13992 of Lecture Notes in Computer Science, pages 349-370. Springer, 2023. doi:10.1007/978-3-031-30829-1\_17.
[18] Orna Kupferman and Yoad Lustig. Lattice automata. In Byron Cook and Andreas Podelski, editors, 8th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2007, volume 4349 of Lecture Notes in Computer Science, pages 199-213. Springer, 2007. doi:10.1007/978-3-540-69738-1\_14.
[19] Yongming Li, Manfred Droste, and Lihui Lei. Model checking of linear-time properties in multi-valued systems. Information Sciences, 377:51-74, 2017. doi:10.1016/J.INS.2016.10.030.
[20] Eleni Mandrali. Weighted LTL with discounting. In Nelma Moreira and Rogério Reis, editors, 17th International Conference on Implementation and Application of Automata, 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,. PhD thesis, Aristotle University of Thessaloniki, 2013. doi:10.12681/eadd/35478.
[22] Eleni Mandrali. A translation of weighted LTL formulas to weighted Büchi automata over ω-valuation monoids. Scientific Annals of Computer Science, 31(2):223-292, 2021. doi:10.7561/SACS.2021.2.223.
[23] 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.
[24] Gethin Norman and David Parker. Quantitative verification: Formal guarantees for timeliness, reliability and performance. Technical report, London Mathematical Society and the Smith Institute, 2014.
[25] Dominique Perrin and Jean-Eric Pin. Infinite words – automata, semigroups, logic and games, volume 141 of Pure and applied mathematics series. Elsevier Morgan Kaufmann, 2004.
[26] Amir Pnueli. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science, SFCS 1977, pages 46-57, 1977. doi:10.1109/SFCS.1977.32.
[27] Junyan Qian, Fan Shi, Yong Cai, and Haiyu Pan. Approximate safety properties in metric transition systems. IEEE Transactions on Reliability, 71(1):221-234, 2022. doi:10.1109/TR.2021.3139616.
[28] Joseph Sifakis. System design in the era of iot – meeting the autonomy challenge. In Simon Bliudze and Saddek Bensalem, editors, Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design, MeTRiD@ETAPS 2018, volume 272 of Electronic Proceedings in Theoretical Computer Science, pages 1-22, 2018. doi:10.4204/EPTCS.272.1.
[29] A. Prasad Sistla. Safety, liveness and fairness in temporal logic. Formal Aspects of Computing, 6(5):495-512, 1994. doi:10.1007/BF01211865.
[30] Stephen L. Smith, Jana Tumova, Calin Belta, and Daniela Rus. Optimal path planning for surveillance with temporal-logic constraints. International Journal of Robotics Research, 30(14):1695-1708, 2011. doi:10.1177/0278364911417911.
[31] 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.
[32] Sigal Weiner, Matan Hasson, Orna Kupferman, Eyal Pery, and Zohar Shevach. Weighted safety. In Dang Van Hung and Mizuhito Ogawa, editors, 11th International Symposium on Automated Technology for Verification and Analysis, ATVA 2013, volume 8172 of Lecture Notes in Computer Science, pages 133–147. Springer, 2013. doi:10.1007/978-3-319-02444-8\_11.
Bibtex
@article{sacscuza:mandrali2023dwswlpm,
title={Describing Weighted Safety with Weighted LTL over Product omega-valuation Monoids},
author={E. Mandrali},
journal={Scientific Annals of Computer Science},
volume={33},
number={2},
organization={Alexandru Ioan Cuza University, Ia\c si, Rom\^ania},
year={2023},
pages={93-157},
publisher={Alexandru Ioan Cuza University Press, Ia\c si},
doi={10.7561/SACS.2023.2.93}
}