Document Open Access Logo

Weighted Transducers for Robustness Verification

Authors Emmanuel Filiot, Nicolas Mazzocchi, Jean-François Raskin, Sriram Sankaranarayanan, Ashutosh Trivedi

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.17.pdf
  • Filesize: 0.75 MB
  • 21 pages

Document Identifiers

Author Details

Emmanuel Filiot
  • Université Libre de Bruxelles, Belgium
Nicolas Mazzocchi
  • Université Libre de Bruxelles, Belgium
Jean-François Raskin
  • Université Libre de Bruxelles, Belgium
Sriram Sankaranarayanan
  • University of Colorado Boulder, CO, USA
Ashutosh Trivedi
  • University of Colorado Boulder, CO, USA

Funding

This work is partially supported by the PDR project Subgame perfection in graph games (F.R.S.-FNRS), the MIS project F451019F (F.R.S.-FNRS), the ARC project Non-Zero Sum Game Graphs: Applications to Reactive Synthesis and Beyond (Fédération Wallonie-Bruxelles), the EOS project Verifying Learning Artificial Intelligence Systems (F.R.S.-FNRS and FWO), the COST Action 16228 GAMENET (European Cooperation in Science and Technology), and the US National Science Foundation (NSF) under award numbers CPS 1836900 and CCF 1815983.
  • Filiot, Emmanuel: Associate researcher at F.R.S.-FNRS
  • Mazzocchi, Nicolas: PhD student funded by a FRIA fellowship from the F.R.S.-FNRS.

Cite As Get BibTex

Emmanuel Filiot, Nicolas Mazzocchi, Jean-François Raskin, Sriram Sankaranarayanan, and Ashutosh Trivedi. Weighted Transducers for Robustness Verification. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 17:1-17:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CONCUR.2020.17

Abstract

Automata theory provides us with fundamental notions such as languages, membership, emptiness and inclusion that in turn allow us to specify and verify properties of reactive systems in a useful manner. However, these notions all yield "yes"/"no" answers that sometimes fall short of being satisfactory answers when the models being analyzed are imperfect, and the observations made are prone to errors. To address this issue, a common engineering approach is not just to verify that a system satisfies a property, but whether it does so robustly. We present notions of robustness that place a metric on words, thus providing a natural notion of distance between words. Such a metric naturally leads to a topological neighborhood of words and languages, leading to quantitative and robust versions of the membership, emptiness and inclusion problems. More generally, we consider weighted transducers to model the cost of errors. Such a transducer models neighborhoods of words by providing the cost of rewriting a word into another. The main contribution of this work is to study robustness verification problems in the context of weighted transducers. We provide algorithms for solving the robust and quantitative versions of the membership and inclusion problems while providing useful motivating case studies including approximate pattern matching problems to detect clinically relevant events in a large type-1 diabetes dataset.

Subject Classification

ACM Subject Classification
  • Computer systems organization → Reliability
  • Theory of computation → Formal languages and automata theory
Keywords
  • Weighted transducers
  • Quantitative verification
  • Fault-tolerance

Metrics

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

References

  1. Takumi Akazaki and Ichiro Hasuo. Time robustness in MTL and expressivity in hybrid system falsification. In Computer Aided Verification (CAV), volume 9207 of Lecture Notes in Computer Science, pages 356-374. Springer, 2015. Google Scholar
  2. Shaull Almagor, Udi Boker, and Orna Kupferman. What’s decidable about weighted automata? In Tevfik Bultan and Pao-Ann Hsiung, editors, Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011, Taipei, Taiwan, October 11-14, 2011. Proceedings, volume 6996 of Lecture Notes in Computer Science, pages 482-491. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24372-1_37.
  3. Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A Henzinger, P-H Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. The algorithmic analysis of hybrid systems. Theoretical computer science, 138(1):3-34, 1995. Google Scholar
  4. Rajeev Alur and David L Dill. A theory of timed automata. Theoretical computer science, 126(2):183-235, 1994. Google Scholar
  5. Rajeev Alur, Sampath Kannan, Kevin Tian, and Yifei Yuan. On the complexity of shortest path problems on discounted cost graphs. In Language and Automata Theory and Applications - 7th International Conference, LATA 2013, Bilbao, Spain, April 2-5, 2013. Proceedings, pages 44-55, 2013. Google Scholar
  6. Rajeev Alur and Parthasarathy Madhusudan. Visibly pushdown languages. In Proceedings of the thirty-sixth annual ACM symposium on Theory of computing, pages 202-211. ACM, 2004. Google Scholar
  7. Ezio Bartocci, Jyotirmoy Deshmukh, Alexandre Donze, Georgios Fainekos, Oded Maler, Dejan Nickovic, and Sriram Sankaranarayanan. Specification-based monitoring of cyber-physical systems: A survey on theory, tools and applications. In Lectures on Runtime Verification, volume 10457 of LNCS, pages 135-175, 2018. Google Scholar
  8. Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In International Conference on Concurrency Theory, pages 135-150. Springer, 1997. Google Scholar
  9. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Expressiveness and closure properties for quantitative languages. Logical Methods in Computer Science, 6(3), 2010. URL: http://arxiv.org/abs/1007.4018.
  10. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. ACM Trans. Comput. Logic, 11(4):23:1-23:38, July 2010. URL: https://doi.org/10.1145/1805950.1805953.
  11. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors. Handbook of Model Checking. Springer, 2018. Google Scholar
  12. Jyotirmoy V. Deshmukh, Rupak Majumdar, and Vinayak S. Prabhu. Quantifying conformance using the skorokhod metric. Formal Methods Syst. Des., 50(2-3):168-206, 2017. Google Scholar
  13. Michel Marie Deza and Elena Deza. Encyclopedia of Distances. Springer, 2009. Google Scholar
  14. Alexandre Donze and Oded Maler. Robust satisfaction of temporal logic over real-valued signals. In Formal Modeling and Analysis of Timed Systems, volume 6246 of LNCS, pages 92-106. Springer, 2010. Google Scholar
  15. Manfred Droste, Werner Kuich, and Heiko Vogler. Handbook of weighted automata. Springer Science & Business Media, 2009. Google Scholar
  16. Georgios E. Fainekos and George J. Pappas. Robustness of temporal logic specifications for continuous-time signals. Theoretical Computer Science, 410(42):4262-4291, 2009. Google Scholar
  17. Thomas A. Henzinger, Jan Otop, and Roopsha Samanta. Lipschitz robustness of finite-state transducers. In Venkatesh Raman and S. P. Suresh, editors, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, December 15-17, 2014, New Delhi, India, volume 29 of LIPIcs, pages 431-443. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2014.431.
  18. Richard M. Karp. A characterization of the minimum cycle mean in a digraph. Discrete Mathematics, 23(3):309-311, 1978. URL: https://doi.org/10.1016/0012-365X(78)90011-0.
  19. Dexter Kozen. Lower bounds for natural proof systems. In Foundations of Computer Science, pages 254-266, 1977. Google Scholar
  20. David M. Maahs, Peter Calhoun, Bruce A. Buckingham, H. Peter Chase, Irene Hramiak, John Lum, Fraser Cameron, B. Wayne Bequette, Tandy Aye, Terri Paul, Robert Slover, R. Paul Wadwa, Darrell M. Wilson, Craig Kollman, and Roy W. Beck. A randomized trial of a home system to reduce nocturnal hypoglycemia in type 1 diabetes. Diabetes Care, 37(7):1885-1891, 2014. URL: https://doi.org/10.2337/dc13-2159.
  21. Aurelien Rizk, Gregory Batt, Francois Fages, and Sylvain Soliman. Continuous valuations of temporal logic specifications with applications to parameter optimization and robustness measures. Theor. Comput. Sci., 412(26):2827-2839, 2011. Google Scholar
  22. Roopsha Samanta, Jyotirmoy V. Deshmukh, and Swarat Chaudhuri. Robustness analysis of string transducers. In Dang Van Hung and Mizuhito Ogawa, editors, Automated Technology for Verification and Analysis - 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013. Proceedings, volume 8172 of Lecture Notes in Computer Science, pages 427-441. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-02444-8_30.
  23. Stefan Schwoon. Model-checking pushdown systems. PhD thesis, Technische Universität München, 2002. Google Scholar
  24. Masaki Waga, Étienne André, and Ichiro Hasuo. Symbolic monitoring against specifications parametric in time and data. In Computer Aided Verification, pages 520-539, Cham, 2019. Springer International Publishing. 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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact