关键词: 逻辑标记转换系统, 预备模拟, 划分对, 划分精化问题

Abstract: Luttgen et al. combined process algebras and temporal logics to propose the notion of logic labeled transition system (LLTS) and corresponding refinement relation: LLTS ready simulation. To give a method to determine LLTS ready simulation between different states, based on the concept of partition pair, this paper brings a notion of stable partition pair which is isomorphic to LLTS ready simulation, and proposes the coarsest partition problem of generalization relation, then proves the equivalence between this notion and the LLTS ready simulation quotient. From this equivalence, this paper presents a calculus ρ to determine LLTS ready simulation relation between two logic labeled transition systems, and gives the correctness of this calculus. Finally, this paper presents a realistic example to show how this calculus operates.

Key words: logic labeled transition system, ready simulation, partition pair, partition refinement problems