{"id":1263,"date":"2014-11-18T07:49:06","date_gmt":"2014-11-17T22:49:06","guid":{"rendered":"http:\/\/www.nil.co.jp\/Japanese\/blog\/?p=1263"},"modified":"2014-11-18T07:49:06","modified_gmt":"2014-11-17T22:49:06","slug":"kaos-99-%e9%81%8e%e7%a8%8b%e3%83%99%e3%83%bc%e3%82%b9%e3%81%ae%e4%bb%95%e6%a7%98-4-4-2-11","status":"publish","type":"post","link":"https:\/\/www.nil.co.jp\/Japanese\/blog\/?p=1263","title":{"rendered":"KAOS (99) \u904e\u7a0b\u30d9\u30fc\u30b9\u306e\u4ed5\u69d8 (4.4.2-11)"},"content":{"rendered":"<p>\u3053\u308c\u307e\u3067\u306e\u4f8b\u3067\u898b\u305f\u3088\u3046\u306b\uff0c\u6642\u76f8\u8ad6\u7406\u306b\u3088\u308a\uff0c\u81ea\u7136\u8a00\u8a9e\u306b\u8fd1\u3044\u5f62\u3067\u8981\u6c42\u3084\u524d\u63d0\u3092\u8a18\u8ff0\u3059\u308b\u3053\u3068\u304c\u3067\u304d\u308b\u3053\u3068\u304c\u5206\u304b\u308b\uff0e\u4e00\u65b9\u3067\uff0c\u5e38\u306b\u81ea\u7136\u306b\u8a18\u8ff0\u3067\u304d\u308b\u3068\u3044\u3046\u308f\u3051\u3067\u306f\u306a\u3044\uff0e\u5c11\u3057\u8907\u96d1\u306a\u5f0f\u306b\u306a\u308b\u3068\uff0c\u76f4\u611f\u7684\u306b\u610f\u5473\u3092\u3068\u308a\u3065\u3089\u304f\u306a\u308b\uff0e<\/p>\n<p>\u5bfe\u51e6\u306e\u65b9\u6cd5\u3068\u3057\u3066\uff0c\u539f\u66f8\u3067\u306f\uff0c\u8a18\u8ff0\u30d1\u30bf\u30fc\u30f3[ref]\u00a0Dwyer, Matthew B., George S. Avrunin, and James C. Corbett. &#8220;Patterns in property specifications for finite-state verification.&#8221;,\u00a0<i>\u00a0Proceedings of the 1999 International Conference on<\/i>. IEEE, 1999.[\/ref]\u3092\u7d39\u4ecb\u3057\u3066\u3044\u308b\uff0e<\/p>\n<p>\u3053\u308c\u306f\uff0c\u8981\u6c42\u4ed5\u69d8\u306b\u826f\u304f\u51fa\u3066\u304f\u308b\u81ea\u7136\u8a00\u8a9e\u8868\u73fe\u3092\uff0cLTL \u5f0f\u3084 CTL \u5f0f\u306b\u7f6e\u304d\u63db\u3048\u308b\u305f\u3081\u306e\u30d1\u30bf\u30fc\u30f3\u3067\u3042\u308b\uff0e\u4f8b\u3048\u3070\uff0c\u300c\u5148\u884c\u3059\u308b\u300d\u306b\u3064\u3044\u3066\u8003\u3048\u308b\uff0e<\/p>\n<p>\u5e38\u306b\uff0c\u300cS \u304c P \u306b\u5148\u884c\u3059\u308b\u300d\u306e\u3067\u3042\u308c\u3070\uff0c\u6b21\u306e\u69d8\u306b\u30d1\u30bf\u30fc\u30f3\u5316\u3067\u304d\u308b\uff08\u3053\u3053\u3067\u306f LTL \u5f0f\u306e\u307f\u3092\u8a18\u8f09\u3059\u308b\uff0e\u3082\u3068\u306e\u8ad6\u6587\u3067\u306f\uff0c\u3088\u304f\u3042\u308b\u6642\u9593\u8a18\u8ff0\u306e\u30d1\u30bf\u30fc\u30f3\u306b\u5bfe\u3057\u3066\uff0cCTL\u3068\u7b46\u8005\u305f\u3061\u304c\u9650\u91cf\u6b63\u898f\u8868\u73fe\uff08quantified reqular expression\uff09\u3068\u547c\u3076\u65b9\u6cd5\u3067\u3082\u8868\u73fe\u3057\u3066\u3044\u308b\uff09\uff0e<\/p>\n<p style=\"padding-left: 30px;\">\u25c7 P \u2192 (\u00acP U (S\u2227\u00acP))<\/p>\n<p style=\"padding-left: 30px;\">\u4e26\u3073\u3068\u3057\u3066\u306f\uff0c S, P \u3067\u3042\u308b\uff0e\u3044\u3064\u304b\u306f\uff0cP \u306b\u306a\u308b\u304c\uff0cS \u306b\u306a\u308b\u307e\u3067\u306f P \u306f\u507d\u3067\u306a\u304f\u3066\u306f\u306a\u3089\u306a\u3044\uff0e\u304b\u3064\uff0cS\u3068\u306a\u3063\u305f\u5834\u5408\u3067\u3082\uff0cP\u306f\u507d\u3067\u306a\u304f\u3066\u306f\u306a\u3089\u306a\u3044\uff0e<\/p>\n<p style=\"padding-left: 30px;\">\u4e00\u3064\u306e\u7f6e\u304d\u63db\u3048\u3068\u3057\u3066\u59a5\u5f53\u3067\u3042\u308b\u3053\u3068\u304c\u308f\u304b\u308b\uff0e\u4ee5\u5f8c\u3082\u30d1\u30bf\u30fc\u30f3\u3092\u793a\u3059\u304c\uff0c\u7279\u306b\u89e3\u8aac\u306f\u52a0\u3048\u306a\u3044\u306e\u3067\uff0cLTL\u306e\u7df4\u7fd2\u3068\u3044\u3046\u3053\u3068\u3067\u8aad\u307f\u53d6\u3063\u3066\u6b32\u3057\u3044\uff0e<\/p>\n<p>\u6b21\u306f\uff0cR\u306e\u524d\u3067\u306f\uff0c\u300cS \u304c P \u306b\u5148\u884c\u3059\u308b\u300d\u5834\u5408\u3067\u3042\u308b\uff0e<\/p>\n<p style=\"padding-left: 30px;\">\u25c7R \u2192 (\u00acP U (S \u00a0\u2228 \u00a0R))<\/p>\n<p>\u9006\u306b\uff0cQ\u4ee5\u5f8c\uff0c\u300cS \u304c P \u306b\u5148\u884c\u3059\u308b\u300d\u5834\u5408\u306f\uff0c\u6b21\u306b\u306a\u308b\uff0e<\/p>\n<p style=\"padding-left: 30px;\">\u25a1\u00acQ \u00a0\u2228 \u00a0\u25c7 (Q \u2227 \u25c7 (\u00acP U (S \u00a0\u2228 \u25a1\u00acP)))<\/p>\n<p>Q\u3068R\u306e\u9593\u3067\uff0c\u300cS \u304c P \u306b\u5148\u884c\u3059\u308b\u300d\u5834\u5408\u306f\u6b21\u306b\u306a\u308b\uff0e<\/p>\n<p style=\"padding-left: 30px;\">\u25a1((Q \u2227\u25c7R) \u2192 (\u00acP U (S \u00a0\u2228 \u00a0R)))<\/p>\n<p style=\"padding-left: 30px;\">Q\u4ee5\u964d\uff0cR\u307e\u3067\u306e\u9593\u3067\uff0c\u300cS \u304c P \u306b\u5148\u884c\u3059\u308b\u300d\u5834\u5408\u306f\uff0c\u6b21\u306b\u306a\u308b\uff0e<\/p>\n<p style=\"padding-left: 30px;\">\u25a1(Q \u2192 \u00a0((\u00acP U (S \u00a0\u2228 \u00a0R)) \u00a0\u2228 \u00a0\u25a1\u00acP))<\/p>\n<p style=\"text-align: right;\"><em>(nil)<\/em><\/p>\n","protected":false},"excerpt":{"rendered":"<p>\u3053\u308c\u307e\u3067\u306e\u4f8b\u3067\u898b\u305f\u3088\u3046\u306b\uff0c\u6642\u76f8\u8ad6\u7406\u306b\u3088\u308a\uff0c\u81ea\u7136\u8a00\u8a9e\u306b\u8fd1\u3044\u5f62\u3067\u8981\u6c42\u3084\u524d\u63d0\u3092\u8a18\u8ff0\u3059\u308b\u3053\u3068\u304c\u3067\u304d\u308b\u3053\u3068\u304c\u5206\u304b\u308b\uff0e\u4e00\u65b9\u3067\uff0c\u5e38\u306b\u81ea\u7136\u306b\u8a18\u8ff0\u3067\u304d\u308b\u3068\u3044\u3046\u308f\u3051\u3067\u306f\u306a\u3044\uff0e\u5c11\u3057\u8907\u96d1\u306a\u5f0f\u306b\u306a\u308b\u3068\uff0c\u76f4\u611f\u7684\u306b\u610f\u5473\u3092\u3068\u308a\u3065\u3089\u304f\u306a\u308b\uff0e \u5bfe\u51e6\u306e\u65b9\u6cd5\u3068 [&hellip;]<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[21,40,31,10],"tags":[80,79],"class_list":["post-1263","post","type-post","status-publish","format-standard","hentry","category-kaos","category-40","category-requirements","category-re","tag-80","tag-79"],"_links":{"self":[{"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=\/wp\/v2\/posts\/1263","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=1263"}],"version-history":[{"count":5,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=\/wp\/v2\/posts\/1263\/revisions"}],"predecessor-version":[{"id":1285,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=\/wp\/v2\/posts\/1263\/revisions\/1285"}],"wp:attachment":[{"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=1263"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=1263"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=1263"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}