反應式和并發(fā)系統(tǒng)的時序邏輯

 
 
 
第Ⅰ部分并 發(fā) 模 型
第1章基本模型
1.1通用模型
1.1.1基礎語言
1.1.2基本轉(zhuǎn)換系統(tǒng)
1.1.3轉(zhuǎn)換關系ρτ
1.1.4使能與非使能轉(zhuǎn)換
1.1.5空轉(zhuǎn)換與勤勉轉(zhuǎn)換
1.1.6計算
1.1.7具體模型
1.2模型1： 轉(zhuǎn)換圖
1.2.1聲明
1.2.2進程
1.2.3基本轉(zhuǎn)換系統(tǒng)圖
1.2.4用交錯表示并發(fā)性
1.2.5調(diào)度
1.3模型2： 共享變量文本
1.3.1簡單語句
1.3.2復合語句
1.3.3程序
1.3.4文本程序中的標記
1.3.5標記等價關系
1.3.6文本語言中的位置
1.4共享變量文本語義
1.4.1狀態(tài)變量和狀態(tài)
1.4.2轉(zhuǎn)換
1.4.3初始條件
1.4.4計算
1.4.5下標變量
1.5語句間的結(jié)構關系
1.5.1子語句
1.5.2控制謂詞at、after和in
1.5.3語句的使能性
1.5.4進程和并行語句
1.5.5競爭語句
1.6行為等價
1.6.1初步近似
1.6.2可觀測和可簡化的行為
1.6.3轉(zhuǎn)換系統(tǒng)的等價性
1.6.4語句一致性
1.6.5例子
1.6.6模擬與實現(xiàn)
1.7分組語句
1.7.1分組語句
1.7.2與分組語句關聯(lián)的轉(zhuǎn)換
1.8信號量語句
1.8.1信號量需求
1.8.2信號量語句
1.8.3互斥信號量的應用
1.8.4信號量的其他應用
1.9區(qū)域語句
1.9.1比較信號量和區(qū)域語句
1.9.2選擇語句中的同步
1.10模型3： 消息傳遞文本
1.10.1通信語句
1.10.2緩沖能力
1.10.3例子
1.10.4條件通信語句
1.10.5同步模型和異步模型的比較
1.10.6公平服務器
1.11模型4： Petri網(wǎng)
1.11.1網(wǎng)
1.11.2標記
1.11.3圖形化表示
1.11.4點火
1.11.5Petri系統(tǒng)
1.11.6例子
問題
文獻注釋
 
第2章真并發(fā)模型
2.1交錯和并發(fā)
2.1.1重疊執(zhí)行
2.1.2交錯計算
2.1.3細粒度
2.2限制臨界引用
2.2.1臨界引用
2.2.2語句的LCR約束
2.2.3LCR程序
2.2.4需要額外保護
2.2.5每個程序都有一個LCR精化
2.2.6每個程序都有一個LCR等價
2.2.7語義臨界引用
2.2.8合并語句
2.2.9with語句
2.3弱公平性
2.3.1公平性需求
2.3.2不公平計算
2.3.3弱公平性
2.3.4弱公平性需求
2.4弱公平性需求的含義
2.4.1不能保證選擇公平性
2.4.2轉(zhuǎn)換弱公平性與進程弱公平性
2.4.3弱公平性調(diào)度
2.4.4不能檢測弱公平性
2.4.5非公平轉(zhuǎn)換
2.5強公平性
2.5.1弱公平性不足
2.5.2強公平性需求
2.5.3強公平性調(diào)度
2.6同步語句
2.7通信語句
2.7.1同步通信互斥
2.7.2異步通信互斥
2.8總結(jié): 公平轉(zhuǎn)換系統(tǒng)
2.9Petri網(wǎng)公平性
2.9.1弱公平性
2.9.2非一元網(wǎng)轉(zhuǎn)換的強公平性
2.9.3互斥
2.10公平性語義
2.10.1公平性防止有限區(qū)分
2.10.2公平性和隨機選擇
問題
文獻注釋
第Ⅱ部分規(guī)約
第3章時序邏輯
3.1狀態(tài)公式
3.1.1狀態(tài)語言
3.1.2狀態(tài)公式語義
3.2時序公式： 將來算子
3.3時序公式： 過去算子
3.3.1簡單例子
3.3.2可滿足性和有效性
3.3.3等價性、一致性和蘊涵性
3.3.4可替換性
3.3.5過去公式和將來公式
3.3.6的較弱形式
3.3.7算子的基本集合
3.3.8限制型算子
3.4時序算子的基本屬性
3.4.1模式及其有效性
3.4.2單調(diào)性
3.4.3自反性
3.4.4限制性
3.4.5擴展性
3.4.6對偶性
3.4.7強算子和弱算子
3.4.8冪等性
3.4.9吸收性
3.4.10上一時刻和下一時刻的交換性
3.4.11全稱算子和存在算子
3.4.12引用變量的下一個值和前一個值
3.4.13語義弱公平性
3.5證明系統(tǒng)
3.6證明系統(tǒng)公理
3.6.1將來公理
3.6.2過去公理
3.6.3混合公理
3.6.4狀態(tài)重言式公理
3.7基本推理規(guī)則
3.7.1泛化規(guī)則和特指規(guī)則
3.7.2替換規(guī)則
3.7.3分離規(guī)則
3.8導出規(guī)則
3.8.1指定規(guī)則
3.8.2命題推理規(guī)則
3.8.3蘊涵分離規(guī)則
3.8.4蘊涵命題推理規(guī)則
3.8.5從蘊涵到規(guī)則
3.8.6證明舉例
3.9等詞和量詞
3.9.1參數(shù)化的句子符號
3.9.2帶參數(shù)模式的規(guī)則GEN
3.9.3帶量詞公式的規(guī)則INST
3.9.4變量替換
3.9.5等詞公理
3.9.6框架公理
3.9.7證明舉例
3.9.8變量的下一個值和前一個值
3.9.9量詞公理
3.9.10量詞規(guī)則
3.9.11證明舉例
3.10從一般有效性到程序有效性
3.10.1計算對應的模型
3.10.2程序有效性和狀態(tài)有效性
3.10.3擴展演繹系統(tǒng)
3.10.4建立P狀態(tài)有效性
3.10.5建立P有效性
3.10.6程序依賴規(guī)則
3.10.7導出規(guī)則
3.10.8時序語義公理
問題
文獻注釋
第4章程序?qū)傩?br />4.1局部語言
4.1.1位置謂詞
4.1.2轉(zhuǎn)換的使能性
4.1.3終止謂詞
4.1.4轉(zhuǎn)換謂詞
4.1.5通信謂詞
4.1.6規(guī)約變量
4.2屬性分類
4.2.1安全性
4.2.2保證性
4.2.3義務性
4.2.4響應性
4.2.5持續(xù)性
4.2.6反應性
4.2.7反應性類是最大的類
4.2.8分類
4.2.9標準公式
4.2.10安全性活性分類
4.3安全性例子： 狀態(tài)不變性
4.3.1全局不變性
4.3.2部分正確性
4.3.3無死鎖性
4.3.4局部無死鎖性
4.3.5容錯性
4.3.6互斥性
4.3.7通信事件的不變性
4.4安全性例子： 過去不變性
4.4.1單調(diào)性
4.4.2缺乏主動響應
4.4.3無重復輸出
4.4.4先進先出
4.4.5嚴格優(yōu)先性
4.4.6有界超越
4.5進展性例子： 從保證性到反應性
4.5.1終止性和完全正確性
4.5.2保證性事件
4.5.3間歇斷言
4.5.4無個體饑荒和無活鎖
4.5.5可訪問性
4.5.6確保響應
4.5.7最終有界性
4.5.8表示公平性需求
4.5.9最終可靠性
4.6例子： 資源分配
4.6.1消息傳遞方式
4.6.2消息傳遞方式的安全性
4.6.3消息傳遞方式的進展性
4.6.4共享變量方式
4.6.5共享變量方式的安全性
4.6.6共享變量方式的進展性
4.7規(guī)約語言表達能力
4.7.1觀察奇偶性
4.7.2量詞公式描述奇偶性
4.7.3有重復輸入的緩沖
4.7.4量詞公式描述緩沖
4.7.5通信歷史變量
4.8反應模塊規(guī)約
4.8.1模塊語句
4.8.2模塊規(guī)約
4.8.3執(zhí)行模塊的任務
4.8.4模塊實現(xiàn)的障礙
4.8.5模塊的計算
4.9復合模塊規(guī)約
4.9.1層次分解
4.9.2更改超越一次的變量
4.9.3分解安全性規(guī)約
4.9.4異步通信模塊
4.9.5同步通信模塊
4.9.6資源重新分配
問題
文獻注釋
參考文獻