CTL公式与不动点.ppt

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),