License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2020.17
URN: urn:nbn:de:0030-drops-128290
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/12829/
Filiot, Emmanuel ;
Mazzocchi, Nicolas ;
Raskin, Jean-François ;
Sankaranarayanan, Sriram ;
Trivedi, Ashutosh
Weighted Transducers for Robustness Verification
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.
BibTeX - Entry
@InProceedings{filiot_et_al:LIPIcs:2020:12829,
author = {Emmanuel Filiot and Nicolas Mazzocchi and Jean-Fran{\c{c}}ois Raskin and Sriram Sankaranarayanan and Ashutosh Trivedi},
title = {{Weighted Transducers for Robustness Verification}},
booktitle = {31st International Conference on Concurrency Theory (CONCUR 2020)},
pages = {17:1--17:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-160-3},
ISSN = {1868-8969},
year = {2020},
volume = {171},
editor = {Igor Konnov and Laura Kov{\'a}cs},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/12829},
URN = {urn:nbn:de:0030-drops-128290},
doi = {10.4230/LIPIcs.CONCUR.2020.17},
annote = {Keywords: Weighted transducers, Quantitative verification, Fault-tolerance}
}
|
Keywords: |
|
Weighted transducers, Quantitative verification, Fault-tolerance |
|
Collection: |
|
31st International Conference on Concurrency Theory (CONCUR 2020) |
|
Issue Date: |
|
2020 |
|
Date of publication: |
|
26.08.2020 |
