{"id":1276,"date":"2014-01-24T17:18:12","date_gmt":"2014-01-24T16:18:12","guid":{"rendered":"https:\/\/project.inria.fr\/plasma-lab\/?page_id=1276"},"modified":"2015-03-13T11:36:47","modified_gmt":"2015-03-13T10:36:47","slug":"checking-unbounded-a-bltl-properties","status":"publish","type":"page","link":"https:\/\/project.inria.fr\/plasma-lab\/documentation\/algorithms\/checking-unbounded-a-bltl-properties\/","title":{"rendered":"Checking unbounded A-BLTL properties"},"content":{"rendered":"<p>PLASMA Lab can check unbounded properties from the <a href=\"https:\/\/project.inria.fr\/plasma-lab\/property-language\/#ABLTL\">A-BLTL<\/a> logic. The algorithm that is used involved a reachability check of the underlying finite automata model. To do this PLASMA Lab calls the <a href=\"http:\/\/www.prismmodelchecker.org\/\">PRISM<\/a> model-checker. We explain below how to configure PLASMA Lab in order to use this functionality:<\/p>\n<ul>\n<li>Step 1: install <a href=\"http:\/\/www.prismmodelchecker.org\/\">PRISM<\/a> in your system.<\/li>\n<li>Step 2: download the script <a href=\"http:\/\/plasma-lab.gforge.inria.fr\/plasma_lab_bundle\/prism_reach\">prism_reach<\/a>.<\/li>\n<li>Step 3: in the script edit the line with the path to PRISM<\/li>\n<li>Step 4: launch PLASMA Lab with the option &#8216;-Dprism_reach=path&#8217; where &#8216;path&#8217; is the path to the script.\n<\/ul>\n<p><\/p>","protected":false},"excerpt":{"rendered":"<p>PLASMA Lab can check unbounded properties from the A-BLTL logic. The algorithm that is used involved a reachability check of the underlying finite automata model. To do this PLASMA Lab calls the PRISM model-checker. We explain below how to configure PLASMA Lab in order to use this functionality: Step 1:\u2026<\/p>\n<p> <a class=\"continue-reading-link\" href=\"https:\/\/project.inria.fr\/plasma-lab\/documentation\/algorithms\/checking-unbounded-a-bltl-properties\/\"><span>Continue reading<\/span><i class=\"crycon-right-dir\"><\/i><\/a> <\/p>\n","protected":false},"author":235,"featured_media":0,"parent":1585,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-1276","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/1276","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/users\/235"}],"replies":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/comments?post=1276"}],"version-history":[{"count":6,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/1276\/revisions"}],"predecessor-version":[{"id":1814,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/1276\/revisions\/1814"}],"up":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/1585"}],"wp:attachment":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/media?parent=1276"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}