CTL公式与不动点-－金锄头文库

第1页 / 共11页

第2页 / 共11页

第3页 / 共11页

第4页 / 共11页

第5页 / 共11页

第6页 / 共11页

第7页 / 共11页

第8页 / 共11页

第9页 / 共11页

第10页 / 共11页

CTL公式与不动点,中国科学院软件研究所张文辉 ,2,完备偏序,完备偏序：最小元、每条链有最小上界有最小元只有有穷链的偏序是完备偏序有最小元的有穷域上的偏序是完备偏序 S：有穷域则(2S,)是一个有穷域上的完备偏序,3,完备偏序(X, )上的函数f是连续的：即对X上的每条链D，,连续函数,4,单调函数,只有有穷链的完备偏序上的函数是连续的当且仅当它是单调的有穷域(2S,) 上的函数是连续的当且仅当它是单调的,5,不动点,6,EG 和 EU,7,EG 和 EU,8,sZ.(pEX Z) sEG p,9,sZ.(pEX Z) sEG p,10,sE(pUq) s Z.(q(pEX Z),11,sE(pUq) s Z.(q(pEX Z),