{"id":677,"date":"2016-07-21T12:25:22","date_gmt":"2016-07-21T15:25:22","guid":{"rendered":"https:\/\/sbia.org.br\/lnlm\/?page_id=677"},"modified":"2016-07-21T12:25:22","modified_gmt":"2016-07-21T15:25:22","slug":"vol12-no2-art3","status":"publish","type":"page","link":"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/vol12-no2-art3\/","title":{"rendered":"Symbolic Regression for Non-Deterministic Actions"},"content":{"rendered":"<p><strong>T\u00edtulo:<\/strong> Symbolic Regression for Non-Deterministic Actions<\/p>\n<p><strong>Autores:<\/strong> Menezes, Maria Viviane de; Barros, Leliane Nunes de; Pereira, Silvio do Lago<\/p>\n<p align=\"justify\"><strong>Resumo:<\/strong> Model checking (MC) is a widely used approach for verifying if a formal model of a system satisfies a particular temporal logic formula. Symbolic model checking has been largely applied to solve non-deterministic planning problems, an area called planning as model checking. In this approach, the planning domain is the system to be verified and the planning goal is the formula that must be satisfied. In general, the planning domain is given by a set of action specifications given in terms of preconditions and effects formulas and the MC pre-image computation performs some kind of translation of the actions specification into a symbolic representation of the whole state-transition space. However, the symbolic representation of the entire state transition space is a very expensive operation and, in some cases, even using the symbolic representation it is impossible to come up with a plan for large problems. In order to overcome this limitation, one can compute the pre-image of X by using directly the action specification, without representing the whole state-transition space, an operation called symbolic regression. In this paper, we propose new symbolic non-deterministic regression operations based on Quantified Boolean Formulas (QBF) inference, as an extension of previous work on deterministic symbolic planning. In addition, we prove that the regression operations are equivalent to existing pre-image operations.<\/p>\n<p><strong>Palavras-chave:<\/strong> Model Checking; Automated Planning; Non-Deterministic Actions; Temporal Logic<\/p>\n<p><strong>P\u00e1ginas:<\/strong> 17<\/p>\n<p><strong>C\u00f3digo DOI:<\/strong> <a href=\"http:\/\/dx.doi.org\/10.21528\/lnlm-vol12-no2-art3\">10.21528\/lmln-vol12-no2-art3<\/a><\/p>\n<p><strong>Artigo em PDF:<\/strong> <a href=\"https:\/\/sbia.org.br\/lnlm\/wp-content\/uploads\/sites\/4\/2016\/07\/vol12-no2-art3.pdf\" rel=\"\">vol12-no2-art3.pdf<\/a><\/p>\n<p><strong>Arquivo BibTex:<\/strong> <a href=\"https:\/\/sbia.org.br\/lnlm\/wp-content\/uploads\/sites\/4\/2016\/07\/vol12-no2-art3.bib\" rel=\"\">vol12-no2-art3.bib<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>T\u00edtulo: Symbolic Regression for Non-Deterministic Actions Autores: Menezes, Maria Viviane de; Barros, Leliane Nunes de; Pereira, Silvio do Lago Resumo: Model checking (MC) is a widely used approach for verifying if a formal model of a system satisfies a particular <a href=\"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/vol12-no2-art3\/\" class=\"read-more\">Read More &#8230;<\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":669,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-677","page","type-page","status-publish","hentry"],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v26.9 - https:\/\/yoast.com\/product\/yoast-seo-wordpress\/ -->\n<title>Symbolic Regression for Non-Deterministic Actions - Learning and NonLinear Models<\/title>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/vol12-no2-art3\/\" \/>\n<meta property=\"og:locale\" content=\"pt_BR\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"Symbolic Regression for Non-Deterministic Actions - Learning and NonLinear Models\" \/>\n<meta property=\"og:description\" content=\"T\u00edtulo: Symbolic Regression for Non-Deterministic Actions Autores: Menezes, Maria Viviane de; Barros, Leliane Nunes de; Pereira, Silvio do Lago Resumo: Model checking (MC) is a widely used approach for verifying if a formal model of a system satisfies a particular Read More ...\" \/>\n<meta property=\"og:url\" content=\"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/vol12-no2-art3\/\" \/>\n<meta property=\"og:site_name\" content=\"Learning and NonLinear Models\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"Est. tempo de leitura\" \/>\n\t<meta name=\"twitter:data1\" content=\"1 minuto\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/vol12-no2-art3\/\",\"url\":\"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/vol12-no2-art3\/\",\"name\":\"Symbolic Regression for Non-Deterministic Actions - Learning and NonLinear Models\",\"isPartOf\":{\"@id\":\"https:\/\/sbia.org.br\/lnlm\/#website\"},\"datePublished\":\"2016-07-21T15:25:22+00:00\",\"breadcrumb\":{\"@id\":\"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/vol12-no2-art3\/#breadcrumb\"},\"inLanguage\":\"pt-BR\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/vol12-no2-art3\/\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/vol12-no2-art3\/#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"Browse issues\",\"item\":\"https:\/\/sbia.org.br\/lnlm\/publicacoes\/\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"Learning &#038; Nonlinear Models &#8211; L&#038;NLM &#8211; Volume 12 &#8211; N\u00famero 2\",\"item\":\"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/\"},{\"@type\":\"ListItem\",\"position\":3,\"name\":\"Symbolic Regression for Non-Deterministic Actions\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\/\/sbia.org.br\/lnlm\/#website\",\"url\":\"https:\/\/sbia.org.br\/lnlm\/\",\"name\":\"Learning and NonLinear Models\",\"description\":\"\",\"publisher\":{\"@id\":\"https:\/\/sbia.org.br\/lnlm\/#organization\"},\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/sbia.org.br\/lnlm\/?s={search_term_string}\"},\"query-input\":{\"@type\":\"PropertyValueSpecification\",\"valueRequired\":true,\"valueName\":\"search_term_string\"}}],\"inLanguage\":\"pt-BR\"},{\"@type\":\"Organization\",\"@id\":\"https:\/\/sbia.org.br\/lnlm\/#organization\",\"name\":\"Learning and NonLinear Models\",\"url\":\"https:\/\/sbia.org.br\/lnlm\/\",\"logo\":{\"@type\":\"ImageObject\",\"inLanguage\":\"pt-BR\",\"@id\":\"https:\/\/sbia.org.br\/lnlm\/#\/schema\/logo\/image\/\",\"url\":\"https:\/\/sbia.org.br\/lnlm\/wp-content\/uploads\/2021\/07\/logo-lnlm.png\",\"contentUrl\":\"https:\/\/sbia.org.br\/lnlm\/wp-content\/uploads\/2021\/07\/logo-lnlm.png\",\"width\":398,\"height\":94,\"caption\":\"Learning and NonLinear Models\"},\"image\":{\"@id\":\"https:\/\/sbia.org.br\/lnlm\/#\/schema\/logo\/image\/\"}}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"Symbolic Regression for Non-Deterministic Actions - Learning and NonLinear Models","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/vol12-no2-art3\/","og_locale":"pt_BR","og_type":"article","og_title":"Symbolic Regression for Non-Deterministic Actions - Learning and NonLinear Models","og_description":"T\u00edtulo: Symbolic Regression for Non-Deterministic Actions Autores: Menezes, Maria Viviane de; Barros, Leliane Nunes de; Pereira, Silvio do Lago Resumo: Model checking (MC) is a widely used approach for verifying if a formal model of a system satisfies a particular Read More ...","og_url":"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/vol12-no2-art3\/","og_site_name":"Learning and NonLinear Models","twitter_card":"summary_large_image","twitter_misc":{"Est. tempo de leitura":"1 minuto"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/vol12-no2-art3\/","url":"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/vol12-no2-art3\/","name":"Symbolic Regression for Non-Deterministic Actions - Learning and NonLinear Models","isPartOf":{"@id":"https:\/\/sbia.org.br\/lnlm\/#website"},"datePublished":"2016-07-21T15:25:22+00:00","breadcrumb":{"@id":"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/vol12-no2-art3\/#breadcrumb"},"inLanguage":"pt-BR","potentialAction":[{"@type":"ReadAction","target":["https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/vol12-no2-art3\/"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/vol12-no2-art3\/#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"Browse issues","item":"https:\/\/sbia.org.br\/lnlm\/publicacoes\/"},{"@type":"ListItem","position":2,"name":"Learning &#038; Nonlinear Models &#8211; L&#038;NLM &#8211; Volume 12 &#8211; N\u00famero 2","item":"https:\/\/sbia.org.br\/lnlm\/publicacoes\/vol12-no2\/"},{"@type":"ListItem","position":3,"name":"Symbolic Regression for Non-Deterministic Actions"}]},{"@type":"WebSite","@id":"https:\/\/sbia.org.br\/lnlm\/#website","url":"https:\/\/sbia.org.br\/lnlm\/","name":"Learning and NonLinear Models","description":"","publisher":{"@id":"https:\/\/sbia.org.br\/lnlm\/#organization"},"potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/sbia.org.br\/lnlm\/?s={search_term_string}"},"query-input":{"@type":"PropertyValueSpecification","valueRequired":true,"valueName":"search_term_string"}}],"inLanguage":"pt-BR"},{"@type":"Organization","@id":"https:\/\/sbia.org.br\/lnlm\/#organization","name":"Learning and NonLinear Models","url":"https:\/\/sbia.org.br\/lnlm\/","logo":{"@type":"ImageObject","inLanguage":"pt-BR","@id":"https:\/\/sbia.org.br\/lnlm\/#\/schema\/logo\/image\/","url":"https:\/\/sbia.org.br\/lnlm\/wp-content\/uploads\/2021\/07\/logo-lnlm.png","contentUrl":"https:\/\/sbia.org.br\/lnlm\/wp-content\/uploads\/2021\/07\/logo-lnlm.png","width":398,"height":94,"caption":"Learning and NonLinear Models"},"image":{"@id":"https:\/\/sbia.org.br\/lnlm\/#\/schema\/logo\/image\/"}}]}},"_links":{"self":[{"href":"https:\/\/sbia.org.br\/lnlm\/wp-json\/wp\/v2\/pages\/677","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/sbia.org.br\/lnlm\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/sbia.org.br\/lnlm\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/sbia.org.br\/lnlm\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/sbia.org.br\/lnlm\/wp-json\/wp\/v2\/comments?post=677"}],"version-history":[{"count":0,"href":"https:\/\/sbia.org.br\/lnlm\/wp-json\/wp\/v2\/pages\/677\/revisions"}],"up":[{"embeddable":true,"href":"https:\/\/sbia.org.br\/lnlm\/wp-json\/wp\/v2\/pages\/669"}],"wp:attachment":[{"href":"https:\/\/sbia.org.br\/lnlm\/wp-json\/wp\/v2\/media?parent=677"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}