Search | arXiv e-print repository

<!DOCTYPE html> <html lang="en"> <head> <meta charset="utf-8"/> <meta name="viewport" content="width=device-width, initial-scale=1"/>  <link rel="apple-touch-icon" sizes="180x180" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/apple-touch-icon.png"> <link rel="icon" type="image/png" sizes="32x32" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/favicon-32x32.png"> <link rel="icon" type="image/png" sizes="16x16" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/favicon-16x16.png"> <link rel="manifest" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/site.webmanifest"> <link rel="mask-icon" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/safari-pinned-tab.svg" color="#b31b1b"> <link rel="shortcut icon" href="https://static.arxiv.org/static/base/1.0.0a5/images/icons/favicon.ico"> <meta name="msapplication-TileColor" content="#b31b1b"> <meta name="msapplication-config" content="images/icons/browserconfig.xml"> <meta name="theme-color" content="#b31b1b">  <title>Search | arXiv e-print repository</title> <script defer src="https://static.arxiv.org/static/base/1.0.0a5/fontawesome-free-5.11.2-web/js/all.js"></script> <link rel="stylesheet" href="https://static.arxiv.org/static/base/1.0.0a5/css/arxivstyle.css" /> <script type="text/x-mathjax-config"> MathJax.Hub.Config({ messageStyle: "none", extensions: ["tex2jax.js"], jax: ["input/TeX", "output/HTML-CSS"], tex2jax: { inlineMath: [ ['$','$'], ["\$","\$"] ], displayMath: [ ['$$','$$'], ["\\[","\\]"] ], processEscapes: true, ignoreClass: '.*', processClass: 'mathjax.*' }, TeX: { extensions: ["AMSmath.js", "AMSsymbols.js", "noErrors.js"], noErrors: { inlineDelimiters: ["$","$"], multiLine: false, style: { "font-size": "normal", "border": "" } } }, "HTML-CSS": { availableFonts: ["TeX"] } }); </script> <script src='//static.arxiv.org/MathJax-2.7.3/MathJax.js'></script> <script src="https://static.arxiv.org/static/base/1.0.0a5/js/notification.js"></script> <link rel="stylesheet" href="https://static.arxiv.org/static/search/0.5.6/css/bulma-tooltip.min.css" /> <link rel="stylesheet" href="https://static.arxiv.org/static/search/0.5.6/css/search.css" /> <script src="https://code.jquery.com/jquery-3.2.1.slim.min.js" integrity="sha256-k2WSCIexGzOj3Euiig+TlR8gA0EmPjuc79OEeY5L45g=" crossorigin="anonymous"></script> <script src="https://static.arxiv.org/static/search/0.5.6/js/fieldset.js"></script> <style> radio#cf-customfield_11400 { display: none; } </style> </head> <body> <header><a href="#main-container" class="is-sr-only">Skip to main content</a>  <div class="attribution level is-marginless" role="banner"> <div class="level-left"> <a class="level-item" href="https://cornell.edu/"><img src="https://static.arxiv.org/static/base/1.0.0a5/images/cornell-reduced-white-SMALL.svg" alt="Cornell University" width="200" aria-label="logo" /></a> </div> <div class="level-right is-marginless"><p class="sponsors level-item is-marginless"><span id="support-ack-url">We gratefully acknowledge support from<br /> the Simons Foundation, <a href="https://info.arxiv.org/about/ourmembers.html">member institutions</a>, and all contributors. <a href="https://info.arxiv.org/about/donate.html">Donate</a></span></p></div> </div>  <div class="identity level is-marginless"> <div class="level-left"> <div class="level-item"> <a class="arxiv" href="https://arxiv.org/" aria-label="arxiv-logo"> <img src="https://static.arxiv.org/static/base/1.0.0a5/images/arxiv-logo-one-color-white.svg" aria-label="logo" alt="arxiv logo" width="85" style="width:85px;"/> </a> </div> </div> <div class="search-block level-right"> <form class="level-item mini-search" method="GET" action="https://arxiv.org/search"> <div class="field has-addons"> <div class="control"> <input class="input is-small" type="text" name="query" placeholder="Search..." aria-label="Search term or terms" /> <p class="help"><a href="https://info.arxiv.org/help">Help</a> | <a href="https://arxiv.org/search/advanced">Advanced Search</a></p> </div> <div class="control"> <div class="select is-small"> <select name="searchtype" aria-label="Field to search"> <option value="all" selected="selected">All fields</option> <option value="title">Title</option> <option value="author">Author</option> <option value="abstract">Abstract</option> <option value="comments">Comments</option> <option value="journal_ref">Journal reference</option> <option value="acm_class">ACM classification</option> <option value="msc_class">MSC classification</option> <option value="report_num">Report number</option> <option value="paper_id">arXiv identifier</option> <option value="doi">DOI</option> <option value="orcid">ORCID</option> <option value="author_id">arXiv author ID</option> <option value="help">Help pages</option> <option value="full_text">Full text</option> </select> </div> </div> <input type="hidden" name="source" value="header"> <button class="button is-small is-cul-darker">Search</button> </div> </form> </div> </div>  <div class="container"> <div class="user-tools is-size-7 has-text-right has-text-weight-bold" role="navigation" aria-label="User menu"> <a href="https://arxiv.org/login">Login</a> </div> </div> </header> <main class="container" id="main-container"> <div class="level is-marginless"> <div class="level-left"> <h1 class="title is-clearfix"> Showing 1–29 of 29 results for author: <span class="mathjax">Rue脽, H</span> </h1> </div> <div class="level-right is-hidden-mobile">  <span class="help" style="display: inline-block;"><a href="https://github.com/arXiv/arxiv-search/releases">Search v0.5.6 released 2020-02-24</a>  </span> </div> </div> <div class="content"> <form method="GET" action="/search/cs" aria-role="search"> Searching in archive <strong>cs</strong>. <a href="/search/?searchtype=author&query=Rue%C3%9F%2C+H">Search in all archives.</a> <div class="field has-addons-tablet"> <div class="control is-expanded"> <label for="query" class="hidden-label">Search term or terms</label> <input class="input is-medium" id="query" name="query" placeholder="Search term..." type="text" value="Rue脽, H"> </div> <div class="select control is-medium"> <label class="is-hidden" for="searchtype">Field</label> <select class="is-medium" id="searchtype" name="searchtype"><option value="all">All fields</option><option value="title">Title</option><option selected value="author">Author(s)</option><option value="abstract">Abstract</option><option value="comments">Comments</option><option value="journal_ref">Journal reference</option><option value="acm_class">ACM classification</option><option value="msc_class">MSC classification</option><option value="report_num">Report number</option><option value="paper_id">arXiv identifier</option><option value="doi">DOI</option><option value="orcid">ORCID</option><option value="license">License (URI)</option><option value="author_id">arXiv author ID</option><option value="help">Help pages</option><option value="full_text">Full text</option></select> </div> <div class="control"> <button class="button is-link is-medium">Search</button> </div> </div> <div class="field"> <div class="control is-size-7"> <label class="radio"> <input checked id="abstracts-0" name="abstracts" type="radio" value="show"> Show abstracts </label> <label class="radio"> <input id="abstracts-1" name="abstracts" type="radio" value="hide"> Hide abstracts </label> </div> </div> <div class="is-clearfix" style="height: 2.5em"> <div class="is-pulled-right"> <a href="/search/advanced?terms-0-term=Rue%C3%9F%2C+H&terms-0-field=author&size=50&order=-announced_date_first">Advanced Search</a> </div> </div> <input type="hidden" name="order" value="-announced_date_first"> <input type="hidden" name="size" value="50"> </form> <div class="level breathe-horizontal"> <div class="level-left"> <form method="GET" action="/search/"> <div style="display: none;"> <select id="searchtype" name="searchtype"><option value="all">All fields</option><option value="title">Title</option><option selected value="author">Author(s)</option><option value="abstract">Abstract</option><option value="comments">Comments</option><option value="journal_ref">Journal reference</option><option value="acm_class">ACM classification</option><option value="msc_class">MSC classification</option><option value="report_num">Report number</option><option value="paper_id">arXiv identifier</option><option value="doi">DOI</option><option value="orcid">ORCID</option><option value="license">License (URI)</option><option value="author_id">arXiv author ID</option><option value="help">Help pages</option><option value="full_text">Full text</option></select> <input id="query" name="query" type="text" value="Rue脽, H"> <ul id="abstracts"><li><input checked id="abstracts-0" name="abstracts" type="radio" value="show"> <label for="abstracts-0">Show abstracts</label></li><li><input id="abstracts-1" name="abstracts" type="radio" value="hide"> <label for="abstracts-1">Hide abstracts</label></li></ul> </div> <div class="box field is-grouped is-grouped-multiline level-item"> <div class="control"> <span class="select is-small"> <select id="size" name="size"><option value="25">25</option><option selected value="50">50</option><option value="100">100</option><option value="200">200</option></select> </span> <label for="size">results per page</label>. </div> <div class="control"> <label for="order">Sort results by</label> <span class="select is-small"> <select id="order" name="order"><option selected value="-announced_date_first">Announcement date (newest first)</option><option value="announced_date_first">Announcement date (oldest first)</option><option value="-submitted_date">Submission date (newest first)</option><option value="submitted_date">Submission date (oldest first)</option><option value="">Relevance</option></select> </span> </div> <div class="control"> <button class="button is-small is-link">Go</button> </div> </div> </form> </div> </div> <ol class="breathe-horizontal" start="1"> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2409.19318">arXiv:2409.19318</a> <span> [<a href="https://arxiv.org/pdf/2409.19318">pdf</a>, <a href="https://arxiv.org/ps/2409.19318">ps</a>, <a href="https://arxiv.org/format/2409.19318">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Computer Science and Game Theory">cs.GT</span> </div> </div> <p class="title is-5 mathjax"> Fairness Analysis with Shapley-Owen Effects </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2409.19318v1-abstract-short" style="display: inline;"> We argue that relative importance and its equitable attribution in terms of Shapley-Owen effects is an appropriate one, and, if we accept a small number of reasonable imperatives for equitable attribution, the only way to measure fairness. On the other hand, the computation of Shapley-Owen effects can be very demanding. Our main technical result is a spectral decomposition of the Shapley-Owen effe… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2409.19318v1-abstract-full').style.display = 'inline'; document.getElementById('2409.19318v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2409.19318v1-abstract-full" style="display: none;"> We argue that relative importance and its equitable attribution in terms of Shapley-Owen effects is an appropriate one, and, if we accept a small number of reasonable imperatives for equitable attribution, the only way to measure fairness. On the other hand, the computation of Shapley-Owen effects can be very demanding. Our main technical result is a spectral decomposition of the Shapley-Owen effects, which decomposes the computation of these indices into a model-specific and a model-independent part. The model-independent part is precomputed once and for all, and the model-specific computation of Shapley-Owen effects is expressed analytically in terms of the coefficients of the model's \emph{polynomial chaos expansion} (PCE), which can now be reused to compute different Shapley-Owen effects. We also propose an algorithm for computing precise and sparse truncations of the PCE of the model and the spectral decomposition of the Shapley-Owen effects, together with upper bounds on the accumulated approximation errors. The approximations of both the PCE and the Shapley-Owen effects converge to their true values. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2409.19318v1-abstract-full').style.display = 'none'; document.getElementById('2409.19318v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 28 September, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> September 2024. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2404.17834">arXiv:2404.17834</a> <span> [<a href="https://arxiv.org/pdf/2404.17834">pdf</a>, <a href="https://arxiv.org/format/2404.17834">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> Efficient Reactive Synthesis </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Ye%2C+X">Xin Ye</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2404.17834v1-abstract-short" style="display: inline;"> Our main result is a polynomial time algorithm for deciding realizability for the GXU sublogic of linear temporal logic. This logic is particularly suitable for the specification of embedded control systems, and it is more expressive than GR(1). Reactive control programs for GXU specifications are represented as Mealy machines, which are extended by the monitoring of input events. Now, realizabili… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2404.17834v1-abstract-full').style.display = 'inline'; document.getElementById('2404.17834v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2404.17834v1-abstract-full" style="display: none;"> Our main result is a polynomial time algorithm for deciding realizability for the GXU sublogic of linear temporal logic. This logic is particularly suitable for the specification of embedded control systems, and it is more expressive than GR(1). Reactive control programs for GXU specifications are represented as Mealy machines, which are extended by the monitoring of input events. Now, realizability for GXU specifications is shown to be equivalent to solving a certain subclass of 2QBF satisfiability problems. These logical problems can be solved in cubic time in the size of GXU specifications. For unrealizable GXU specifications, stronger environment assumptions are mined from failed consistency checks based on Padoa's characterization of definability and Craig interpolation. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2404.17834v1-abstract-full').style.display = 'none'; document.getElementById('2404.17834v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 27 April, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> April 2024. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2404.16663">arXiv:2404.16663</a> <span> [<a href="https://arxiv.org/pdf/2404.16663">pdf</a>, <a href="https://arxiv.org/format/2404.16663">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Computers and Society">cs.CY</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> Conditional Fairness for Generative AIs </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cheng%2C+C">Chih-Hong Cheng</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a>, <a href="/search/cs?searchtype=author&query=Wu%2C+C">Changshun Wu</a>, <a href="/search/cs?searchtype=author&query=Zhao%2C+X">Xingyu Zhao</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2404.16663v4-abstract-short" style="display: inline;"> The deployment of generative AI (GenAI) models raises significant fairness concerns, addressed in this paper through novel characterization and enforcement techniques specific to GenAI. Unlike standard AI performing specific tasks, GenAI's broad functionality requires "conditional fairness" tailored to the context being generated, such as demographic fairness in generating images of poor people ve… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2404.16663v4-abstract-full').style.display = 'inline'; document.getElementById('2404.16663v4-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2404.16663v4-abstract-full" style="display: none;"> The deployment of generative AI (GenAI) models raises significant fairness concerns, addressed in this paper through novel characterization and enforcement techniques specific to GenAI. Unlike standard AI performing specific tasks, GenAI's broad functionality requires "conditional fairness" tailored to the context being generated, such as demographic fairness in generating images of poor people versus successful business leaders. We define two fairness levels: the first evaluates fairness in generated outputs, independent of prompts and models; the second assesses inherent fairness with neutral prompts. Given the complexity of GenAI and challenges in fairness specifications, we focus on bounding the worst case, considering a GenAI system unfair if the distance between appearances of a specific group exceeds preset thresholds. We also explore combinatorial testing for accessing relative completeness in intersectional fairness. By bounding the worst case, we develop a prompt injection scheme within an agent-based framework to enforce conditional fairness with minimal intervention, validated on state-of-the-art GenAI systems. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2404.16663v4-abstract-full').style.display = 'none'; document.getElementById('2404.16663v4-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 15 August, 2024; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 25 April, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> April 2024. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2401.02239">arXiv:2401.02239</a> <span> [<a href="https://arxiv.org/pdf/2401.02239">pdf</a>, <a href="https://arxiv.org/ps/2401.02239">ps</a>, <a href="https://arxiv.org/format/2401.02239">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> A Decision Method for Elementary Stream Calculus </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2401.02239v1-abstract-short" style="display: inline;"> The main result is a doubly exponential decision procedure for the first-order equality theory of streams with both arithmetic and control-oriented stream operations. This stream logic is expressive for elementary problems of stream calculus. </span> <span class="abstract-full has-text-grey-dark mathjax" id="2401.02239v1-abstract-full" style="display: none;"> The main result is a doubly exponential decision procedure for the first-order equality theory of streams with both arithmetic and control-oriented stream operations. This stream logic is expressive for elementary problems of stream calculus. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2401.02239v1-abstract-full').style.display = 'none'; document.getElementById('2401.02239v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 4 January, 2024; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> January 2024. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">19 pages</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">MSC Class:</span> I.1; J.6; F.4 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2401.00164">arXiv:2401.00164</a> <span> [<a href="https://arxiv.org/pdf/2401.00164">pdf</a>, <a href="https://arxiv.org/ps/2401.00164">ps</a>, <a href="https://arxiv.org/format/2401.00164">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> Solving Causal Stream Inclusions </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2401.00164v2-abstract-short" style="display: inline;"> We study solutions to systems of stream inclusions of the form 'f in T(f)', where the nondeterministic transformer 'T' on omega-infinite streams is assumed to be causal in the sense that elements in output streams are determined by a finite prefix of inputs. We first establish a correspondence between logic-based causality and metric-based contraction. Based on this causality-contraction connectio… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2401.00164v2-abstract-full').style.display = 'inline'; document.getElementById('2401.00164v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2401.00164v2-abstract-full" style="display: none;"> We study solutions to systems of stream inclusions of the form 'f in T(f)', where the nondeterministic transformer 'T' on omega-infinite streams is assumed to be causal in the sense that elements in output streams are determined by a finite prefix of inputs. We first establish a correspondence between logic-based causality and metric-based contraction. Based on this causality-contraction connection we then apply fixpoint principles to the spherically complete ultrametric space of streams to construct solutions of stream inclusions. The underlying fixpoint iterations induce fixpoint induction principles to reason about these solutions.In addition, the fixpoint approximation provides an anytime algorithm with which finite prefixes of solutions can be calculated. These developments are illustrated for some central concepts of system design. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2401.00164v2-abstract-full').style.display = 'none'; document.getElementById('2401.00164v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 24 June, 2024; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 30 December, 2023; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> January 2024. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">MSC Class:</span> D.2; F.2 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2307.12716">arXiv:2307.12716</a> <span> [<a href="https://arxiv.org/pdf/2307.12716">pdf</a>, <a href="https://arxiv.org/format/2307.12716">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> Safety Performance of Neural Networks in the Presence of Covariate Shift </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cheng%2C+C">Chih-Hong Cheng</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a>, <a href="/search/cs?searchtype=author&query=Theodorou%2C+K">Konstantinos Theodorou</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2307.12716v1-abstract-short" style="display: inline;"> Covariate shift may impact the operational safety performance of neural networks. A re-evaluation of the safety performance, however, requires collecting new operational data and creating corresponding ground truth labels, which often is not possible during operation. We are therefore proposing to reshape the initial test set, as used for the safety performance evaluation prior to deployment, base… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2307.12716v1-abstract-full').style.display = 'inline'; document.getElementById('2307.12716v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2307.12716v1-abstract-full" style="display: none;"> Covariate shift may impact the operational safety performance of neural networks. A re-evaluation of the safety performance, however, requires collecting new operational data and creating corresponding ground truth labels, which often is not possible during operation. We are therefore proposing to reshape the initial test set, as used for the safety performance evaluation prior to deployment, based on an approximation of the operational data. This approximation is obtained by observing and learning the distribution of activation patterns of neurons in the network during operation. The reshaped test set reflects the distribution of neuron activation values as observed during operation, and may therefore be used for re-evaluating safety performance in the presence of covariate shift. First, we derive conservative bounds on the values of neurons by applying finite binning and static dataflow analysis. Second, we formulate a mixed integer linear programming (MILP) constraint for constructing the minimum set of data points to be removed in the test set, such that the difference between the discretized test and operational distributions is bounded. We discuss potential benefits and limitations of this constraint-based approach based on our initial experience with an implemented research prototype. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2307.12716v1-abstract-full').style.display = 'none'; document.getElementById('2307.12716v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 24 July, 2023; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> July 2023. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2306.08447">arXiv:2306.08447</a> <span> [<a href="https://arxiv.org/pdf/2306.08447">pdf</a>, <a href="https://arxiv.org/format/2306.08447">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> </div> </div> <p class="title is-5 mathjax"> Towards Rigorous Design of OoD Detectors </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cheng%2C+C">Chih-Hong Cheng</a>, <a href="/search/cs?searchtype=author&query=Wu%2C+C">Changshun Wu</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a>, <a href="/search/cs?searchtype=author&query=Bensalem%2C+S">Saddek Bensalem</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2306.08447v1-abstract-short" style="display: inline;"> Out-of-distribution (OoD) detection techniques are instrumental for safety-related neural networks. We are arguing, however, that current performance-oriented OoD detection techniques geared towards matching metrics such as expected calibration error, are not sufficient for establishing safety claims. What is missing is a rigorous design approach for developing, verifying, and validating OoD detec… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2306.08447v1-abstract-full').style.display = 'inline'; document.getElementById('2306.08447v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2306.08447v1-abstract-full" style="display: none;"> Out-of-distribution (OoD) detection techniques are instrumental for safety-related neural networks. We are arguing, however, that current performance-oriented OoD detection techniques geared towards matching metrics such as expected calibration error, are not sufficient for establishing safety claims. What is missing is a rigorous design approach for developing, verifying, and validating OoD detectors. These design principles need to be aligned with the intended functionality and the operational domain. Here, we formulate some of the key technical challenges, together with a possible way forward, for developing a rigorous and safety-related design methodology for OoD detectors. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2306.08447v1-abstract-full').style.display = 'none'; document.getElementById('2306.08447v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 14 June, 2023; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> June 2023. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2304.00060">arXiv:2304.00060</a> <span> [<a href="https://arxiv.org/pdf/2304.00060">pdf</a>, <a href="https://arxiv.org/format/2304.00060">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Cryptography and Security">cs.CR</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> Evidential Transactions with Cyberlogic </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a>, <a href="/search/cs?searchtype=author&query=Shankar%2C+N">Natarajan Shankar</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2304.00060v1-abstract-short" style="display: inline;"> Cyberlogic is an enabling logical foundation for building and analyzing digital transactions that involve the exchange of digital forms of evidence. It is based on an extension of (first-order) intuitionistic predicate logic with an attestation and a knowledge modality. The key ideas underlying Cyberlogic are extremely simple, as (1) public keys correspond to authorizations, (2) transactions are s… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2304.00060v1-abstract-full').style.display = 'inline'; document.getElementById('2304.00060v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2304.00060v1-abstract-full" style="display: none;"> Cyberlogic is an enabling logical foundation for building and analyzing digital transactions that involve the exchange of digital forms of evidence. It is based on an extension of (first-order) intuitionistic predicate logic with an attestation and a knowledge modality. The key ideas underlying Cyberlogic are extremely simple, as (1) public keys correspond to authorizations, (2) transactions are specified as distributed logic programs, and (3) verifiable evidence is collected by means of distributed proof search. Verifiable evidence, in particular, are constructed from extra-logical elements such as signed documents and cryptographic signatures. Despite this conceptual simplicity of Cyberlogic, central features of authorization policies including trust, delegation, and revocation of authority are definable. An expressive temporal-epistemic logic for specifying distributed authorization policies and protocols is therefore definable in Cyberlogic using a trusted time source. We describe the distributed execution of Cyberlogic programs based on the hereditary Harrop fragment in terms of distributed proof search, and we illustrate some fundamental issues in the distributed construction of certificates. The main principles of encoding and executing cryptographic protocols in Cyberlogic are demonstrated. Finally, a functional encryption scheme is proposed for checking certificates of evidential transactions when policies are kept private. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2304.00060v1-abstract-full').style.display = 'none'; document.getElementById('2304.00060v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 20 March, 2023; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> April 2023. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">41 pages</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Report number:</span> SRI International, CSL Technical Report SRI-CSL-2023-01 <span class="has-text-black-bis has-text-weight-semibold">MSC Class:</span> 68M11 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2201.10436">arXiv:2201.10436</a> <span> [<a href="https://arxiv.org/pdf/2201.10436">pdf</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> </div> </div> <p class="title is-5 mathjax"> Safe AI -- How is this Possible? </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Rue%C3%9F%2C+H">Harald Rue脽</a>, <a href="/search/cs?searchtype=author&query=Burton%2C+S">Simon Burton</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2201.10436v2-abstract-short" style="display: inline;"> Ttraditional safety engineering is coming to a turning point moving from deterministic, non-evolving systems operating in well-defined contexts to increasingly autonomous and learning-enabled AI systems which are acting in largely unpredictable operating contexts. We outline some of underlying challenges of safe AI and suggest a rigorous engineering framework for minimizing uncertainty, thereby in… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2201.10436v2-abstract-full').style.display = 'inline'; document.getElementById('2201.10436v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2201.10436v2-abstract-full" style="display: none;"> Ttraditional safety engineering is coming to a turning point moving from deterministic, non-evolving systems operating in well-defined contexts to increasingly autonomous and learning-enabled AI systems which are acting in largely unpredictable operating contexts. We outline some of underlying challenges of safe AI and suggest a rigorous engineering framework for minimizing uncertainty, thereby increasing confidence, up to tolerable levels, in the safe behavior of AI systems. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2201.10436v2-abstract-full').style.display = 'none'; document.getElementById('2201.10436v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 11 May, 2022; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 25 January, 2022; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> January 2022. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">42 pages, 4 figures, 1 table</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2201.03413">arXiv:2201.03413</a> <span> [<a href="https://arxiv.org/pdf/2201.03413">pdf</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Computers and Society">cs.CY</span> </div> </div> <p class="title is-5 mathjax"> Systems Challenges for Trustworthy Embodied Systems </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Rue%C3%9F%2C+H">Harald Rue脽</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2201.03413v2-abstract-short" style="display: inline;"> A new generation of increasingly autonomous and self-learning embodied systems is about to be developed. When deploying embodied systems into a real-life context we face various engineering challenges, as it is crucial to coordinate the behavior of embodied systems in a beneficial manner, ensure their compatibility with our human-centered social values, and design verifiably safe and reliable huma… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2201.03413v2-abstract-full').style.display = 'inline'; document.getElementById('2201.03413v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2201.03413v2-abstract-full" style="display: none;"> A new generation of increasingly autonomous and self-learning embodied systems is about to be developed. When deploying embodied systems into a real-life context we face various engineering challenges, as it is crucial to coordinate the behavior of embodied systems in a beneficial manner, ensure their compatibility with our human-centered social values, and design verifiably safe and reliable human-machine interaction. We are arguing that traditional systems engineering is coming to a climacteric from embedded to embodied systems, and with assuring the trustworthiness of dynamic federations of situationally aware, intent-driven, explorative, ever-evolving, largely non-predictable, and increasingly autonomous embodied systems in uncertain, complex, and unpredictable real-world contexts. We are therefore identifying a number of urgent systems challenges for trustworthy embodied systems, including robust and human-centric AI, cognitive architectures, uncertainty quantification, trustworthy self-integration, and continual analysis and assurance. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2201.03413v2-abstract-full').style.display = 'none'; document.getElementById('2201.03413v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 26 April, 2022; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 10 January, 2022; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> January 2022. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">57 pages, 7 figures, 3 tables. Public project deliverable, fortiss whitepaper</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2012.15080">arXiv:2012.15080</a> <span> [<a href="https://arxiv.org/pdf/2012.15080">pdf</a>, <a href="https://arxiv.org/format/2012.15080">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Cryptography and Security">cs.CR</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> Security Engineering for ISO 21434 </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Dantas%2C+Y+G">Yuri Gil Dantas</a>, <a href="/search/cs?searchtype=author&query=Nigam%2C+V">Vivek Nigam</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2012.15080v3-abstract-short" style="display: inline;"> The ISO 21434 is a new standard that has been proposed to address the future challenges of automotive cybersecurity. This white paper takes a closer look at the ISO 21434 helping engineers to understand the ISO 21434 parts, the key activities to be carried out and the main artefacts that shall be produced. As any certification, obtaining the ISO 21434 certification can be daunting at first sight.… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2012.15080v3-abstract-full').style.display = 'inline'; document.getElementById('2012.15080v3-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2012.15080v3-abstract-full" style="display: none;"> The ISO 21434 is a new standard that has been proposed to address the future challenges of automotive cybersecurity. This white paper takes a closer look at the ISO 21434 helping engineers to understand the ISO 21434 parts, the key activities to be carried out and the main artefacts that shall be produced. As any certification, obtaining the ISO 21434 certification can be daunting at first sight. Engineers have to deploy processes that include several security risk assessment methods to produce security arguments and evidence supporting item security claims. In this white paper, we propose a security engineering approach that can ease this process by relying on Rigorous Security Assessments and Incremental Assessment Maintenance methods supported by automation. We demonstrate by example that the proposed approach can greatly increase the quality of the produced artefacts, the efficiency to produce them, as well as enable continuous security assessment. Finally, we point out some key research directions that we are investigating to fully realize the proposed approach. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2012.15080v3-abstract-full').style.display = 'none'; document.getElementById('2012.15080v3-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 17 January, 2021; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 30 December, 2020; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> December 2020. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">This is a White Paper. This is a preliminary version. Its figures and template are to be finalized by our marketing department. V3 corrects a number of typos</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">ACM Class:</span> I.2.4; I.2.5 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/2012.11406">arXiv:2012.11406</a> <span> [<a href="https://arxiv.org/pdf/2012.11406">pdf</a>, <a href="https://arxiv.org/format/2012.11406">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> </div> </div> <p class="title is-5 mathjax"> Knowledge as Invariance -- History and Perspectives of Knowledge-augmented Machine Learning </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Sagel%2C+A">Alexander Sagel</a>, <a href="/search/cs?searchtype=author&query=Sahu%2C+A">Amit Sahu</a>, <a href="/search/cs?searchtype=author&query=Matthes%2C+S">Stefan Matthes</a>, <a href="/search/cs?searchtype=author&query=Pfeifer%2C+H">Holger Pfeifer</a>, <a href="/search/cs?searchtype=author&query=Qiu%2C+T">Tianming Qiu</a>, <a href="/search/cs?searchtype=author&query=Rue%C3%9F%2C+H">Harald Rue脽</a>, <a href="/search/cs?searchtype=author&query=Shen%2C+H">Hao Shen</a>, <a href="/search/cs?searchtype=author&query=W%C3%B6rmann%2C+J">Julian W枚rmann</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="2012.11406v1-abstract-short" style="display: inline;"> Research in machine learning is at a turning point. While supervised deep learning has conquered the field at a breathtaking pace and demonstrated the ability to solve inference problems with unprecedented accuracy, it still does not quite live up to its name if we think of learning as the process of acquiring knowledge about a subject or problem. Major weaknesses of present-day deep learning mode… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2012.11406v1-abstract-full').style.display = 'inline'; document.getElementById('2012.11406v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="2012.11406v1-abstract-full" style="display: none;"> Research in machine learning is at a turning point. While supervised deep learning has conquered the field at a breathtaking pace and demonstrated the ability to solve inference problems with unprecedented accuracy, it still does not quite live up to its name if we think of learning as the process of acquiring knowledge about a subject or problem. Major weaknesses of present-day deep learning models are, for instance, their lack of adaptability to changes of environment or their incapability to perform other kinds of tasks than the one they were trained for. While it is still unclear how to overcome these limitations, one can observe a paradigm shift within the machine learning community, with research interests shifting away from increasing the performance of highly parameterized models to exceedingly specific tasks, and towards employing machine learning algorithms in highly diverse domains. This research question can be approached from different angles. For instance, the field of Informed AI investigates the problem of infusing domain knowledge into a machine learning model, by using techniques such as regularization, data augmentation or post-processing. On the other hand, a remarkable number of works in the recent years has focused on developing models that by themselves guarantee a certain degree of versatility and invariance with respect to the domain or problem at hand. Thus, rather than investigating how to provide domain-specific knowledge to machine learning models, these works explore methods that equip the models with the capability of acquiring the knowledge by themselves. This white paper provides an introduction and discussion of this emerging field in machine learning research. To this end, it reviews the role of knowledge in machine learning, and discusses its relation to the concept of invariance, before providing a literature review of the field. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('2012.11406v1-abstract-full').style.display = 'none'; document.getElementById('2012.11406v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 21 December, 2020; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> December 2020. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1810.04866">arXiv:1810.04866</a> <span> [<a href="https://arxiv.org/pdf/1810.04866">pdf</a>, <a href="https://arxiv.org/format/1810.04866">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> Model-Based Safety and Security Engineering </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Nigam%2C+V">Vivek Nigam</a>, <a href="/search/cs?searchtype=author&query=Pretschner%2C+A">Alexander Pretschner</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1810.04866v2-abstract-short" style="display: inline;"> By exploiting the increasing surface attack of systems, cyber-attacks can cause catastrophic events, such as, remotely disable safety mechanisms. This means that in order to avoid hazards, safety and security need to be integrated, exchanging information, such as, key hazards/threats, risk evaluations, mechanisms used. This white paper describes some steps towards this integration by using models.… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1810.04866v2-abstract-full').style.display = 'inline'; document.getElementById('1810.04866v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1810.04866v2-abstract-full" style="display: none;"> By exploiting the increasing surface attack of systems, cyber-attacks can cause catastrophic events, such as, remotely disable safety mechanisms. This means that in order to avoid hazards, safety and security need to be integrated, exchanging information, such as, key hazards/threats, risk evaluations, mechanisms used. This white paper describes some steps towards this integration by using models. We start by identifying some key technical challenges. Then we demonstrate how models, such as Goal Structured Notation (GSN) for safety and Attack Defense Trees (ADT) for security, can address these challenges. In particular, (1) we demonstrate how to extract in an automated fashion security relevant information from safety assessments by translating GSN-Models into ADTs; (2) We show how security results can impact the confidence of safety assessments; (3) We propose a collaborative development process where safety and security assessments are built by incrementally taking into account safety and security analysis; (4) We describe how to carry out trade-off analysis in an automated fashion, such as identifying when safety and security arguments contradict each other and how to solve such contradictions. We conclude pointing out that these are the first steps towards a wide range of techniques to support Safety and Security Engineering. As a white paper, we avoid being too technical, preferring to illustrate features by using examples and thus being more accessible. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1810.04866v2-abstract-full').style.display = 'none'; document.getElementById('1810.04866v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 2 January, 2019; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 11 October, 2018; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> October 2018. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">White paper on Safety and Security Engineering using Models</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1806.02338">arXiv:1806.02338</a> <span> [<a href="https://arxiv.org/pdf/1806.02338">pdf</a>, <a href="https://arxiv.org/format/1806.02338">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Machine Learning">stat.ML</span> </div> </div> <p class="title is-5 mathjax"> Towards Dependability Metrics for Neural Networks </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cheng%2C+C">Chih-Hong Cheng</a>, <a href="/search/cs?searchtype=author&query=N%C3%BChrenberg%2C+G">Georg N眉hrenberg</a>, <a href="/search/cs?searchtype=author&query=Huang%2C+C">Chung-Hao Huang</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a>, <a href="/search/cs?searchtype=author&query=Yasuoka%2C+H">Hirotoshi Yasuoka</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1806.02338v2-abstract-short" style="display: inline;"> Artificial neural networks (NN) are instrumental in realizing highly-automated driving functionality. An overarching challenge is to identify best safety engineering practices for NN and other learning-enabled components. In particular, there is an urgent need for an adequate set of metrics for measuring all-important NN dependability attributes. We address this challenge by proposing a number of… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1806.02338v2-abstract-full').style.display = 'inline'; document.getElementById('1806.02338v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1806.02338v2-abstract-full" style="display: none;"> Artificial neural networks (NN) are instrumental in realizing highly-automated driving functionality. An overarching challenge is to identify best safety engineering practices for NN and other learning-enabled components. In particular, there is an urgent need for an adequate set of metrics for measuring all-important NN dependability attributes. We address this challenge by proposing a number of NN-specific and efficiently computable metrics for measuring NN dependability attributes including robustness, interpretability, completeness, and correctness. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1806.02338v2-abstract-full').style.display = 'none'; document.getElementById('1806.02338v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 8 June, 2018; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 6 June, 2018; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> June 2018. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1710.03107">arXiv:1710.03107</a> <span> [<a href="https://arxiv.org/pdf/1710.03107">pdf</a>, <a href="https://arxiv.org/format/1710.03107">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> Verification of Binarized Neural Networks via Inter-Neuron Factoring </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cheng%2C+C">Chih-Hong Cheng</a>, <a href="/search/cs?searchtype=author&query=N%C3%BChrenberg%2C+G">Georg N眉hrenberg</a>, <a href="/search/cs?searchtype=author&query=Huang%2C+C">Chung-Hao Huang</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1710.03107v2-abstract-short" style="display: inline;"> We study the problem of formal verification of Binarized Neural Networks (BNN), which have recently been proposed as a energy-efficient alternative to traditional learning networks. The verification of BNNs, using the reduction to hardware verification, can be even more scalable by factoring computations among neurons within the same layer. By proving the NP-hardness of finding optimal factoring a… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1710.03107v2-abstract-full').style.display = 'inline'; document.getElementById('1710.03107v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1710.03107v2-abstract-full" style="display: none;"> We study the problem of formal verification of Binarized Neural Networks (BNN), which have recently been proposed as a energy-efficient alternative to traditional learning networks. The verification of BNNs, using the reduction to hardware verification, can be even more scalable by factoring computations among neurons within the same layer. By proving the NP-hardness of finding optimal factoring as well as the hardness of PTAS approximability, we design polynomial-time search heuristics to generate factoring solutions. The overall framework allows applying verification techniques to moderately-sized BNNs for embedded devices with thousands of neurons and inputs. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1710.03107v2-abstract-full').style.display = 'none'; document.getElementById('1710.03107v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 19 January, 2018; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 9 October, 2017; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> October 2017. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Version 2: add proofs for hardness of PTAS approximability, remove experiments on randomized examples and some not-so-important optimizations</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1709.00911">arXiv:1709.00911</a> <span> [<a href="https://arxiv.org/pdf/1709.00911">pdf</a>, <a href="https://arxiv.org/format/1709.00911">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> </div> </div> <p class="title is-5 mathjax"> Neural Networks for Safety-Critical Applications - Challenges, Experiments and Perspectives </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cheng%2C+C">Chih-Hong Cheng</a>, <a href="/search/cs?searchtype=author&query=Diehl%2C+F">Frederik Diehl</a>, <a href="/search/cs?searchtype=author&query=Hamza%2C+Y">Yassine Hamza</a>, <a href="/search/cs?searchtype=author&query=Hinz%2C+G">Gereon Hinz</a>, <a href="/search/cs?searchtype=author&query=N%C3%BChrenberg%2C+G">Georg N眉hrenberg</a>, <a href="/search/cs?searchtype=author&query=Rickert%2C+M">Markus Rickert</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a>, <a href="/search/cs?searchtype=author&query=Troung-Le%2C+M">Michael Troung-Le</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1709.00911v1-abstract-short" style="display: inline;"> We propose a methodology for designing dependable Artificial Neural Networks (ANN) by extending the concepts of understandability, correctness, and validity that are crucial ingredients in existing certification standards. We apply the concept in a concrete case study in designing a high-way ANN-based motion predictor to guarantee safety properties such as impossibility for the ego vehicle to sugg… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1709.00911v1-abstract-full').style.display = 'inline'; document.getElementById('1709.00911v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1709.00911v1-abstract-full" style="display: none;"> We propose a methodology for designing dependable Artificial Neural Networks (ANN) by extending the concepts of understandability, correctness, and validity that are crucial ingredients in existing certification standards. We apply the concept in a concrete case study in designing a high-way ANN-based motion predictor to guarantee safety properties such as impossibility for the ego vehicle to suggest moving to the right lane if there exists another vehicle on its right. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1709.00911v1-abstract-full').style.display = 'none'; document.getElementById('1709.00911v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 4 September, 2017; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> September 2017. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Summary for activities conducted in the fortiss Eigenforschungsprojekt "TdpSW - Towards dependable and predictable SW for ML-based autonomous systems". All ANN-based motion predictors being formally analyzed are available in the source file</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1705.01040">arXiv:1705.01040</a> <span> [<a href="https://arxiv.org/pdf/1705.01040">pdf</a>, <a href="https://arxiv.org/format/1705.01040">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Machine Learning">cs.LG</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Artificial Intelligence">cs.AI</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> Maximum Resilience of Artificial Neural Networks </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cheng%2C+C">Chih-Hong Cheng</a>, <a href="/search/cs?searchtype=author&query=N%C3%BChrenberg%2C+G">Georg N眉hrenberg</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1705.01040v2-abstract-short" style="display: inline;"> The deployment of Artificial Neural Networks (ANNs) in safety-critical applications poses a number of new verification and certification challenges. In particular, for ANN-enabled self-driving vehicles it is important to establish properties about the resilience of ANNs to noisy or even maliciously manipulated sensory input. We are addressing these challenges by defining resilience properties of A… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1705.01040v2-abstract-full').style.display = 'inline'; document.getElementById('1705.01040v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1705.01040v2-abstract-full" style="display: none;"> The deployment of Artificial Neural Networks (ANNs) in safety-critical applications poses a number of new verification and certification challenges. In particular, for ANN-enabled self-driving vehicles it is important to establish properties about the resilience of ANNs to noisy or even maliciously manipulated sensory input. We are addressing these challenges by defining resilience properties of ANN-based classifiers as the maximal amount of input or sensor perturbation which is still tolerated. This problem of computing maximal perturbation bounds for ANNs is then reduced to solving mixed integer optimization problems (MIP). A number of MIP encoding heuristics are developed for drastically reducing MIP-solver runtimes, and using parallelization of MIP-solvers results in an almost linear speed-up in the number (up to a certain limit) of computing cores in our experiments. We demonstrate the effectiveness and scalability of our approach by means of computing maximal resilience bounds for a number of ANN benchmark sets ranging from typical image recognition scenarios to the autonomous maneuvering of robots. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1705.01040v2-abstract-full').style.display = 'none'; document.getElementById('1705.01040v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 5 July, 2017; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 28 April, 2017; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> May 2017. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Timestamp research work conducted in the project. version 2: fix some typos, rephrase the definition, and add some more existing work</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1704.07097">arXiv:1704.07097</a> <span> [<a href="https://arxiv.org/pdf/1704.07097">pdf</a>, <a href="https://arxiv.org/format/1704.07097">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> Automated Analysis of Multi-View Software Architectures </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cheng%2C+C">Chih-Hong Cheng</a>, <a href="/search/cs?searchtype=author&query=Hamza%2C+Y">Yassine Hamza</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1704.07097v1-abstract-short" style="display: inline;"> Software architectures usually are comprised of different views for capturing static, runtime, and deployment aspects. What is currently missing, however, are formal validation and verification techniques of multi-view architecture in very early phases of the software development lifecycle. The main contribution of this paper therefore is the construction of a single formal model (in Promela) for… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1704.07097v1-abstract-full').style.display = 'inline'; document.getElementById('1704.07097v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1704.07097v1-abstract-full" style="display: none;"> Software architectures usually are comprised of different views for capturing static, runtime, and deployment aspects. What is currently missing, however, are formal validation and verification techniques of multi-view architecture in very early phases of the software development lifecycle. The main contribution of this paper therefore is the construction of a single formal model (in Promela) for certain stylized, and widely used, multi-view architectures by suitably interpreting and fusing sub-models from different UML diagrams. Possible counter-examples produced by model checking are fed back as test scenarios for debugging the multi-view architectural model. We have implemented this algorithm as a plug-in for the Enterprise Architect development tool, and successfully used SPIN model checking for debugging some industrial architectural multi-view models by identifying a number of undesirable corner cases. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1704.07097v1-abstract-full').style.display = 'none'; document.getElementById('1704.07097v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 24 April, 2017; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> April 2017. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Timestamping research work conducted under the fortiss Eigenforschung project</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1605.01153">arXiv:1605.01153</a> <span> [<a href="https://arxiv.org/pdf/1605.01153">pdf</a>, <a href="https://arxiv.org/format/1605.01153">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> Structural Synthesis for GXW Specifications </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cheng%2C+C">Chih-Hong Cheng</a>, <a href="/search/cs?searchtype=author&query=Hamza%2C+Y">Yassine Hamza</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1605.01153v3-abstract-short" style="display: inline;"> We define the GXW fragment of linear temporal logic (LTL) as the basis for synthesizing embedded control software for safety-critical applications. Since GXW includes the use of a weak-until operator we are able to specify a number of diverse programmable logic control (PLC) problems, which we have compiled from industrial training sets. For GXW controller specifications, we develop a novel approa… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1605.01153v3-abstract-full').style.display = 'inline'; document.getElementById('1605.01153v3-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1605.01153v3-abstract-full" style="display: none;"> We define the GXW fragment of linear temporal logic (LTL) as the basis for synthesizing embedded control software for safety-critical applications. Since GXW includes the use of a weak-until operator we are able to specify a number of diverse programmable logic control (PLC) problems, which we have compiled from industrial training sets. For GXW controller specifications, we develop a novel approach for synthesizing a set of synchronously communicating actor-based controllers. This synthesis algorithm proceeds by means of recursing over the structure of GXW specifications, and generates a set of dedicated and synchronously communicating sub-controllers according to the formula structure. In a subsequent step, 2QBF constraint solving identifies and tries to resolve potential conflicts between individual GXW specifications. This structural approach to GXW synthesis supports traceability between requirements and the generated control code as mandated by certification regimes for safety-critical software. Synthesis for GXW specifications is in PSPACE compared to 2EXPTIME-completeness of full-fledged LTL synthesis. Indeed our experimental results suggest that GXW synthesis scales well to industrial-sized control synthesis problems with 20 input and output ports and beyond. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1605.01153v3-abstract-full').style.display = 'none'; document.getElementById('1605.01153v3-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 6 July, 2016; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 4 May, 2016; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> May 2016. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">The long (including appendix) version being reviewed by CAV'16 program committee. Compared to the submitted version, one author (out of her wish) is moved to the Acknowledgement. (v2) Corrected typos. (v3) Add an additional remark over environment assumption and easy corner cases</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1504.05513">arXiv:1504.05513</a> <span> [<a href="https://arxiv.org/pdf/1504.05513">pdf</a>, <a href="https://arxiv.org/format/1504.05513">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Formal Languages and Automata Theory">cs.FL</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Symbolic Computation">cs.SC</span> </div> </div> <p class="title is-5 mathjax"> Timed Orchestration for Component-based Systems </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cheng%2C+C">Chih-Hong Cheng</a>, <a href="/search/cs?searchtype=author&query=Astefanoaei%2C+L">Lacramioara Astefanoaei</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a>, <a href="/search/cs?searchtype=author&query=Rayana%2C+S+B">Souha Ben Rayana</a>, <a href="/search/cs?searchtype=author&query=Bensalem%2C+S">Saddek Bensalem</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1504.05513v3-abstract-short" style="display: inline;"> Individual machines in flexible production lines explicitly expose capabilities at their interfaces by means of parametric skills. Given such a set of configurable machines, a line integrator is faced with the problem of finding and tuning parameters for each machine such that the overall production line implements given safety and temporal requirements in an optimized and robust fashion. We forma… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1504.05513v3-abstract-full').style.display = 'inline'; document.getElementById('1504.05513v3-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1504.05513v3-abstract-full" style="display: none;"> Individual machines in flexible production lines explicitly expose capabilities at their interfaces by means of parametric skills. Given such a set of configurable machines, a line integrator is faced with the problem of finding and tuning parameters for each machine such that the overall production line implements given safety and temporal requirements in an optimized and robust fashion. We formalize this problem of configuring and orchestrating flexible production lines as a parameter synthesis problem for systems of parametric timed automata, where interactions are based on skills. Parameter synthesis problems for interaction-level LTL properties are translated to parameter synthesis problems for state-based safety properties. For safety properties, synthesis problems are solved by checking satisfiability of $\exists\forall$SMT constraints. For constraint generation, we provide a set of computationally cheap over-approximations of the set of reachable states, together with fence constructions as sufficient conditions for safety formulas. We demonstrate the feasibility of our approach by solving typical machine configuration problems as encountered in industrial automation. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1504.05513v3-abstract-full').style.display = 'none'; document.getElementById('1504.05513v3-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 20 May, 2016; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 21 April, 2015; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> April 2015. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Timestamp of the work, with evaluation added by creating MES orchestration examples. (v3): typo fix and bring back definition and citation in en^t as in v1</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1405.2409">arXiv:1405.2409</a> <span> [<a href="https://arxiv.org/pdf/1405.2409">pdf</a>, <a href="https://arxiv.org/format/1405.2409">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> G4LTL-ST: Automatic Generation of PLC Programs </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cheng%2C+C">Chih-Hong Cheng</a>, <a href="/search/cs?searchtype=author&query=Huang%2C+C">Chung-Hao Huang</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a>, <a href="/search/cs?searchtype=author&query=Stattelmann%2C+S">Stefan Stattelmann</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1405.2409v2-abstract-short" style="display: inline;"> G4LTL-ST automatically synthesizes control code for industrial Programmable Logic Controls (PLC) from timed behavioral specifications of input-output signals. These specifications are expressed in a linear temporal logic (LTL) extended with non-linear arithmetic constraints and timing constraints on signals. G4LTL-ST generates code in IEC 61131-3-compatible Structured Text, which is compiled into… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1405.2409v2-abstract-full').style.display = 'inline'; document.getElementById('1405.2409v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1405.2409v2-abstract-full" style="display: none;"> G4LTL-ST automatically synthesizes control code for industrial Programmable Logic Controls (PLC) from timed behavioral specifications of input-output signals. These specifications are expressed in a linear temporal logic (LTL) extended with non-linear arithmetic constraints and timing constraints on signals. G4LTL-ST generates code in IEC 61131-3-compatible Structured Text, which is compiled into executable code for a large number of industrial field-level devices. The synthesis algorithm of G4LTL-ST implements pseudo-Boolean abstraction of data constraints and the compilation of timing constraints into LTL, together with a counterstrategy-guided abstraction refinement synthesis loop. Since temporal logic specifications are notoriously difficult to use in practice, G4LTL-ST supports engineers in specifying realizable control problems by suggesting suitable restrictions on the behavior of the control environment from failed synthesis attempts. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1405.2409v2-abstract-full').style.display = 'none'; document.getElementById('1405.2409v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 15 May, 2014; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 10 May, 2014; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> May 2014. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">This is the full version of the CAV'14 paper. Research concepts developed this paper are mainly from the technical report "Numerical LTL synthesis for cyber-physical systems", coauthored by Chih-Hong Cheng (ABB Research) and Edward A. Lee (UC Berkeley)</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1401.1693">arXiv:1401.1693</a> <span> [<a href="https://arxiv.org/pdf/1401.1693">pdf</a>, <a href="https://arxiv.org/format/1401.1693">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> Certification for mu-calculus with winning strategies </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Hofmann%2C+M">Martin Hofmann</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1401.1693v1-abstract-short" style="display: inline;"> We define memory-efficient certificates for $渭$-calculus model checking problems based on the well-known correspondence of the $渭$-calculus model checking with winning certain parity games. Winning strategies can independently checked, in low polynomial time, by observing that there is no reachable strongly connected component in the graph of the parity game whose largest priority is odd. Winning… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1401.1693v1-abstract-full').style.display = 'inline'; document.getElementById('1401.1693v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1401.1693v1-abstract-full" style="display: none;"> We define memory-efficient certificates for $渭$-calculus model checking problems based on the well-known correspondence of the $渭$-calculus model checking with winning certain parity games. Winning strategies can independently checked, in low polynomial time, by observing that there is no reachable strongly connected component in the graph of the parity game whose largest priority is odd. Winning strategies are computed by fixpoint iteration following the naive semantics of $渭$-calculus. We instrument the usual fixpoint iteration of $渭$-calculus model checking so that it produces evidence in the form of a winning strategy; these winning strategies can be computed in polynomial time in $|S|$ and in space $O(|S|^2 |蠁|^2)$, where $|S|$ is the size of the state space and $|蠁|$ the length of the formula $蠁$\@. The main technical contribution here is the notion and algebra of partial winning strategies. On the technical level our work can be seen as a new, simpler, and immediate constructive proof of the correspondence between $渭$-calculus and parity games. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1401.1693v1-abstract-full').style.display = 'none'; document.getElementById('1401.1693v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 8 January, 2014; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> January 2014. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Presented at the VeriSure workshop associated with CAV'13 in St. Petersburg in July 2013</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1310.3723">arXiv:1310.3723</a> <span> [<a href="https://arxiv.org/pdf/1310.3723">pdf</a>, <a href="https://arxiv.org/ps/1310.3723">ps</a>, <a href="https://arxiv.org/format/1310.3723">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Cryptography and Security">cs.CR</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Distributed, Parallel, and Cluster Computing">cs.DC</span> </div> </div> <p class="title is-5 mathjax"> Security policies for distributed systems </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Quilbeuf%2C+J">Jean Quilbeuf</a>, <a href="/search/cs?searchtype=author&query=Igna%2C+G">Georgeta Igna</a>, <a href="/search/cs?searchtype=author&query=Bytschkow%2C+D">Denis Bytschkow</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1310.3723v1-abstract-short" style="display: inline;"> A security policy specifies a security property as the maximal information flow. A distributed system composed of interacting processes implicitly defines an intransitive security policy by repudiating direct information flow between processes that do not exchange messages directly. We show that implicitly defined security policies in distributed systems are enforced, provided that processes run i… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1310.3723v1-abstract-full').style.display = 'inline'; document.getElementById('1310.3723v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1310.3723v1-abstract-full" style="display: none;"> A security policy specifies a security property as the maximal information flow. A distributed system composed of interacting processes implicitly defines an intransitive security policy by repudiating direct information flow between processes that do not exchange messages directly. We show that implicitly defined security policies in distributed systems are enforced, provided that processes run in separation, and possible process communication on a technical platform is restricted to specified message paths of the system. Furthermore, we propose to further restrict the allowable information flow by adding filter functions for controlling which messages may be transmitted between processes, and we prove that locally checking filter functions is sufficient for ensuring global security policies. Altogether, global intransitive security policies are established by means of local verification conditions for the (trusted) processes of the distributed system. Moreover, security policies may be implemented securely on distributed integration platforms which ensure partitioning. We illustrate our results with a smart grid case study, where we use CTL model checking for discharging local verification conditions for each process under consideration. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1310.3723v1-abstract-full').style.display = 'none'; document.getElementById('1310.3723v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 14 October, 2013; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> October 2013. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Submitted to POST14</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1306.6115">arXiv:1306.6115</a> <span> [<a href="https://arxiv.org/pdf/1306.6115">pdf</a>, <a href="https://arxiv.org/format/1306.6115">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> On Behavioral Types for OSGi: From Theory to Implementation </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Blech%2C+J+O">Jan Olaf Blech</a>, <a href="/search/cs?searchtype=author&query=Rue%C3%9F%2C+H">Harald Rue脽</a>, <a href="/search/cs?searchtype=author&query=Sch%C3%A4tz%2C+B">Bernhard Sch盲tz</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1306.6115v1-abstract-short" style="display: inline;"> This report presents our work on behavioral types for OSGi component systems. It extends previously published work and presents features and details that have not yet been published. In particular, we cover a discussion on behavioral types in general, and Eclipse based implementation work on behavioral types . The implementation work covers: editors, means for comparing types at development and ru… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1306.6115v1-abstract-full').style.display = 'inline'; document.getElementById('1306.6115v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1306.6115v1-abstract-full" style="display: none;"> This report presents our work on behavioral types for OSGi component systems. It extends previously published work and presents features and details that have not yet been published. In particular, we cover a discussion on behavioral types in general, and Eclipse based implementation work on behavioral types . The implementation work covers: editors, means for comparing types at development and runtime, a tool connection to resolve incompatibilities, and an AspectJ based infrastructure to ensure behavioral type correctness at runtime of a system. Furthermore, the implementation comprises various auxiliary operations. We present some evaluation work based on examples. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1306.6115v1-abstract-full').style.display = 'none'; document.getElementById('1306.6115v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 25 June, 2013; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> June 2013. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">arXiv admin note: text overlap with arXiv:1302.5175</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1306.3456">arXiv:1306.3456</a> <span> [<a href="https://arxiv.org/pdf/1306.3456">pdf</a>, <a href="https://arxiv.org/format/1306.3456">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> </div> <p class="title is-5 mathjax"> EFSMT: A Logical Framework for Cyber-Physical Systems </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cheng%2C+C">Chih-Hong Cheng</a>, <a href="/search/cs?searchtype=author&query=Shankar%2C+N">Natarajan Shankar</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a>, <a href="/search/cs?searchtype=author&query=Bensalem%2C+S">Saddek Bensalem</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1306.3456v1-abstract-short" style="display: inline;"> The design of cyber-physical systems is challenging in that it includes the analysis and synthesis of distributed and embedded real-time systems for controlling, often in a nonlinear way, the environment. We address this challenge with EFSMT, the exists-forall quantified first-order fragment of propositional combinations over constraints (including nonlinear arithmetic), as the logical framework a… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1306.3456v1-abstract-full').style.display = 'inline'; document.getElementById('1306.3456v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1306.3456v1-abstract-full" style="display: none;"> The design of cyber-physical systems is challenging in that it includes the analysis and synthesis of distributed and embedded real-time systems for controlling, often in a nonlinear way, the environment. We address this challenge with EFSMT, the exists-forall quantified first-order fragment of propositional combinations over constraints (including nonlinear arithmetic), as the logical framework and foundation for analyzing and synthesizing cyber-physical systems. We demonstrate the expressiveness of EFSMT by reducing a number of pivotal verification and synthesis problems to EFSMT. Exemplary problems in this paper include synthesis for robust control via BIBO stability, Lyapunov coefficient finding for nonlinear control systems, distributed priority synthesis for orchestrating system components, and synthesis for hybrid control systems. We are also proposing an algorithm for solving EFSMT problems based on the interplay between two SMT solvers for respectively solving universally and existentially quantified problems. This algorithms builds on commonly used techniques in modern SMT solvers, and generalizes them to quantifier reasoning by counterexample-guided constraint strengthening. The EFSMT solver uses Bernstein polynomials for solving nonlinear arithmetic constraints. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1306.3456v1-abstract-full').style.display = 'none'; document.getElementById('1306.3456v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 14 June, 2013; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> June 2013. </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1211.6189">arXiv:1211.6189</a> <span> [<a href="https://arxiv.org/pdf/1211.6189">pdf</a>, <a href="https://arxiv.org/format/1211.6189">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Systems and Control">eess.SY</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> </div> <div class="is-inline-block" style="margin-left: 0.5rem"> <div class="tags has-addons"> <span class="tag is-dark is-size-7">doi</span> <span class="tag is-light is-size-7"><a class="" href="https://doi.org/10.4204/EPTCS.102.7">10.4204/EPTCS.102.7 <i class="fa fa-external-link" aria-hidden="true"></i></a></span> </div> </div> </div> <p class="title is-5 mathjax"> Distributed Priority Synthesis </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cheng%2C+C">Chih-Hong Cheng</a>, <a href="/search/cs?searchtype=author&query=Yan%2C+R">Rongjie Yan</a>, <a href="/search/cs?searchtype=author&query=Bensalem%2C+S">Saddek Bensalem</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1211.6189v1-abstract-short" style="display: inline;"> Given a set of interacting components with non-deterministic variable update and given safety requirements, the goal of priority synthesis is to restrict, by means of priorities, the set of possible interactions in such a way as to guarantee the given safety conditions for all possible runs. In distributed priority synthesis we are interested in obtaining local sets of priorities, which are de… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1211.6189v1-abstract-full').style.display = 'inline'; document.getElementById('1211.6189v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1211.6189v1-abstract-full" style="display: none;"> Given a set of interacting components with non-deterministic variable update and given safety requirements, the goal of priority synthesis is to restrict, by means of priorities, the set of possible interactions in such a way as to guarantee the given safety conditions for all possible runs. In distributed priority synthesis we are interested in obtaining local sets of priorities, which are deployed in terms of local component controllers sharing intended next moves between components in local neighborhoods only. These possible communication paths between local controllers are specified by means of a communication architecture. We formally define the problem of distributed priority synthesis in terms of a multi-player safety game between players for (angelically) selecting the next transition of the components and an environment for (demonically) updating uncontrollable variables. We analyze the complexity of the problem, and propose several optimizations including a solution-space exploration based on a diagnosis method using a nested extension of the usual attractor computation in games together with a reduction to corresponding SAT problems. When diagnosis fails, the method proposes potential candidates to guide the exploration. These optimized algorithms for solving distributed priority synthesis problems have been integrated into the VissBIP framework. An experimental validation of this implementation is performed using a range of case studies including scheduling in multicore processors and modular robotics. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1211.6189v1-abstract-full').style.display = 'none'; document.getElementById('1211.6189v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 26 November, 2012; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> November 2012. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">In Proceedings SSV 2012, arXiv:1211.5873</span> </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Journal ref:</span> EPTCS 102, 2012, pp. 57-72 </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1112.1783">arXiv:1112.1783</a> <span> [<a href="https://arxiv.org/pdf/1112.1783">pdf</a>, <a href="https://arxiv.org/format/1112.1783">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Computer Science and Game Theory">cs.GT</span> </div> </div> <p class="title is-5 mathjax"> Distributed Priority Synthesis and its Applications </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cheng%2C+C">Chih-Hong Cheng</a>, <a href="/search/cs?searchtype=author&query=Bensalem%2C+S">Saddek Bensalem</a>, <a href="/search/cs?searchtype=author&query=Yan%2C+R">Rongjie Yan</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a>, <a href="/search/cs?searchtype=author&query=Buckl%2C+C">Christian Buckl</a>, <a href="/search/cs?searchtype=author&query=Knoll%2C+A">Alois Knoll</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1112.1783v2-abstract-short" style="display: inline;"> Given a set of interacting components with non-deterministic variable update and given safety requirements, the goal of priority synthesis is to restrict, by means of priorities, the set of possible interactions in such a way as to guarantee the given safety conditions for all possible runs. In distributed priority synthesis we are interested in obtaining local sets of priorities, which are deploy… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1112.1783v2-abstract-full').style.display = 'inline'; document.getElementById('1112.1783v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1112.1783v2-abstract-full" style="display: none;"> Given a set of interacting components with non-deterministic variable update and given safety requirements, the goal of priority synthesis is to restrict, by means of priorities, the set of possible interactions in such a way as to guarantee the given safety conditions for all possible runs. In distributed priority synthesis we are interested in obtaining local sets of priorities, which are deployed in terms of local component controllers sharing intended next moves between components in local neighborhoods only. These possible communication paths between local controllers are specified by means of a communication architecture. We formally define the problem of distributed priority synthesis in terms of a multi-player safety game between players for (angelically) selecting the next transition of the components and an environment for (demonically) updating uncontrollable variables; this problem is NP-complete. We propose several optimizations including a solution-space exploration based on a diagnosis method using a nested extension of the usual attractor computation in games together with a reduction to corresponding SAT problems. When diagnosis fails, the method proposes potential candidates to guide the exploration. These optimized algorithms for solving distributed priority synthesis problems have been integrated into our VissBIP framework. An experimental validation of this implementation is performed using a range of case studies including scheduling in multicore processors and modular robotics. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1112.1783v2-abstract-full').style.display = 'none'; document.getElementById('1112.1783v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 27 January, 2012; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 8 December, 2011; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> December 2011. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">1. Timestamp the joint work "Distributed Priority Synthesis" from four institutes (Verimag, TUM, ISCAS, fortiss). 2. This version (v.2) updates related work in distributed synthesis</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1107.1383">arXiv:1107.1383</a> <span> [<a href="https://arxiv.org/pdf/1107.1383">pdf</a>, <a href="https://arxiv.org/format/1107.1383">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Logic in Computer Science">cs.LO</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Systems and Control">eess.SY</span> </div> </div> <p class="title is-5 mathjax"> Algorithms for Synthesizing Priorities in Component-based Systems </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cheng%2C+C">Chih-Hong Cheng</a>, <a href="/search/cs?searchtype=author&query=Bensalem%2C+S">Saddek Bensalem</a>, <a href="/search/cs?searchtype=author&query=Chen%2C+Y">Yu-Fang Chen</a>, <a href="/search/cs?searchtype=author&query=Yan%2C+R">Rongjie Yan</a>, <a href="/search/cs?searchtype=author&query=Jobstmann%2C+B">Barbara Jobstmann</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a>, <a href="/search/cs?searchtype=author&query=Buckl%2C+C">Christian Buckl</a>, <a href="/search/cs?searchtype=author&query=Knoll%2C+A">Alois Knoll</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1107.1383v2-abstract-short" style="display: inline;"> We present algorithms to synthesize component-based systems that are safe and deadlock-free using priorities, which define stateless-precedence between enabled actions. Our core method combines the concept of fault-localization (using safety-game) and fault-repair (using SAT for conflict resolution). For complex systems, we propose three complementary methods as preprocessing steps for priority sy… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1107.1383v2-abstract-full').style.display = 'inline'; document.getElementById('1107.1383v2-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1107.1383v2-abstract-full" style="display: none;"> We present algorithms to synthesize component-based systems that are safe and deadlock-free using priorities, which define stateless-precedence between enabled actions. Our core method combines the concept of fault-localization (using safety-game) and fault-repair (using SAT for conflict resolution). For complex systems, we propose three complementary methods as preprocessing steps for priority synthesis, namely (a) data abstraction to reduce component complexities, (b) alphabet abstraction and #-deadlock to ignore components, and (c) automated assumption learning for compositional priority synthesis. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1107.1383v2-abstract-full').style.display = 'none'; document.getElementById('1107.1383v2-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 7 October, 2011; <span class="has-text-black-bis has-text-weight-semibold">v1</span> submitted 6 July, 2011; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> July 2011. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">Full version of the ATVA'11 paper (compared to the 1st arXiv version, we add one additional sentence to avoid confusion)</span> </p> </li> <li class="arxiv-result"> <div class="is-marginless"> <p class="list-title is-inline-block"><a href="https://arxiv.org/abs/1011.0268">arXiv:1011.0268</a> <span> [<a href="https://arxiv.org/pdf/1011.0268">pdf</a>, <a href="https://arxiv.org/format/1011.0268">other</a>] </span> </p> <div class="tags is-inline-block"> <span class="tag is-small is-link tooltip is-tooltip-top" data-tooltip="Computer Science and Game Theory">cs.GT</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Distributed, Parallel, and Cluster Computing">cs.DC</span> <span class="tag is-small is-grey tooltip is-tooltip-top" data-tooltip="Software Engineering">cs.SE</span> </div> </div> <p class="title is-5 mathjax"> A Game-theoretic Approach for Synthesizing Fault-Tolerant Embedded Systems </p> <p class="authors"> <span class="search-hit">Authors:</span> <a href="/search/cs?searchtype=author&query=Cheng%2C+C">Chih-Hong Cheng</a>, <a href="/search/cs?searchtype=author&query=Ruess%2C+H">Harald Ruess</a>, <a href="/search/cs?searchtype=author&query=Knoll%2C+A">Alois Knoll</a>, <a href="/search/cs?searchtype=author&query=Buckl%2C+C">Christian Buckl</a> </p> <p class="abstract mathjax"> <span class="has-text-black-bis has-text-weight-semibold">Abstract</span>: <span class="abstract-short has-text-grey-dark mathjax" id="1011.0268v1-abstract-short" style="display: inline;"> In this paper, we present an approach for fault-tolerant synthesis by combining predefined patterns for fault-tolerance with algorithmic game solving. A non-fault-tolerant system, together with the relevant fault hypothesis and fault-tolerant mechanism templates in a pool are translated into a distributed game, and we perform an incomplete search of strategies to cope with undecidability. The resu… <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1011.0268v1-abstract-full').style.display = 'inline'; document.getElementById('1011.0268v1-abstract-short').style.display = 'none';">▽ More</a> </span> <span class="abstract-full has-text-grey-dark mathjax" id="1011.0268v1-abstract-full" style="display: none;"> In this paper, we present an approach for fault-tolerant synthesis by combining predefined patterns for fault-tolerance with algorithmic game solving. A non-fault-tolerant system, together with the relevant fault hypothesis and fault-tolerant mechanism templates in a pool are translated into a distributed game, and we perform an incomplete search of strategies to cope with undecidability. The result of the game is translated back to executable code concretizing fault-tolerant mechanisms using constraint solving. The overall approach is implemented to a prototype tool chain and is illustrated using examples. <a class="is-size-7" style="white-space: nowrap;" onclick="document.getElementById('1011.0268v1-abstract-full').style.display = 'none'; document.getElementById('1011.0268v1-abstract-short').style.display = 'inline';">△ Less</a> </span> </p> <p class="is-size-7"><span class="has-text-black-bis has-text-weight-semibold">Submitted</span> 1 November, 2010; <span class="has-text-black-bis has-text-weight-semibold">originally announced</span> November 2010. </p> <p class="comments is-size-7"> <span class="has-text-black-bis has-text-weight-semibold">Comments:</span> <span class="has-text-grey-dark mathjax">The extended version of the paper "Synthesis of Fault-Tolerant Embedded Systems using Games: from Theory to Practice" in VMCAI'11</span> </p> </li> </ol> <div class="is-hidden-tablet">  <span class="help" style="display: inline-block;"><a href="https://github.com/arXiv/arxiv-search/releases">Search v0.5.6 released 2020-02-24</a>  </span> </div> </div> </main> <footer> <div class="columns is-desktop" role="navigation" aria-label="Secondary">  <div class="column"> <div class="columns"> <div class="column"> <ul class="nav-spaced"> <li><a href="https://info.arxiv.org/about">About</a></li> <li><a href="https://info.arxiv.org/help">Help</a></li> </ul> </div> <div class="column"> <ul class="nav-spaced"> <li> <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512" class="icon filter-black" role="presentation"><title>contact arXiv</title><desc>Click here to contact arXiv</desc><path d="M502.3 190.8c3.9-3.1 9.7-.2 9.7 4.7V400c0 26.5-21.5 48-48 48H48c-26.5 0-48-21.5-48-48V195.6c0-5 5.7-7.8 9.7-4.7 22.4 17.4 52.1 39.5 154.1 113.6 21.1 15.4 56.7 47.8 92.2 47.6 35.7.3 72-32.8 92.3-47.6 102-74.1 131.6-96.3 154-113.7zM256 320c23.2.4 56.6-29.2 73.4-41.4 132.7-96.3 142.8-104.7 173.4-128.7 5.8-4.5 9.2-11.5 9.2-18.9v-19c0-26.5-21.5-48-48-48H48C21.5 64 0 85.5 0 112v19c0 7.4 3.4 14.3 9.2 18.9 30.6 23.9 40.7 32.4 173.4 128.7 16.8 12.2 50.2 41.8 73.4 41.4z"/></svg> <a href="https://info.arxiv.org/help/contact.html"> Contact</a> </li> <li> <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512" class="icon filter-black" role="presentation"><title>subscribe to arXiv mailings</title><desc>Click here to subscribe</desc><path d="M476 3.2L12.5 270.6c-18.1 10.4-15.8 35.6 2.2 43.2L121 358.4l287.3-253.2c5.5-4.9 13.3 2.6 8.6 8.3L176 407v80.5c0 23.6 28.5 32.9 42.5 15.8L282 426l124.6 52.2c14.2 6 30.4-2.9 33-18.2l72-432C515 7.8 493.3-6.8 476 3.2z"/></svg> <a href="https://info.arxiv.org/help/subscribe"> Subscribe</a> </li> </ul> </div> </div> </div>   <div class="column"> <div class="columns"> <div class="column"> <ul class="nav-spaced"> <li><a href="https://info.arxiv.org/help/license/index.html">Copyright</a></li> <li><a href="https://info.arxiv.org/help/policies/privacy_policy.html">Privacy Policy</a></li> </ul> </div> <div class="column sorry-app-links"> <ul class="nav-spaced"> <li><a href="https://info.arxiv.org/help/web_accessibility.html">Web Accessibility Assistance</a></li> <li> <p class="help"> <a class="a11y-main-link" href="https://status.arxiv.org" target="_blank">arXiv Operational Status <svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 256 512" class="icon filter-dark_grey" role="presentation"><path d="M224.3 273l-136 136c-9.4 9.4-24.6 9.4-33.9 0l-22.6-22.6c-9.4-9.4-9.4-24.6 0-33.9l96.4-96.4-96.4-96.4c-9.4-9.4-9.4-24.6 0-33.9L54.3 103c9.4-9.4 24.6-9.4 33.9 0l136 136c9.5 9.4 9.5 24.6.1 34z"/></svg></a><br> Get status notifications via <a class="is-link" href="https://subscribe.sorryapp.com/24846f03/email/new" target="_blank"><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 512 512" class="icon filter-black" role="presentation"><path d="M502.3 190.8c3.9-3.1 9.7-.2 9.7 4.7V400c0 26.5-21.5 48-48 48H48c-26.5 0-48-21.5-48-48V195.6c0-5 5.7-7.8 9.7-4.7 22.4 17.4 52.1 39.5 154.1 113.6 21.1 15.4 56.7 47.8 92.2 47.6 35.7.3 72-32.8 92.3-47.6 102-74.1 131.6-96.3 154-113.7zM256 320c23.2.4 56.6-29.2 73.4-41.4 132.7-96.3 142.8-104.7 173.4-128.7 5.8-4.5 9.2-11.5 9.2-18.9v-19c0-26.5-21.5-48-48-48H48C21.5 64 0 85.5 0 112v19c0 7.4 3.4 14.3 9.2 18.9 30.6 23.9 40.7 32.4 173.4 128.7 16.8 12.2 50.2 41.8 73.4 41.4z"/></svg>email</a> or <a class="is-link" href="https://subscribe.sorryapp.com/24846f03/slack/new" target="_blank"><svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 448 512" class="icon filter-black" role="presentation"><path d="M94.12 315.1c0 25.9-21.16 47.06-47.06 47.06S0 341 0 315.1c0-25.9 21.16-47.06 47.06-47.06h47.06v47.06zm23.72 0c0-25.9 21.16-47.06 47.06-47.06s47.06 21.16 47.06 47.06v117.84c0 25.9-21.16 47.06-47.06 47.06s-47.06-21.16-47.06-47.06V315.1zm47.06-188.98c-25.9 0-47.06-21.16-47.06-47.06S139 32 164.9 32s47.06 21.16 47.06 47.06v47.06H164.9zm0 23.72c25.9 0 47.06 21.16 47.06 47.06s-21.16 47.06-47.06 47.06H47.06C21.16 243.96 0 222.8 0 196.9s21.16-47.06 47.06-47.06H164.9zm188.98 47.06c0-25.9 21.16-47.06 47.06-47.06 25.9 0 47.06 21.16 47.06 47.06s-21.16 47.06-47.06 47.06h-47.06V196.9zm-23.72 0c0 25.9-21.16 47.06-47.06 47.06-25.9 0-47.06-21.16-47.06-47.06V79.06c0-25.9 21.16-47.06 47.06-47.06 25.9 0 47.06 21.16 47.06 47.06V196.9zM283.1 385.88c25.9 0 47.06 21.16 47.06 47.06 0 25.9-21.16 47.06-47.06 47.06-25.9 0-47.06-21.16-47.06-47.06v-47.06h47.06zm0-23.72c-25.9 0-47.06-21.16-47.06-47.06 0-25.9 21.16-47.06 47.06-47.06h117.84c25.9 0 47.06 21.16 47.06 47.06 0 25.9-21.16 47.06-47.06 47.06H283.1z"/></svg>slack</a> </p> </li> </ul> </div> </div> </div>  </div> </footer> <script src="https://static.arxiv.org/static/base/1.0.0a5/js/member_acknowledgement.js"></script> </body> </html>

CINXE.COM

Search | arXiv e-print repository