{"id":1242,"date":"2014-11-17T07:51:00","date_gmt":"2014-11-16T22:51:00","guid":{"rendered":"http:\/\/www.nil.co.jp\/Japanese\/blog\/?p=1242"},"modified":"2014-11-17T07:51:00","modified_gmt":"2014-11-16T22:51:00","slug":"kaos-98-%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-10","status":"publish","type":"post","link":"https:\/\/www.nil.co.jp\/Japanese\/blog\/?p=1242","title":{"rendered":"KAOS (98) \u904e\u7a0b\u30d9\u30fc\u30b9\u306e\u4ed5\u69d8 (4.4.2-10)"},"content":{"rendered":"<p style=\"text-align: justify;\">\u3053\u3053\u307e\u3067\u306f\uff0c\u7dda\u5f62\u6642\u9593\u8ad6\u7406\uff08LTL\uff09\u3068\u547c\u3070\u308c\u308b\u6642\u9593\u3092\u7dda\u5f62\u3067\u30e2\u30c7\u30eb\u5316\u3057\u305f\u3068\u304d\u306e\u6f14\u7b97\u5b50\u306b\u3064\u3044\u3066\u3067\u3042\u3063\u305f\uff0e\u5206\u5c90\u3067\u6642\u9593\u3092\u30e2\u30c7\u30eb\u5316\u3059\u308b\u5834\u5408\u3082\u3042\u308b\uff0e\u4ee3\u8868\u7684\u306a\u3082\u306e\u306b\uff0cCTL\uff08Computation Tree Logic)\u304c\u3042\u308b\uff0e<\/p>\n<p style=\"text-align: justify;\">\u00a0\u6642\u9593\u304c\u5206\u5c90\u3059\u308b\u3068\u3044\u3046\u306e\u306f\uff0c\u4ee5\u524d\u7c21\u5358\u306b\u7d39\u4ecb\u3057\u305f\u69d8\u76f8\u8ad6\u7406\u306b\u610f\u5473\u3092\u4e0e\u3048\u308b\u65b9\u6cd5\u3067\u3042\u308b\u53ef\u80fd\u4e16\u754c\u610f\u5473\u8ad6\u306b\u57fa\u3065\u3044\u3066\u3044\u308b\uff0e<\/p>\n<p style=\"text-align: justify;\">CTL\u3067\u306f\u3053\u308c\u307e\u3067\uff0c\u4f7f\u7528\u3057\u305f\u69d8\u76f8\u8ad6\u7406\u6f14\u7b97\u5b50\u306f\u304a\u304a\u3080\u306d\u6b21\u306e\u69d8\u306b\u5bfe\u5fdc\u3059\u308b\uff0e<\/p>\n<p style=\"text-align: justify; padding-left: 30px;\">\u25cb\u3000\uff1a\u3000X\u3000(neXt)<\/p>\n<p style=\"text-align: justify; padding-left: 30px;\">\u25a1\u3000\uff1a\u3000G\u3000(Global)<\/p>\n<p style=\"text-align: justify; padding-left: 30px;\">\u25c7\u3000\uff1a\u3000F\u3000(Future)<\/p>\n<p style=\"text-align: justify;\">U, W \u306b\u3064\u3044\u3066\u306f\u57fa\u672c\u7684\u306b\u306f\u540c\u3058\uff0e<\/p>\n<p style=\"text-align: justify;\">\u4f46\u3057\uff0c\u3053\u308c\u3089\uff08\u30d1\u30b9\u5f0f\u6f14\u7b97\u5b50\uff09\u306f\u5358\u72ec\u3067\u306f\u7528\u3044\u3089\u308c\u306a\u3044\uff0e\u72b6\u614b\u5f0f\u3092\u69cb\u6210\u3059\u308bA\uff08\u5168\u3066\u306e\u30d1\u30b9\uff09\u304a\u3088\u3073E\uff08\u3042\u308b\u30d1\u30b9\uff09\u3068\u7d44\u307f\u5408\u308f\u305b\u308b\uff0e\u524d\u8005\u306f\u5168\u3066\u306e\u5206\u5c90\u3057\u305f\u30d1\u30b9\u3067\u6210\u7acb\u3059\u308b\u5834\u5408\uff0cE\u306f\u5206\u5c90\u3057\u305f\u3044\u305a\u308c\u304b\u306e\u30d1\u30b9\u3067\u6210\u7acb\u3059\u308b\u5834\u5408\u3067\u3042\u308b\uff08LTL\u3067\u306f\uff0c\u6697\u9ed9\u7684\u306b A \u304c\u4ed8\u52a0\u3055\u308c\u3066\u3044\u308b\u3068\u8003\u3048\u308b\u3053\u3068\u3082\u3067\u304d\u308b\uff09\uff0e<\/p>\n<p style=\"text-align: justify;\">\u5f93\u3063\u3066\uff0c\u5206\u5c90\u578b\u306e\u5834\u5408\uff0c\u6642\u76f8\u8ad6\u7406\u6f14\u7b97\u5b50\u306f\uff0c\u6b21\u306e\u69d8\u306b\u306a\u308b\uff0e<\/p>\n<p style=\"text-align: justify; padding-left: 30px;\">AG \u03c6\u3000\uff1a\u5168\u3066\u306e\u30d1\u30b9\u306b\u304a\u3044\u3066\uff0c\u5e38\u306b \u03c6 \u304c\u6210\u7acb\u3059\u308b\uff0e<\/p>\n<p style=\"text-align: justify; padding-left: 30px;\">EF \u03c6\u3000\uff1a\u3042\u308b\u30d1\u30b9\u306b\u304a\u3044\u3066\uff0c\u3044\u3064\u304b\u306f \u03c6 \u304c\u6210\u7acb\u3059\u308b\uff0e<\/p>\n<p style=\"text-align: justify;\">\u3053\u306eLTL\u3068CTL\u3067\u306f\uff0c\u8868\u73fe\u80fd\u529b\u306b\u4e00\u90e8\u9055\u3044\u304c\u3042\u308b\uff0e<\/p>\n<p style=\"text-align: justify;\">\u4f8b\u3048\u3070\uff0c\u4e0a\u8a18\u306e EF\u03c6 \u306f\uff0cLTL\u3067\u306f\u8868\u73fe\u3067\u304d\u306a\u3044\uff0e\u7dda\u5f62\u3067\u3042\u308b\u304b\u3089\u5f53\u7136\u3067\u3042\u308b\uff0e\u4e00\u65b9\u3067\uff0cLTL\u5f0f\u306e \u25c7\u25a1\u03c6 \u306f\uff0cCTL\u5f0f\u3067\u306f\u8868\u73fe\u3067\u304d\u306a\u3044\uff0e\u985e\u4f3c\u306e\u8868\u73fe\uff1aAF AG \u03c6 \u3067\u306f\uff0c\u5fc5\u305a \u03c6 \u304c\u6210\u7acb\u3057\u306a\u304f\u3066\u306f\u306a\u3089\u306a\u3044\uff0e\u3057\u304b\u3057\uff0cLTL\u5f0f\u3067\u306f\uff0c\u505c\u6b62\u3057\u306a\u3044\u30b7\u30b9\u30c6\u30e0\uff08\u53cd\u5fdc\u578b\u30b7\u30b9\u30c6\u30e0\u306e\u672c\u8cea\u7684\u7279\u5fb4\uff09\u3067\u306f\uff0c\u03c6 \u304c\u771f\u306b\u306a\u308b\u3053\u3068\u3092\u89b3\u5bdf\u3059\u308b\u3053\u3068\u306f\u306a\u3044\uff0e\u5178\u578b\u7684\u306b\u306f\uff0c\u25c7\u25a1 ABORT \u3092\u8003\u3048\u308c\u3070\u826f\u3044\uff0e<\/p>\n<p style=\"text-align: justify;\">\u3053\u306e\u9055\u3044\u304c\uff0c\u8981\u6c42\u66f8\u306e\u8a18\u8ff0\u306b\u304a\u3044\u3066\u306f LTL \u304c\u597d\u307e\u308c\uff0c\u6709\u9650\u6642\u9593\u3067\u7d50\u679c\u3092\u51fa\u3059\u5fc5\u8981\u306e\u3042\u308b\u30e2\u30c7\u30eb\u691c\u67fb\u306b\u304a\u3044\u3066\u306f CTL \u304c\u597d\u307e\u308c\u308b\u7406\u7531\u3068\u306a\u3063\u3066\u3044\u308b[ref]\u7406\u8ad6\u3068\u3057\u3066\u306f\uff0cCTL*\u3068\u547c\u3070\u308c\u308b\u8ad6\u7406\u304c\u305d\u308c\u305e\u308c\u306e\u30b9\u30fc\u30d1\u30bb\u30c3\u30c8\u3068\u3057\u3066\u5b9a\u7fa9\u3055\u308c\u3066\u3044\u308b\uff0e\u30d1\u30b9\u5f0f\u306b\u3082\u30d1\u30b9\u5f0f\u3092\u8a18\u8ff0\u3067\u304d\u308b\u65b9\u5f0f\u3067\u3042\u308b\uff0e\u3057\u304b\u3057\uff0c\u5b9f\u52d9\u4e0a\u306f\uff0c\u3044\u307e\u306e\u3068\u3053\u308d LTL \u306a\u3044\u3057\u306f CTL \u304c\u7528\u3044\u3089\u308c\u3066\u3044\u308b[\/ref]\uff0e<\/p>\n<p style=\"text-align: right;\"><em>(nil)<\/em><\/p>\n<p style=\"text-align: right;\">\n","protected":false},"excerpt":{"rendered":"<p>\u3053\u3053\u307e\u3067\u306f\uff0c\u7dda\u5f62\u6642\u9593\u8ad6\u7406\uff08LTL\uff09\u3068\u547c\u3070\u308c\u308b\u6642\u9593\u3092\u7dda\u5f62\u3067\u30e2\u30c7\u30eb\u5316\u3057\u305f\u3068\u304d\u306e\u6f14\u7b97\u5b50\u306b\u3064\u3044\u3066\u3067\u3042\u3063\u305f\uff0e\u5206\u5c90\u3067\u6642\u9593\u3092\u30e2\u30c7\u30eb\u5316\u3059\u308b\u5834\u5408\u3082\u3042\u308b\uff0e\u4ee3\u8868\u7684\u306a\u3082\u306e\u306b\uff0cCTL\uff08Computation Tree Logic)\u304c\u3042\u308b\uff0e \u00a0\u6642\u9593 [&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":[],"class_list":["post-1242","post","type-post","status-publish","format-standard","hentry","category-kaos","category-40","category-requirements","category-re"],"_links":{"self":[{"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=\/wp\/v2\/posts\/1242","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=1242"}],"version-history":[{"count":10,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=\/wp\/v2\/posts\/1242\/revisions"}],"predecessor-version":[{"id":1267,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=\/wp\/v2\/posts\/1242\/revisions\/1267"}],"wp:attachment":[{"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=1242"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=1242"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=1242"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}