{"id":1160,"date":"2014-11-10T08:13:55","date_gmt":"2014-11-09T23:13:55","guid":{"rendered":"http:\/\/www.nil.co.jp\/Japanese\/blog\/?p=1160"},"modified":"2014-11-10T08:13:55","modified_gmt":"2014-11-09T23:13:55","slug":"kaos-91-%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-3","status":"publish","type":"post","link":"https:\/\/www.nil.co.jp\/Japanese\/blog\/?p=1160","title":{"rendered":"KAOS (91) \u904e\u7a0b\u30d9\u30fc\u30b9\u306e\u4ed5\u69d8 (4.4.2-3)"},"content":{"rendered":"

\u6642\u76f8\u8ad6\u7406\u306b\u306f\uff0c\u69d8\u3005\u306a\u30bf\u30a4\u30d7\u304c\u3042\u308b\uff0e\u6642\u9593\u3092\u96e2\u6563\u7684\u3068\u6349\u3048\u308b\u304b\u30fb\u9023\u7d9a\u7684\u3068\u6349\u3048\u308b\u304b\uff0e\u672a\u6765\u306e\u307f\u3092\u6271\u3046\u304b\u30fb\u904e\u53bb\u3082\u6271\u3046\u304b\uff0e\u6642\u9593\u306e\u5206\u5c90\uff08\u53ef\u80fd\u306a\u672a\u6765\uff09\u3092\u30e2\u30c7\u30eb\u5316\u3059\u308b\u304b\u5426\u304b\uff0e<\/p>\n

\u3053\u3053\u3067\u306f\uff0c\u8981\u6c42\u306b\u95a2\u9023\u3057\u305d\u3046\u306a\u57fa\u672c\u7684\u306a\u3068\u3053\u308d\u306e\u307f\u3092\u6271\u3046\uff0e\u307e\u305f\uff0c\u3053\u3053\u3067\u306f\uff0c\u6642\u9593\u8ef8\u4e0a\u306e\u9806\u756a\u306e\u307f\u3092\u554f\u984c\u306b\u3059\u308b\uff0e3msec\u304b\u3089 5msec\u306e\u9593\u3068\u3044\u3063\u305f\u6642\u9593\u3092\u8ad6\u7406\u3067\u6271\u3046\u3053\u3068\u306f\u96e3\u3057\u3044\uff0e<\/p>\n

\u3053\u3053\u3067\u306f\uff0cManna\u6c0f\u3068Pnueli\u6c0f\u306b\u3088\u308b\u6559\u79d1\u66f8[ref]Pnueli, Amir, and Zohar Manna. “The temporal logic of reactive and concurrent systems.” , 1992.[\/ref]\u304b\u3089\uff0e<\/p>\n

\u3044\u307e\uff0c\u72b6\u614b\u306e\u5217\u3092\u03c3\u3068\u3057\uff0c\u305d\u306e j \u756a\u76ee\u304c\u5f0f \u03c6 \u3092\u6e80\u8db3\u3057\u3066\u3044\u308b\u3068\u304d\uff0c\u6b21\u306e\u69d8\u306b\u8a18\u8ff0\u3059\u308b\u3053\u3068\u3068\u3059\u308b\uff0e<\/p>\n

(\u03c3, j)\u00a0\u22a7 \u03c6.<\/p>\n

\u300c\u5426\u5b9a\u300d\u6f14\u7b97\u5b50\u3000\u00ac<\/strong><\/p>\n

(\u03c3, \u00a0j) \u00a0\u22a7 \u00ac\u03c6 \u00a0 iff \u00a0 (\u03c3, \u00a0j) \u22ad \u03c6.<\/p>\n

\u00a0j \u756a\u76ee\u304c p \u3067\u306a\u3044\u3068\u3044\u3046\u3053\u3068\u306f\uff0cp \u3067\u3042\u308b\u3053\u3068\u304c\u6b63\u3057\u304f\u306a\u3044\uff0e\u201diff C\u201d \u306f\u300c\u3082\u3057\uff0cC \u306a\u3089\u3070\uff0c\u304b\u3064 C \u306e\u6642\u306b\u9650\u308a\u300d\u3068\u3044\u3046\u610f\u5473\u3067\u3042\u308b\uff0e\u3044\u308f\u3086\u308b\u5fc5\u8981\u5341\u5206\u6761\u4ef6\u3092\u793a\u3059\uff0e<\/p>\n

\u300c\u9078\u8a00\u300d\u6f14\u7b97\u5b50\u3000 \u2228\u00a0<\/strong><\/p>\n

(\u03c3, j) \u00a0 \u22a7 \u00a0 \u03c6 \u2228 \u03c8 \u00a0 iff \u00a0 (\u03c3, \u00a0j) \u22a7 \u03c6 or\u00a0(\u03c3, j)\u00a0\u22a7 \u03c8.<\/p>\n

\u3053\u308c\u3082\u554f\u984c\u306a\u3044\u3068\u601d\u3046\uff0e\u5426\u5b9a\u3068\u9078\u8a00\u304b\u3089\uff0c\u2227\uff08\u9023\u8a00\uff09\uff0c\u2192\uff08\u542b\u610f\uff09\uff0c\u2194\uff08\u540c\u7b49\uff09\u3082\u5c0e\u51fa\u3067\u304d\u308b\uff0e<\/p>\n

\n
\n
\n

\u2194\uff08equivalence\uff09\u306f\u59cb\u3081\u3066\u304b\u3082\u3057\u308c\u306a\u3044\uff0e\u6b21\u306e\u610f\u5473\u3067\u3042\u308b\uff0eA\u2194B \u2261 (A\u2192B) \u2227 (B \u2192A)<\/p>\n<\/div>\n<\/div>\n<\/div>\n

\u300c\u6b21\u300d\u6f14\u7b97\u5b50\u3000\u25cb<\/strong><\/p>\n

\u3053\u3053\u304b\u3089\uff0c\u6642\u76f8\u8ad6\u7406\u7279\u6709\u306e\u8a18\u53f7\u306e\u4f7f\u3044\u65b9\u3067\u3042\u308b\uff0e<\/p>\n

(\u03c3, j)\u00a0\u22a7 \u25cb \u03c6 \u00a0 iff \u00a0 (\u03c3, j+1)\u00a0\u22a7 \u03c6.<\/p>\n

p \u306e\u6b21\u306e\u72b6\u614b\u3092\u6307\u3059\uff0e\u7c21\u5358\u306a\u4f8b\u3060\u3068\u6b21\u306b\u306a\u308b\uff0e\u300c\u60b2\u3057\u3044\u300d\u2227 \u00ac\u300c\u91d1\u92ad\u7684\u306b\u6075\u307e\u308c\u3066\u3044\u308b\u300d\u21d2\u3000\u25cb\u300c\u60b2\u3057\u3044\u300d<\/p>\n

\u300c\u21d2\u300d\u306e\u610f\u5473\u306f\uff0c\u5f8c\u306b\u8a18\u8ff0\u3059\u308b\uff0e<\/p>\n

\u7c21\u5358\u306a\u3088\u3046\u3067\uff0c\u5c11\u3057\u9593\u9055\u3048\u3084\u3059\u3044\uff0e\u3082\u3046\u5c11\u3057\u8907\u96d1\u306a\u4f8b\u3092\u8003\u3048\u308b\uff0e(x=0) \u2227\u25cb(x=1)\u306e\u771f\u507d\u304c\u3069\u3046\u5909\u5316\u3059\u308b\u304b\u3092\u8003\u3048\u3066\u307f\u308b\uff0e\u72b6\u614b\u5217\u306e\u756a\u53f7\u3068 x \u3092\u6df7\u540c\u3057\u306a\u3044\u3088\u3046\u306b\uff0e<\/p>\n\n\n\n\n\n\n\n\n
\u300c(x=0) \u2227\u25cb(x=1)\u300d\u771f\u7406\u5024\u8868<\/caption>\n
j<\/td>\n0<\/td>\n1<\/td>\n2<\/td>\n3<\/td>\n4<\/td>\n5<\/td>\n6<\/td>\n<\/tr>\n
x<\/td>\n0<\/td>\n0<\/td>\n1<\/td>\n1<\/td>\n0<\/td>\n0<\/td>\n1<\/td>\n<\/tr>\n
x = 0<\/td>\nT<\/td>\nT<\/td>\nF<\/td>\nF<\/td>\nT<\/td>\nT<\/td>\nF<\/td>\n<\/tr>\n
x = 1<\/td>\nF<\/td>\nF<\/td>\nT<\/td>\nT<\/td>\nF<\/td>\nF<\/td>\nT<\/td>\n<\/tr>\n
\u25cb (x=1)<\/td>\nF<\/td>\nT<\/td>\nT<\/td>\nF<\/td>\nF<\/td>\nT<\/td>\nT<\/td>\n<\/tr>\n
(x=0) \u2227\u25cb(x=1)<\/td>\nF<\/td>\nT<\/td>\nF<\/td>\nF<\/td>\nF<\/td>\nT<\/td>\nF<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

\u6a2a\u8ef8\u304c\u6642\u9593\u306e\u9032\u884c\u3092\u793a\u3057\u3066\u3044\u308b\uff0ex\u306e\u5024\u306f\uff0c\u9069\u5f53\u306b\u4e0e\u3048\u3066\u3044\u308b\uff0e\u25cb(x=1) \u306f\uff0cx=1 \u306e\u6b21\u306e\u72b6\u614b\u3067\u3042\u308b\u304b\u3089\uff0c\u4e00\u3064\u5148\u3092\u898b\u308b\uff0ex = 1 \u306e\u771f\u507d\u3092\u4e00\u3064\u5148\u53d6\u308a\u3059\u308b\u3053\u3068\u306b\u306a\u308b\uff0e<\/p>\n

\u6b21\u56de\u306f\uff0c\u672a\u6765\u306b\u95a2\u3059\u308b\u6f14\u7b97\u5b50\u306e\u6b8b\u308a\u3067\u3042\u308b\uff0e<\/p>\n

(nil)<\/em><\/p>\n","protected":false},"excerpt":{"rendered":"

\u6642\u76f8\u8ad6\u7406\u306b\u306f\uff0c\u69d8\u3005\u306a\u30bf\u30a4\u30d7\u304c\u3042\u308b\uff0e\u6642\u9593\u3092\u96e2\u6563\u7684\u3068\u6349\u3048\u308b\u304b\u30fb\u9023\u7d9a\u7684\u3068\u6349\u3048\u308b\u304b\uff0e\u672a\u6765\u306e\u307f\u3092\u6271\u3046\u304b\u30fb\u904e\u53bb\u3082\u6271\u3046\u304b\uff0e\u6642\u9593\u306e\u5206\u5c90\uff08\u53ef\u80fd\u306a\u672a\u6765\uff09\u3092\u30e2\u30c7\u30eb\u5316\u3059\u308b\u304b\u5426\u304b\uff0e \u3053\u3053\u3067\u306f\uff0c\u8981\u6c42\u306b\u95a2\u9023\u3057\u305d\u3046\u306a\u57fa\u672c\u7684\u306a\u3068\u3053\u308d\u306e\u307f\u3092\u6271\u3046\uff0e\u307e\u305f\uff0c\u3053\u3053 […]<\/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":[79],"class_list":["post-1160","post","type-post","status-publish","format-standard","hentry","category-kaos","category-40","category-requirements","category-re","tag-79"],"_links":{"self":[{"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=\/wp\/v2\/posts\/1160","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=1160"}],"version-history":[{"count":20,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=\/wp\/v2\/posts\/1160\/revisions"}],"predecessor-version":[{"id":1233,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=\/wp\/v2\/posts\/1160\/revisions\/1233"}],"wp:attachment":[{"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=1160"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=1160"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=1160"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}