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

第1页 / 共11页

第2页 / 共11页

第3页 / 共11页

第4页 / 共11页

第5页 / 共11页

第6页 / 共11页

第7页 / 共11页

第8页 / 共11页

第9页 / 共11页

第10页 / 共11页

CTL公式与不动点 Still waters run deep.流静水深流静水深,人静心深人静心深 Where there is life, there is hope。有生命必有希望。有生命必有希望2完备偏序完备偏序：最小元、每条链有最小上界有最小元只有有穷链的偏序是完备偏序有最小元的有穷域上的偏序是完备偏序S：有穷域则(2S,)是一个有穷域上的完备偏序3完备偏序(X, )上的函数f是连续的：即对X上的每条链D，连续函数4单调函数只有有穷链的完备偏序上的函数是连续的当且仅当它是单调的有穷域(2S,) 上的函数是连续的当且仅当它是单调的5不动点6EG 和 EU7EG 和 EU8sZ.(pEX Z) sEG p9sZ.(pEX Z) sEG p10sE(pUq) s Z.(q(pEX Z)11sE(pUq) s Z.(q(pEX Z)