余代数逻辑与行为等价在可测空间上的关系

理论计算机科学电子笔记257（2009）71-85www.elsevier.com/locate/entcs可测空间上的余代数逻辑：行为等价与逻辑等价克里斯托夫·舒伯特1德国多特蒙德理工大学软件技术教授摘要研究了一般可测空间上余代数的逻辑等价与行为等价之间的关系模态逻辑解释在这些余代数使用谓词提升。突出的例子包括随机关系和标记马尔可夫转移系统和相应的本地版本的逻辑和行为等价的介绍，它表明，这些概念相吻合的一类广泛的函子。 我们将这些概念到模型检查中常见的相应全局值。在整个过程中，我们都在一般的可测量空间中工作。与以前的工作相比，不需要对状态空间进行拓扑假设。保留字：余代数逻辑，可测空间1介绍内函子的余代数为反应系统的研究提供了一个统一的框架。在这篇文章中，我们将研究可测空间和映射范畴Meas上函子的余代数。次概率函子S将扮演类似于幂集函子的角色，因为它允许我们处理随机方面而不是非确定性方面。突出的例子包括作为子概率函子S的余代数的随机关系和所谓的马尔可夫转移系统[4]，它们作为函子X−<$→（SX）A的余代数出现，对于某些作用集A。1 电子邮件：christoph. tu-dortmund.de1571-0661© 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.11.02772C. Schubert/Electronic Notes in Theoretical Computer Science 257（2009）71−→B−→ B·B模态逻辑，另一方面，似乎是一个适当的语言来谈论性质的余代数，因此反应系统。利用函子T的谓词提升，即自然变换nT ， 引 入 了余代数的模态算子。这里，是函子MeasopSet，它将每个可测量空间发送到其可测量子集的集合。两个余代数中的两个状态被称为逻辑等价（相对于给定的谓词提升族），如果它们满足完全相同的公式。像往常一样，如果我们能找到两个态射，它们的域是给定的余代数，它们的余域重合，并且它们将两个给定的状态映射到同一个状态，那么这两个状态被称为行为等价。我们证明了在谓词提升集上的条件下，上述两个状态等价概念是一致的。这推广了以前的结果在这方面，我们不需要满射的余代数态射，这使我们的本地版本的两个概念的等价。这似乎更类似于通常的共代数模态逻辑（overSet）。我们展示了如何推导出以前的，全球性的，从我们的结果主要的技术困难是证明逻辑是表达性的，也就是说，逻辑等价意味着行为等价。这是使用一个相当简单的因子分解技术。为了确保这一技术的适用性，我们必须依赖于一个有点技术性的概念，即缺乏一个更好的名称-可接受性。与以前的工作相比，我们没有对余代数的基础空间施加任何拓扑我们认为，这使博览会更容易获得。相关工作可测空间上余代数的模态逻辑的表示性这些作品可以分为两组。一类是满足某些拓扑性质的可测空间上的余代数[3，4，6，12]。在[2，8，5]中已经建立了一般可测空间的结果，但仅限于次概率函子S或SA的余代数。我们试图通过建立Meas上一般内函子的表达性结果来重新统一这两个群体。这里使用的基本因子分解技术源于[6]，并在[12]中用于在[13]基于标准Borel空间的最终余代数的存在性被用来将[12]的表达性结果推广到一般可测空间。有一种观点认为，考虑一种顺从性结构的习俗可能是有用的C. Schubert/Electronic Notes in Theoretical Computer Science 257（2009）7173∈ B ∈ A−›→B−→B −→B∈ B ∈ B BA||→|| ||A B A AB一一B||||B B −→ B −→B→ ||∗[12][13][14][15][16][2预赛为了读者的方便和便于参考，我们在这里收集了测度论的一些基本定义和结果几乎所有的结果都是众所周知的。可测空间回想一下，可测空间X由一个集合组成，X与σ-代数X在X上，即：X的一个子集族，它在复分段、可数交集和可数并集。为每个家庭对于一个集合M的子集，存在M上的一个最小σ-代数，我们记为σ（）.如果（1）A=（）则称为生成器（X）。可测函数XY由函数f给出：X Y等 f−1[B]X代表所有B（Y）。 如果Y=σ（），可测量性f由f−1[A]保证X代表所有A. 可衡量的范畴以可测函数为态射的空间用Meas表示。观察我们不区分Meas-态射和它的基本功能。通常我们只写X来代替X。分配XX定义一个函子设置与其由逆像函数的限制给出的对态射的作用，因此f= f−1：YX对于f：X Y。观察到它自然同构于hom-functorMeas（，2），其中2是两点空间，其中每个子集都是可测的。特别地，我们获得：引理2.1：如果f是满射，则测度集保持极限且f是单射.Q引理2.2我们有σ（f −1（A））= f −1（σ（A））。Q特殊态射给定可测空间族（Yi）I和公共定义域函数族（fi：AYi）I，我们定义了初始σ-代数该数据为A=σ（If−[B（Yi）]）。 其特点如下1property：a function g：|X| →A相对于BX和A是 可 测 的 当且仅当所有fi·g：X→Yi都是可测的。如果I={}，则A=f−1[B（Y）]。我74C. Schubert/Electronic Notes in Theoretical Computer Science 257（2009）71我我我−→−α∈·−⊂∈−αAAf−1[Gi]我 我证据 参见[7，Satz 5.2]。Q引理2.3Let（A−f→i|Y|）是一个函数族，并假设每个我我是的。有一个遗传算子Gi。则R∈Fi的初始σ -代数A为2）A+|X|→gi B）by{EB|i∈我I：g−1 [E] ∈ B（Xi）}.它的特征在于h：B→|Y|是由所有h · g i的可测性保证的。这可以用来证明Meas是完备的和共完备的。Lim-代数的构造如下：构造Set中基础图的极限（L，（li）），并用关于投影li的初始σ-代数来装备L，从而用l−1[BXi]生成的σ-代数来装备L。Colimits是用最终的σ-代数对偶地形成。等价关系与不变集设α是集合X上的等价关系。 设ηα：XX/α表示投影。我们得到一个附加条件：η[]PX，，ηα−1[−]P（X/α），其中PX表示X的幂集，按包含排序。由于ηα是满射的，所以每个B∈P（X/α）都是上面的附加函数的定点。另一方面，ηα−1的固定点ηα[]可以很容易地刻画为α-不变量X的子集。 在此为X是α-不变的，如果XA和xα xJ意味着对于每个x，x，J在X中。对于X的α-不变子集，写出Inv（α）。该附加函数仅限于一对互反函数η[]Inv（α），，ηα−1[−]P（X/α）。（一）确定集合X的子集族。 通过以下等式定义等价关系Eq（）：（x，xJ）∈ Eq（A）A∈ A：[x∈AxJ∈A].显然，每个A∈ A都是Eq（A）-不变的。引理2.4我们有Eq（A）= Eq（σA）。Q可分可测空间我们说集合X的子集族A分离点，如果每当x/=XJ则存在A∈A，其中x∈A，XJ∈/A，或反之亦然。σ.C. Schubert/Electronic Notes in Theoretical Computer Science 257（2009）7175BB→→→›→一我我我引理2.5 A分离点当且仅当σ（A）分离点。Q定义2.6一个可测空间X称为可分的，如果X分离点。由可分对象所张成的Meas的全子范畴记为Sep。命题2.7 Sep在Meas Proof 中的mono-sources 和co-products 下关闭 。设（fi：X−→Yi）I是Meas中的单源，并假设xi=xJ在X. 存在i∈I，且fi（x）/=fi（XJ），因此B∈BYi，且（比方说）fi（x）∈B，fi（XJ）∈/B. 因此x∈f−1[B]，xJ∈/f−1[B]，且f−1[B]∈BX因为fi是可测量的。联产品项下的关闭是显而易见的。Q次概率测度可测空间X上的次概率测度是σ-可加函数X[0， 1].X上的所有次概率测度的集合，当赋以关于（ev A）A∈BX的初始σ -代数时，成为可测空间SX，其中ev A：SX[0，1]，μμ（A）。这里，[0， 1]被装备由开子集生成的σ-代数。这个σ -代数的另一个生成元是{[r，1] |r ∈ Q <$[0，1]}.这种次概率构造产生函子S：Meas Meas通过设置Sf（μ）（B）=μ（f−1[B]）对f：X→Y在Meas中，μ∈SX，B∈ BY.引理2.8每个SX是可分的。证据观察到（evA）A∈BX是单源。因此，该主张来自命题2.7Q引理2.9设A ∈ BX在有限交下闭，其中σ（A）=BX。则B（SX）由集合{ev −1 [r，1]]生成|A∈ A，r∈Q<$[0，1]}.证据 将[14]中的引理3.6与引理2.3结合起来。Q3余代数与模型设T：Meas−→Meas是一个函子。一个T-余代数A=（A，d）由可测空间A和一个Meas-态射d：A→TA给出，称为动力学.余代数（A，d）→（AJ，DJ）的一个态射由一个Meas-态射76C. Schubert/Electronic Notes in Theoretical Computer Science 257（2009）71›→−→−→·Ff：A→AJ，使得AfAJddJJJTATfT AJ上下班这导致了T-余代数和态射的范畴CoalgT例1 （i）子概率函子的余代数是随机关系.(ii) X（SX）Act给出的Meas上行为被标记为马尔可夫过程。我们固定一组变量，并定义关于T和Var的模型如下所示定义3.1A（T，Var）-模型由一个T-余代数（A，d）和一个赋值组成;即一个函数Var −V→ B（A）。态射（A，d，V）−f→（AJ，dJ，VJ）由余代数态射（A，d）−f→（AJ，dJ）给出，满足B（f）·VJ=V。这将我们引向模型的Mod（T，Var）类别。注意到我们有一个同构M od（T，T）n=CoalgT。从现在开始，我们固定函子T，变量集;Mod（T，Var）将简单地用Mod表示。众所周知，明显的健忘函子CoalgTMeas创建了共极限;参见[1]。因此，CoalgT是共完全的，因为Meas是如此。这推广到模型：命题3.2明显的健忘函子Mod −→ Coalg T产生余极限。 因此，健忘函子Mod −→ Meas也会创建上极限。证据设D：D−→Mod是一个（小）图。记D（i）=（Xi ， di， Vi），（（X，d），ci）表示CoalgT中（Xi，di）的上极限。注意（BX，Bci）是Set中的极限。由于Dd是D中每个d：i→j的模型态射，赋值的集合（Vi）形成一个自然锥，因此存在唯一的V：Var−→ BX，其中对于每个i，Bci·V=Vi。我们证明了（X，d，V）是D在Mod中的一个余极限.设（fi：Di−→（Y，e，W））是自然上锥，f：XY是诱导CoalgT-态射. 因此，fci= fi成立。 我们有Bci·Bf·W=Bfi·W=Vi=Bci·V，其中第一个方程成立，因为fi是模型态射。因此，Bf·W=V由（Bci）是极限源这一事实得出，即：（X，d.V）−→C. Schubert/Electronic Notes in Theoretical Computer Science 257（2009）7177XXB −→ BB −→ BXBXA×B（Y，e，W）是一个模态射。Q推论3.3 Mod是共同完成的。Q4同品种器械提升设T：Meas→Meas是一个函子。T的n元谓词提升是一个自然变换λ：Bn→ B ·T。我们写n=ar（λ）。例2（i）设r为有理数，定义λr：BX−→BX通过：λr（B）={μ |μ（B）≥ r}= ev −1 [r，1]。（λr）很容易被认为是自然的。 我们写Λ 1={λr|r ∈ Q <$[0，1]}.(ii) 让Act是一个可数的“动作”集合。对于每个有理数r和每个a∈Act，我们定义一个谓词提升λr，a对于SAct，通过λr，a（B）={（μi）i∈Act|μa（B）≥ r}。我们写Λ Act={λr，a|a ∈ Act，r∈ Q <$[0，1]}.(iii) LetT表示由X<$→S（X×X）给出的函子，它对态射有明显的作用.我们定义一个族（κq）q∈Q <$[0，1]，κq（A，B）={μ ∈ S（X × X）|μ（A × B）≥q}= ev −1[q，1]。（二）一类谓词提升的逻辑修复谓词提升的集合Λ我们定义了由Λ（和Var）由以下语法：φ：：= T|φ1∧φ2|v|λ，φar（λ））对v∈Var，λ∈Λ.注4.1可以通过使用更多的布尔连接（由自然变换n建模）和定点算子（由自然变换ω建模）来丰富逻辑;参见[6]的讨论。 我们不这样做，结果一字不差。78C. Schubert/Electronic Notes in Theoretical Computer Science 257（2009）71（2）L（v） =V（v）MF（Ⅲ）M（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）（）（）（）（2）（）（）（）（Ⅲ）解释模型中的逻辑给定一个模型M=（A，d，V），我们可以通过分配一个集合来解释L（Λ），φ∈ BA到每个公式φ如下：TM=Aφ1φ2M=φ1M公司简介λ，φar（λ））M=Bd·λA（φ1M， . 对于M的一个状态x，我们记ThM（x）={φ∈ L|x∈φM}。命题4.2如果f：M −→ N是模型态射，则我们有对于每个φ，Bf（φ N）= φ M。证据证明过程通过公式φ的结构归纳进行，并利用谓词提升的自然性。详情见[6]，其中处理了单峰病例。Q推论4.3如果M −→N，则ThM（x）=ThN（f（x））。Q一个等价关系固定模型=（A，d，V）。设l表示A上的等价，它由公式的扩张确定。因此，在本发明中，xlxjj φ：[x ∈φ xJ∈ φ]，或者，更压缩地，l = Eq（{φ |φ ∈ L}）。注意，我们有xlxjThM（x）=ThM（xJ）。我们写EM=σ（{η1[φM]|φfor mula}）。引理4.4我们有{ηl[<$φ）]|φ公式}={A<$X/l|η−1[A]=<$φ），一些φ}。这两个集合在有限相交下都是封闭的证据 只要利用每一个φ是l-不变的，并应用（1）中的双解。第二个要求是因为有效集的集合在有限交下是封闭的，并且逆像函数保持有限交。Q引理4.5ηl：X−→（X/l，EM）是可解的。证据 由引理4.4可知。Q一般地，EM不是关于BX和η l的最终σ-代数a。 在下文中，ηM将始终表示其域为（X/l，EM）的可测函数。C. Schubert/Electronic Notes in Theoretical Computer Science 257（2009）7179（Ⅲ）M（2）MM（2）D{引理4.6固定一个可测空间Y和一个BY的生成元A。 函数f：X/l−→|Y|是可测的，如果对每个A∈ A存在φ使得η−1·f−1 [A] = φ。证据 这是显而易见的，因为它可以检查发电机的可测量性。Q我们将介绍关于谓词提升集的两个技术条件：可分离性和可容许性。我们的概念可分离谓词提升是一个专门化的一个使用在coalgebraic逻辑集，比照。[11 ]第10段。它首先在[6]中引入，用于一元谓词提升集可容许性是另一个技术条件，我们需要施加，以证明可测性的诱导功能。它在下面介绍，与可分性有关。分离同品种器械提升设λ：Bn−→ B·T是n元谓词提升. 我们定义一个等价关系式λ在TX上设置λφM= Eq（{λX（φ1M，.， φnM）|φ1，...，φn∈ L}）。定义4.7一个谓词提升的集合Λ被称为分离模型，如果我们有≡λ T（ηM）。λ∈Λ如果Λ分离每个模型M，则称Λ分离。例3集合Λ 1和Λ Act是分离的。由Lemma推出4.9（下）和命题4.11。可容许谓词提升定义4.8我们称一个谓词提升集合Λ为可容许的，如果集合{λX/1（ηφ1， . ，ηφar（λ））|λ∈Λ，φ1， . ，φar（λ）∈L}对于每个模型M，生成B（T（X/1，EM））。引理4.9对于每个集合Act，族Λ Act是可容许的。证据写Q=（X/l，EM）。首先考虑Act ={}的情况。我们从引理2.9和引理4.4知道，BSQ由下式生成：= ev−1（ηφ）[规则，1] |φ∈ L，r∈Q<$[0，1]}.80C. Schubert/Electronic Notes in Theoretical Computer Science 257（2009）71r，aQ（Ⅲ）B×{× ∈ B ∈ B|取t，t∈TX，其中t为.<$<$）<$）M={λr，a（ηφ））|r∈Q<$[0，1]，φ∈L }其中最后一个等式成立，因为每个φi）都是不变的。n由于ev−1[r，1] =λr（η φ）成立，这就是可容许性的条件。（ηφ）（Q）对于一般集合Act，观察到我们有C={λQ（ηφ））|a∈ Act，r∈QQ<$[0， 1]，φ∈ L}a∈Act=a∈Act=a∈Actπa−1。{λr（ηφ）|r∈Q <$[0，1]， φ∈L}<$πa−1（D）其中πa：SQAct−→SQ是第a个投影。 由于D生成BSQ，C通过引理2.3生成B（SQAct）。Q引理4.10集合（κr）r∈Q <$[0，1]是可容许的。证据 对于可测空间X和Y，集合ABAX，BY是在有限交下闭的，并且是（X Y）的生成元。因此，该断言由引理2.9得出。Q命题4.11如果每个TX是分离的，那么每个可容许的预测提升集都是分离的。证据固定一个模型M=（X，d，V），λ∈ Λ，元数n，φ1，.，φn∈ L。对于每个t∈TX：T η（t）∈λX/l（ηφ1）， . ，η<$φn））n∈BT η·λX/l（η <$φ1）， . ，ηφn））⇐⇒ t∈λX·（Bη）（ηφ1），.，ηφn））⇐⇒ t∈λX（φ1），.， （φn））JλTη（tJ）。通过T（M）对于所有λ∈ Λ，我们需要证明Tη（t）=EM）和引理2.5，它表明X/l，（T η（t）， T η（tJ））∈Eq{λX/l（ηφ1， . ，ηφar（λ））|λ∈Λ，φ1， . ，φar（λ）∈L}.从上面的计算可以得出，最后一个条件等价于（t，tJ）∈λ.Q同余定理定理4.12设Λ是一个分离的可容许的谓词提升集。对于每个模型M，存在X/1M上的模型结构M/1，使得ηM：M −→ M/1M是一个模型态射。C. Schubert/Electronic Notes in Theoretical Computer Science 257（2009）7181M（）（）= Bd·λ·（Bη）n（ηφ），.，ηφ））X1n（†）（Ⅲ）<$E <$）B·MM（Ⅲ）=Bd·λX（η−1 [η<$1）]，. η−1 [η<$φn）]）†证据我们写M=（X，d，V），l表示lM，Q表示（X/lM，EM）。我们称XLXJ蕴涵（d（x），d（XJ））∈kerTη.根据Λ的分离性，它可以表示为：证明我们有d（x）<$λ d（xJ），对于每个λ ∈ Λ。取λ∈ Λ，记为n = ar（λ）和fix φ1，.，φn∈ L。我们得到：d（x）∈λX（φ1，...， φn） ⇐⇒ x∈Bd·λX（φ1，...， φn）⇐⇒x∈<$<$λ<$（φ1，.，φ1））因此，（d（x），d（xJ））∈ <$λ由xlxJ得出。 因此，存在一个独特的函数q：Q−→TQM为此ηXQDQJJTXTη TQ上下班 我们需要证明q是可测量的。固定任意n元的λ和φ1，...， φn∈ L并观察：η−1·q−1·λQ（η <$φ1），.，ηφn））= Bd· BTη·λQ（ηφ1），.，ηφn））= Bd·λX（φ1），.，（φn））= λφn），其中（）通过φi的不变性成立。q的可测性由Λ的可接受性和引理4.6得出。我们只需要在Q上定义一个估值W。 对于v∈Var，我们设置W（v）=ηv MM。 的l-不变性 vM我们得到η W（v）=η−1[ηV（v）]=V（v），因此W使η成为模型态射。具有此性质的W的唯一性通过Bη的内射性而成立。Q的约简Red（）是定理4.12中构造的模型（Q，q，W）。因此，Q的基础集合由X/lM给出，并且我们有BQ=EM=σ（{η [φM] |φ∈L}）。在解析空间上回想一下，一个可测空间被称为解析的，如果它的可测子集作为一个拓扑空间的波莱尔集出现，而这个拓扑空间是一个具有可数基的可度量拓扑空间82C. Schubert/Electronic Notes in Theoretical Computer Science 257（2009）71MMMM −→ MMMM如果模型的基本可测空间是解析的-这是[4，6，12]中的全面假设-我们可以在不依赖Λ的可容许性的情况下形成reduce Red（）。引理4.14设M =（A，d，V）是A解析的模型，并假设L是可数的。 则EM是关于投影ηlM的最终σ-代数。证据 见[5，推论3]。Q注意，如果Λ和Var都是可数的，则L是可数的。定理4.15设Λ是一个可数的、分离的谓词提升集，Var是可数的。对于每个模型=（A，d，V），A解析，存在A/l上的模型结构/l，使得η：/l 是 模 型 态射。证据我们继续定理4.12的证明，定义商动力学q。 注意q的良定性只是利用了Λ的分离性。 q的可测性直接从引理4.14得出，因为我们有q·η=Tη·d，后一个函数是可测的。Q5逻辑和行为等价定义5.1我们对M，MJ建 模 ， 并在M中声明a，在MJ中声明A J。(i) 我们说状态a和aJ在逻辑上是等价的，如果ThM（a）=ThMJ（aJ）.(ii) 我们说模型M和MJ在逻辑上等价，如果{ThM（a）|a∈A}={ThMJ（aJ）|aJ∈AJ}。(iii) 如果存在模型N和cosspan，我们说状态a和aJ行为等价M −f→ N <$g− MJ（3）f（a）=g（AJ）成立;(iv) 我们说，模型和J是行为等价的，如果存在一个cosspan（3）与f和g满射模型态射。注意，上面介绍的等价概念自然地将自己分为两组：局部或基于状态的概念（1，3）和全局概念（2，4）。命题4.2和推论4.3意味着：• 状态的（局部）行为等价意味着它们的（局部）逻辑等价。C. Schubert/Electronic Notes in Theoretical Computer Science 257（2009）7183MNN MNMM N MN····MN• 模型的（全局）行为等价性意味着它们的（全局）逻辑等价性;现在我们将证明，在适当的条件下，所有四种含义都可以逆转。到目前为止，关于随机关系的模态逻辑的工作在某种程度上集中在全局方面。我们认为局部概念（作为集合上余代数的自同构）更符合经典模态逻辑的精神，它本质上是局部的。定理5.2假设Λ是分离的且可容许的。修复模型和。 如果x的状态 和y的状态在逻辑上是等价的，那么它们在行为上是等价的。证据 我们首先形成余积+的和然后根据定理4.12求Reduce Red（+）。 因此，我们得到以下模型态射MiMM+N，iN，NηJ红色（M+N）（四）根据推论4.3，我们有ThM+N（iM（x））=ThM（x）=ThN（y）=ThM+N（iN（b））。因此，η iM（x）=η iN（y）;也就是说，Red（+ ）证明a和b在行为上是等价的。Q下面关于整体性质等价性的结果实际上是定理5.2的一个简单推论：定理5.3假设Λ是分离的 且可容许的。模型的逻辑等价隐含着模型的行为等价证据设M和N在逻辑上等价，并构成图（4）。我们称η·iM和η·iN是满射的.考虑η·iM，取任意状态[z]为红色（M + N）。 如果z在iM的图像中，我们就完成了。否则，z= iN（y）对于N的某个状态。 我们找到M的一个状态x，其中ThM（x）= ThN（y），因此ThM+N（iM（x））=ThM+N（iN（y）），即ηiM（x）=ηiN（y）=η（z）=[z]。Q6结论和进一步工作我们建立了一般可测空间上的余代数逻辑的表现性结果在这样做的过程中，我们在三个方面改进了以前在这一领域发表的工作：84C. Schubert/Electronic Notes in Theoretical Computer Science 257（2009）71(i) 我们能够在状态空间上没有任何拓扑假设的情况下工作;(ii) 我们在可测空间范畴上使用一般函子，而不依赖于所谓的左或右余代数[6];(iii) 我们考虑了行为和逻辑等价的局部版本，它们处理单个状态而不是整个模型。这似乎符合集合范畴上的共代数模态逻辑的精神。事实上，全局性质是局部性质的简单结果这里所介绍的工作的一个明显的扩展将包括也讨论了双相似性。这是阻碍的事实，即次概率函子不保持弱回调。这里给出的结果的另一个可能的扩展源于这样的观察：可测空间可以被看作是一个集合，其上有一个零维拓扑的基，特别地，容许性的技术概念可以被改写为这些拓扑的连续性条件。这暗示了我们的工作和Stone余代数[9]的工作的可能统一。确认作者要感谢Ernst-Erich Doberkat提供的大量技术讨论。引用[1] J. 艾达·迈克。余代数导论。分类理论与应用，14（8）：157-199，2005.[2] V. Danos，J. Desharnais，F. Laviolette和P. Panangelette。互模拟与余同余概率系统。信息与计算，204：503[3] J. Desharnais，A. Edalat，and P. Panangelo. 标记马尔可夫过程的互模拟。信息与计算，179：163[4] E.- E. 多伯卡特 随机关系马尔可夫转移系统的基础。 Chapman &Hall/CRC Press，Boca Raton，New York，2007.[5] E.- E.多伯卡特一般可测空间中随机Kripke模型的行为和逻辑等价性。 在ProceedingsTAMC 2009，Lect. 计算机科学，第192-200页，2009年。[6] E.- E. Doberkat和C.舒伯特随机右余代数的余代数逻辑。Ann. Pure Appl. Logic，2009.doi：10.1016/j.apal.2008/06/018。[7] J. Elstrodt. 数学与整合理论Springer-Verlag，柏林-海德堡-纽约，第2版，1999年。[8] B. Jacobs 和 A. 索 科 洛 娃 模 态 逻 辑 的 示 例 表 达 性 。 Journal of Logic andComputation，2009. http://dx.doi.org/10.1093/logcom/exn093。C. Schubert/Electronic Notes in Theoretical Computer Science 257（2009）7185[9] C. Kupke，A.Kurz和Y.维尼玛Stone余代数理论计算机科学，327：109[10] D.帕丁森 余代数的终结序列归纳表示逻辑。 NotreDame J.Formal Logic，45（1）：19[11] L. S ch？oder.模态逻辑的表达：极限与边界。计算机科学，390：230 -247，2008.[12] C.舒伯特解析空间上的余代数逻辑。技术报告170，软件技术主席，Te chnis c heUniversit？atDort mund，2007年10月。[13] C.舒伯特测度多项式函子的最终余代数。在Proceedings TAMC 2009，Lect. NotesComputer Science的第5532卷，第325-334页[14] I. D. 维里佐可测空间上的余代数。博士论文，印第安纳大学，2005年。