{"id":5001,"date":"2015-09-04T07:18:11","date_gmt":"2015-09-04T05:18:11","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=5001"},"modified":"2015-09-04T07:18:11","modified_gmt":"2015-09-04T05:18:11","slug":"resena-verified-over-approximation-of-the-diameter-of-propositionally-factored-transition-systems","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-verified-over-approximation-of-the-diameter-of-propositionally-factored-transition-systems\/","title":{"rendered":"Rese\u00f1a: Verified over-approximation of the diameter of propositionally factored transition systems"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en  <a href=\"http:\/\/hol-theorem-prover.org\">HOL4<\/a> sobre verificaci\u00f3n titulado <a href=\"http:\/\/users.cecs.anu.edu.au\/~charlesg\/itp2015.pdf\">Verified over-approximation of the diameter of propositionally factored transition systems<\/a>.<\/p>\n<p>Sus autores son<br \/>\n+ <a href=\"http:\/\/ssrg.nicta.com.au\/people\/?cn=Mohammad+Abdulaziz\">Mohammad Abdulaziz<\/a> (del <a href=\"http:\/\/ssrg.nicta.com.au\/\">Software Systems Research Group<\/a> del <a href=\"https:\/\/en.wikipedia.org\/wiki\/NICTA\">NICTA<\/a> en Camberra, Australia),<br \/>\n+ <a href=\"http:\/\/users.cecs.anu.edu.au\/~charlesg\/\">Charles Gretton<\/a> (de la <a href=\"https:\/\/en.wikipedia.org\/wiki\/Australian_National_University\">Australian National University<\/a> en Camberra, Australia) y<br \/>\n+ <a href=\"http:\/\/ssrg.nicta.com.au\/people\/?cn=Michael+Norrish\">Michael Norrish<\/a> (del <a href=\"http:\/\/ssrg.nicta.com.au\/\">Software Systems Research Group<\/a> del <a href=\"https:\/\/en.wikipedia.org\/wiki\/NICTA\">NICTA<\/a> en Camberra, Australia)<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  To guarantee the completeness of bounded model checking (BMC) we require a completeness threshold. The diameter of the Kripke model of the transition system is a valid completeness threshold for BMC of safety properties. The recurrence diameter gives us an upper bound on the diameter for use in practice. Transition systems are usually described using (propositionally) factored representations. Bounds for such lifted representations are calculated in a compositional way, by first identifying and bounding atomic subsystems, and then composing those results according to subsystem dependencies to arrive at a bound for the concrete system. Compositional approaches are invalid when using the diameter to bound atomic subsystems, and valid when using the recurrence diameter. We provide a novel overapproximation of the diameter, called the sublist diameter, that is tighter than the recurrence diameter. We prove that compositional approaches are valid using it to bound atomic subsystems. Those proofs are mechanised in HOL4. We also describe a novel verified compositional bounding technique which provides tighter overall bounds compared to existing bottom-up approaches.\n<\/p><\/blockquote>\n<p>El trabajo se present\u00f3 el 26 de agosto en el <a href=\"http:\/\/www.inf.kcl.ac.uk\/staff\/urbanc\/itp-2015\">ITP 2015<\/a> (<em>The 6th conference on Interactive Theorem Proving<\/em>).<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en HOL4 se encuentra <a href=\"http:\/\/bit.ly\/1JG6E52\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en HOL4 sobre verificaci\u00f3n titulado Verified over-approximation of the diameter of propositionally factored transition systems. Sus autores son + Mohammad Abdulaziz (del Software Systems Research Group del NICTA en Camberra, Australia), + Charles Gretton (de la Australian National University en Camberra, Australia) y + Michael Norrish (del&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[199,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5001"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=5001"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5001\/revisions"}],"predecessor-version":[{"id":5002,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/5001\/revisions\/5002"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=5001"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=5001"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=5001"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}