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

\u4eca\u56de\u306f\uff0c\u904e\u53bb\u3092\u793a\u3059\u6f14\u7b97\u5b50\u3067\u3042\u308b\uff0e\u5f15\u304d\u7d9a\u304d\u6559\u79d1\u66f8[ref]Pnueli, Amir, and Zohar Manna. “The temporal logic of reactive and concurrent systems.” , 1992.[\/ref]\u304b\u3089\u4f8b\u3092\u3068\u308b\uff0e\u305f\u3060\uff0c\u8a18\u53f7\u304c\u7279\u6b8a\u3067\u30c6\u30ad\u30b9\u30c8\u3067\u306f\u66f8\u304d\u3065\u3089\u3044\u306e\u3067\uff0c\u8a18\u53f7\u306f\uff0cKAOS\u6559\u79d1\u66f8\u306b\u3042\u308b\u3082\u306e\u3092\u4f7f\u3046\uff0e\u3053\u306e\u3042\u305f\u308a\u306e\u8a18\u53f7\u306e\u8c4a\u5bcc\u3055\u304c\uff0c\u7d75\u6587\u5b57\u306b\u4ef2\u9593\u610f\u8b58\u3092\u611f\u3058\u308b\u3088\u3046\u306b\uff0c\u9b45\u529b\u7684\u306a\u3068\u3053\u308d\u304b\u3082\u3057\u308c\u306a\u3044\uff0e<\/p>\n

\u300c\u524d(Previous)\u300d\u6f14\u7b97\u5b50\u3000\u25cf<\/strong><\/p>\n

\u672a\u6765\u306e\u25cb\u306b\u5bfe\u5fdc\u3059\u308b\uff0e<\/p>\n

(\u03c3, j)\u00a0\u22a7 \u25cf p iff \u00a0 \u00a0j>0 and (\u03c3, j – 1)\u00a0\u22a7\u00a0p.<\/span><\/p>\n

\u4e0b\u8a18\u306f\u300c\u524d\u300d\u6f14\u7b97\u5b50\u306e\u771f\u7406\u5024\u3067\u3042\u308b\uff0e\u30bc\u30ed\u304b\u3089\uff11\u306b\u5909\u5316\u3059\u308b\u5834\u6240\u3092\u793a\u3059\uff0e\u300c\u6b21\u300d\u6f14\u7b97\u5b50\u3082\u5408\u308f\u305b\u3066\u793a\u3057\u3066\u3044\u308b\uff0e\u306a\u304a\uff0c\u771f\u306b\u306a\u308b\u305f\u3081\u306b\u306f\uff0cj>0\u306e\u6761\u4ef6\u304c\u3042\u308b\u306e\u3067\uff0c\u6700\u521d\uff08j=0\uff09\u3067\u306f\uff0c\u7121\u6761\u4ef6\u3067\u507d\u306b\u306a\u308b\uff0e<\/p>\n\n\n\n\n\n\n
\u300c(x=1)\u2227\u25cf(x=0)\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>\n1<\/td>\n1<\/td>\n0<\/td>\n0<\/td>\n1<\/td>\n1<\/td>\n0<\/td>\n<\/tr>\n
(x=1)\u2227\u25cf(x=0)<\/td>\nF<\/td>\nF<\/td>\nF<\/td>\nF<\/td>\nT<\/td>\nF<\/td>\nF<\/td>\n<\/tr>\n
(x=0)\u2227\u25cb(x=1)<\/td>\nF<\/td>\nF<\/td>\nF<\/td>\nT<\/td>\nF<\/td>\nF<\/td>\nF<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

 <\/p>\n

\u300c\u4ee5\u524d(Has-alwasy-been)\u300d\u6f14\u7b97\u5b50 \u25a0<\/strong><\/p>\n

(\u03c3, j)\u00a0\u22a7 \u25a0p \u00a0 iff \u00a0 (\u03c3, k) \u22a7\u00a0p for all k, 0\u00a0\u2264 k\u00a0\u2264 j.<\/span><\/p>\n

\u672a\u6765\u306e\u25a1\u306b\u5bfe\u5fdc\u3059\u308b\uff0e\u300c\u305a\u3063\u3068\uff0cp\u3067\u3042\u3063\u305f\u300d\u3068\u3044\u3046\u3053\u3068\u3092\u610f\u5473\u3059\u308b\uff0e<\/p>\n

\u4ee5\u4e0b\u306b\u4f8b\u3092\u793a\u3059\uff0e<\/p>\n\n\n\n\n\n
\u300c\u25a0 (x \u2264 3)\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>\n1<\/td>\n2<\/td>\n3<\/td>\n4<\/td>\n5<\/td>\n6<\/td>\n7<\/td>\n<\/tr>\n
\u25a0 (x\u00a0\u2264 3)<\/td>\nT<\/td>\nT<\/td>\nT<\/td>\nF<\/td>\nF<\/td>\nF<\/td>\nF<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

\u6642\u523b2\u307e\u3067\u306f\uff0c\u5f0f\u304c\u6210\u7acb\u3057\u3066\u3044\u308b\uff0e<\/p>\n

\u300c\u304b\u3064\u3066(Once)\u300d\u6f14\u7b97\u5b50 \u25c6<\/strong><\/p>\n

(\u03c3, j)\u00a0\u22a7 \u25c6p \u00a0 iff \u00a0\u00a0(\u03c3, k) \u22a7\u00a0p for some\u00a0k, 0\u00a0\u2264 k\u00a0\u2264 j.<\/span><\/p>\n

\u300cp\u3067\u771f\u3042\u3063\u305f\u3053\u3068\u304c\u3042\u308b\u300d\u3068\u3044\u3046\u610f\u5473\u3067\u3042\u308b\uff0e<\/p>\n\n\n\n\n\n
\u300c\u25c6 (x = 4)\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>\n1<\/td>\n2<\/td>\n3<\/td>\n4<\/td>\n5<\/td>\n6<\/td>\n7<\/td>\n<\/tr>\n
\u25c6 (x = 4)<\/td>\nF<\/td>\nF<\/td>\nF<\/td>\nT<\/td>\nT<\/td>\nT<\/td>\nF<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

\u300c\u4ee5\u6765(Since)\u300dS \u6f14\u7b97\u5b50
\n<\/strong><\/p>\n

(\u03c3, j)\u00a0\u22a7 p S q \u00a0 iff \u00a0 0\u00a0\u2264 k\u00a0\u2264 j \u3068\u306a\u308b k \u304c\u3042\u308a\uff0c(\u03c3, k) \u22a7 q \u304c\u6210\u308a\u7acb\u3064\uff0e\u304b\u3064\uff0ck < i \u2264\u00a0j \u3067\uff0c\u5168\u3066\u306e i \u306b\u304a\u3044\u3066 (\u03c3, i)\u00a0\u22a7 p.<\/span><\/p>\n

\u304b\u3064\u3066 q \u306b\u51fa\u4f1a\u3063\u305f\uff0e\u305d\u308c\u4ee5\u964d\u306f p \u3067\u3042\u3063\u305f\uff0eq p … p \u3068\u3044\u3046\u5217\u3092\u8003\u3048\u3066\u3044\u308b\uff0e<\/p>\n

\u6b21\u306f\uff0c(x\u00a0\u2264 6) S (x = 3) \u306e\u4f8b\u3067\u3042\u308b<\/p>\n\n\n\n\n\n\n\n
\u300c(x\u00a0\u2264 6) S (x = 3)\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>\n1<\/td>\n2<\/td>\n3<\/td>\n4<\/td>\n5<\/td>\n6<\/td>\n7<\/td>\n<\/tr>\n
x\u00a0\u2264 6<\/td>\nT<\/td>\nT<\/td>\nT<\/td>\nT<\/td>\nT<\/td>\nT<\/td>\nF<\/td>\n<\/tr>\n
x = 3<\/td>\nF<\/td>\nF<\/td>\nT<\/td>\nF<\/td>\nF<\/td>\nF<\/td>\nF<\/td>\n<\/tr>\n
(x\u00a0\u2264 6) S (x = 3)<\/td>\nF<\/td>\nF<\/td>\nT<\/td>\nT<\/td>\nT<\/td>\nT<\/td>\nF<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

\u300c\uff08\u3088\u308f\u3044\uff09\u4ee5\u6765(Back-to)\u300dB \u6f14\u7b97\u5b50
\n<\/strong><\/p>\n

(\u03c3, j)\u00a0\u22a7 p B q \u00a0 iff \u00a0 (\u03c3, j) \u22a7 p S q \u00a0or \u00a0(\u03c3, j) \u22a7 \u25a0p.<\/span><\/p>\n

\u57fa\u672c\u7684\u306b\u306f\uff0cS\u3068\u540c\u3058\u3067\u3042\u308b\uff0e\u305f\u3060\uff0cq \u306b\u51fa\u4f1a\u308f\u306a\u304f\u3066\u3082\u826f\u3044\uff0e\u305d\u306e\u5834\u5408\u306f\uff0cp \u304c\u7d9a\u3044\u3066\u3044\u305f\uff0e<\/p>\n

\u3061\u3087\u3046\u3069\uff0cU \u306b\u5bfe\u3059\u308bW\u3068\u540c\u69d8\u306e\u95a2\u4fc2\u306b\u3042\u308b\uff0e<\/p>\n

\u6b21\u306e\u771f\u7406\u3092\u8003\u3048\u308b\uff0e(x \u2260\u00a04) \u00a0B \u00a0(x = 6)<\/p>\n\n\n\n\n\n\n\n
\u300c(x \u2260\u00a04) B (x = 6)\u300d\u771f\u7406\u5024\u8868<\/caption>\n
j<\/td>\n0<\/td>\n1<\/td>\n2<\/td>\n3<\/td>\n4<\/td>\n5<\/td>\n6<\/td>\n7<\/td>\n8<\/td>\n<\/tr>\n
x<\/td>\n1<\/td>\n2<\/td>\n3<\/td>\n4<\/td>\n5<\/td>\n6<\/td>\n7<\/td>\n8<\/td>\n9<\/td>\n<\/tr>\n
x \u2260\u00a04<\/td>\nT<\/td>\nT<\/td>\nT<\/td>\nF<\/td>\nT<\/td>\nT<\/td>\nT<\/td>\nT<\/td>\nT<\/td>\n<\/tr>\n
x = 6<\/td>\nF<\/td>\nF<\/td>\nF<\/td>\nF<\/td>\nF<\/td>\nT<\/td>\nF<\/td>\nF<\/td>\nF<\/td>\n<\/tr>\n
(x \u2260\u00a04) B (x = 6)<\/td>\nT<\/td>\nT<\/td>\nT<\/td>\nF<\/td>\nF<\/td>\nT<\/td>\nT<\/td>\nT<\/td>\nT<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n

\u524d\u534a\u306e\u771f\u306e\u90e8\u5206\u306f\uff0c\u25a0 p \u306b\u3088\u308b\uff0e\u5f8c\u534a\u306f\uff0cp S q \u304c\u6a5f\u80fd\u3057\u3066\u3044\u308b\uff0e<\/p>\n

\u4ed6\u306b\u3082\u904e\u53bb\u306e\u6f14\u7b97\u5b50\u306f\u3042\u308b\u304c\uff0c\u57fa\u672c\u7684\u306a\u3082\u306e\u306f\u4e0a\u8a18\u306b\u306a\u308b\uff0e<\/p>\n

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

\u4eca\u56de\u306f\uff0c\u904e\u53bb\u3092\u793a\u3059\u6f14\u7b97\u5b50\u3067\u3042\u308b\uff0e\u5f15\u304d\u7d9a\u304d\u6559\u79d1\u66f8[ref]Pnueli, Amir, and Zohar Manna. “The temporal logic of reactive and concurren […]<\/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-1205","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\/1205","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=1205"}],"version-history":[{"count":15,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=\/wp\/v2\/posts\/1205\/revisions"}],"predecessor-version":[{"id":1241,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=\/wp\/v2\/posts\/1205\/revisions\/1241"}],"wp:attachment":[{"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=1205"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=1205"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.nil.co.jp\/Japanese\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=1205"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}