These lecture notes cover basic automata-theoretic concepts and logical formalisms for the modeling and verification of concurrent and distributed systems. Many of these concepts naturally extend the classical automata and logics over words, which provide a framework for modeling sequential systems. A distributed system, on the other hand, combines several (finite or recursive) processes, and will therefore be modeled as a collection of (finite or pushdown, respectively) automata. A crucial parameter of a distributed system is the kind of interaction that is allowed between processes. In this lecture, we focus on the message-passing paradigm. In general, communication in a distributed system creates complex dependencies between events, which are hidden when using a sequential, operational semantics. The approach taken here is based on a faithful preservation of the dependencies of concurrent events. That is, an execution of a system is modeled as a partial order, or graph, rather than a sequence of events.
翻译:这些讲解说明涵盖了基本自动化理论概念以及同时和分布式系统建模和核查的逻辑形式概念。 许多这些概念自然地将古典自动化和逻辑扩展至单词,为相继系统建模提供了框架。 另一方面,分布式系统将若干(无限或递归)程序结合在一起,因此将建为自动数据集(分别是无限或按下)的模型。分布式系统的一个关键参数是两个进程之间允许的互动类型。在本讲解中,我们侧重于信息传递模式。一般而言,分布式系统中的通信在事件之间产生复杂的依赖性,在使用连续操作的语义时,这些事件会隐藏在其中。这里采用的方法是以忠实地保存同时事件的依赖性为基础的。也就是说,系统的执行是按部分顺序而不是按事件顺序建模的系统。