{"id":2428,"date":"2022-12-16T13:25:53","date_gmt":"2022-12-16T16:25:53","guid":{"rendered":"https:\/\/icc.fcen.uba.ar\/?p=2428"},"modified":"2022-12-16T13:25:53","modified_gmt":"2022-12-16T16:25:53","slug":"assumption-monitoring-of-temporal-task-planning-using-stream-runtime-verification","status":"publish","type":"post","link":"https:\/\/icc.fcen.uba.ar\/en\/assumption-monitoring-of-temporal-task-planning-using-stream-runtime-verification\/","title":{"rendered":"Assumption Monitoring of Temporal Task Planning Using Stream Runtime Verification"},"content":{"rendered":"<div class=\"fusion-fullwidth fullwidth-box fusion-builder-row-1 fusion-flex-container nonhundred-percent-fullwidth non-hundred-percent-height-scrolling\" style=\"--awb-border-radius-top-left:0px;--awb-border-radius-top-right:0px;--awb-border-radius-bottom-right:0px;--awb-border-radius-bottom-left:0px;--awb-flex-wrap:wrap;\" ><div class=\"fusion-builder-row fusion-row fusion-flex-align-items-flex-start fusion-flex-content-wrap\" style=\"max-width:1144px;margin-left: calc(-4% \/ 2 );margin-right: calc(-4% \/ 2 );\"><div class=\"fusion-layout-column fusion_builder_column fusion-builder-column-0 fusion_builder_column_1_1 1_1 fusion-flex-column\" style=\"--awb-bg-size:cover;--awb-width-large:100%;--awb-margin-top-large:0px;--awb-spacing-right-large:1.92%;--awb-margin-bottom-large:20px;--awb-spacing-left-large:1.92%;--awb-width-medium:100%;--awb-order-medium:0;--awb-spacing-right-medium:1.92%;--awb-spacing-left-medium:1.92%;--awb-width-small:100%;--awb-order-small:0;--awb-spacing-right-small:1.92%;--awb-spacing-left-small:1.92%;\"><div class=\"fusion-column-wrapper fusion-column-has-shadow fusion-flex-justify-content-flex-start fusion-content-layout-column\"><div class=\"fusion-text fusion-text-1\"><p>Authors: S. Zudaire, F. Gorostiaga, C. Sanchez, G.Schneider, and S. Uchitel.<\/p>\n<p>Abstract: Temporal task planning uses formal techniques such as reactive synthesis to guarantee that a robot will succeed in its mission. This technique requires certain explicit and implicit assumptions and simplifications about the operating environment of the robot, including its sensors and capabilities. A robot executing a plan can produce a\u00a0silent mission failure, where the user may believe that the mission goals were achieved when instead the assumptions were violated at runtime. This entails that mitigation and remediation opportunities are missed.<br \/>\nMonitoring at runtime can detect complex assumption violations and identify silent failures, but such monitoring requires the ability to describe and detect sophisticated temporal properties together with quantitative and complex data. Additional challenges include ensuring the correctness of the monitors and a correct interplay between the planning execution and the monitors, and that monitors run under constrained environments in terms of resources.<br \/>\nIn this paper we propose a solution based on stream runtime verification, which offers a high-level declarative language to describe sophisticated monitors together with guarantees on the execution time and memory usage. We show how monitors can be combined with temporal planning not only to monitor assumptions but also to support mitigation and remediation in UAV missions. We demonstrate our approach both in real and simulated flights for some typical mission scenarios.<br \/>\nMore information: <a href=\"https:\/\/dl.acm.org\/doi\/abs\/10.1007\/978-3-031-19849-6_23\" target=\"_blank\" rel=\"noopener noreferrer\">https:\/\/dl.acm.org\/doi\/abs\/10.1007\/978-3-031-19849-6_23<\/a><\/p>\n<\/div><\/div><\/div><\/div><\/div>\n","protected":false},"excerpt":{"rendered":"","protected":false},"author":9,"featured_media":2429,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[98],"tags":[],"class_list":["post-2428","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-papers"],"_links":{"self":[{"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/posts\/2428","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/users\/9"}],"replies":[{"embeddable":true,"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/comments?post=2428"}],"version-history":[{"count":1,"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/posts\/2428\/revisions"}],"predecessor-version":[{"id":2430,"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/posts\/2428\/revisions\/2430"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/media\/2429"}],"wp:attachment":[{"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/media?parent=2428"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/categories?post=2428"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/icc.fcen.uba.ar\/en\/wp-json\/wp\/v2\/tags?post=2428"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}