2.8 参考文献注释

状态机模型的一般概念源于传统的有限状态自动机。关于有限状态自动机的基本内容，可以参考许多大学本科的教材，如Lewis和Papadimitriou[195]以及Martin[221]的著作。这里定义的某种特定的状态机模型是从大量分布式计算理论的论文中提取出来的，如Fischer和Lynch[119]的Byzantine一致性论文。

不变式断言的思想可能是Floyd[124]关于串行程序中首次提出的，后来被Ashcroft[15]和Lamport[175]推广到并发程序。其他许多地方也用了相似的思想。模拟的思想也有大量来源。最重要的一个来自串行程序中数据抽象方面的早期工作，如Liskov的编程语言CLU[198]，以及Milner[228]和Hoare[158]的工作。后期的工作将这种概念扩展到并行程序，这些工作包括Park[236]、Lamport[177]、Lynch[203]、Lynch和Tuttle[218]以及Jonsson[165]的论文。

[1] 为与原版书一致，本书中代表量、函数、集合等的外文字母、单词用斜体表示。——编辑注