面向邏輯標(biāo)記轉(zhuǎn)換系統(tǒng)的進(jìn)程演算CLLR的研究.pdf

1、為了形式化規(guī)范、驗證和分析反應(yīng)式并發(fā)系統(tǒng)，學(xué)術(shù)界提出并發(fā)展了多種形式化規(guī)范方法。這些方法大體上可分為兩類：基于動作的和基于狀態(tài)的?；趧幼鞯囊?guī)范方法以進(jìn)程代數(shù)（演算）最具代表性；基于狀態(tài)的方法通常以模態(tài)邏輯或演算描述系統(tǒng)規(guī)范。這兩類方法基于不同的觀點，對形式規(guī)范和驗證進(jìn)行了深入而廣泛的研究，具有互補的優(yōu)點：前者支持規(guī)范的組合式（compositional)構(gòu)造、分析和推理；后者擅長描述系統(tǒng)整體和抽象性質(zhì)。十余年來，學(xué)術(shù)界期望構(gòu)建一種允許

2、上述兩種不同風(fēng)格規(guī)范并存且混合使用的架構(gòu)，以此實現(xiàn)可以同時利用它們各自長處的目的。在此愿景驅(qū)使下，多種所謂混合規(guī)范方法被相繼提出，其中，L(u)ttgen和Vogler近年提出的邏輯標(biāo)記轉(zhuǎn)換系統(tǒng)￡簡記為LLTS)克服了其它方法的缺陷，是一個允許自由混合使用通常進(jìn)程算子和邏輯算子進(jìn)行規(guī)范的語義框架。本文旨在基于純演算的方法針對LLTS在理論研究上的空白和缺陷開展工作，主要工作包括如下方面：
　　(1)構(gòu)建面向LLTS的進(jìn)程演算系統(tǒng)C

3、LLR。該工作不但將L(u)ttgen和Vogler的工作(不含隱藏算子）提升到純演算的風(fēng)格，更主要的貢獻(xiàn)在于深入研究了他們沒有涉及的遞歸算子。在深入研究環(huán)境（context)、遞歸進(jìn)程的展開與進(jìn)程轉(zhuǎn)換之間的內(nèi)在聯(lián)系基礎(chǔ)上，我們較為系統(tǒng)地發(fā)展了CLLfl的行為理論，證明了L(u)ttgen和Vogler提出的預(yù)備模擬關(guān)系相對CLLR所有算子的前同余性（precongruence)，從而在理論上保證了CLLfl可以支持規(guī)范組合式的構(gòu)造、分

4、析和推理。作為面向LLTS的演算系統(tǒng)，CLLR包含了邏輯合取和析取算子，并需要處理邏輯復(fù)合所帶來的進(jìn)程協(xié)調(diào)性問題。正因為進(jìn)程協(xié)調(diào)性對進(jìn)程行為的發(fā)散所具有的敏感性，使得CLLR中的遞歸算子處理較之通常進(jìn)程演算要相對困難和復(fù)雜許多。
　　(2)在充分考慮協(xié)調(diào)進(jìn)程與非協(xié)調(diào)進(jìn)程行為差異的基礎(chǔ)上，提出了CLLR的公理系統(tǒng)AXCLL，并證明了該系統(tǒng)的可靠性以及相對無遞歸進(jìn)程的基完備性，從而揭示了通常進(jìn)程算子與邏輯合取及析取算子在預(yù)備模擬關(guān)系下

5、所遵循的代數(shù)律。
　　(3)研究了CLLR中形如X=RStX方程的解，證明了唯一解定理和最大解定理。前者給出了這類方程存在唯一解的充分條件；后者揭示了遞歸進(jìn)程〈X|X=tX〉與X=RStX的解之間的內(nèi)在聯(lián)系：若X是tX的強(qiáng)有衛(wèi)變兀，則〈X|X=tX)是滿足等式X=RStX的最“粗糙”的規(guī)范。
　　(4)作為遞歸算子與方程最大解定理的應(yīng)用，我們研究了將基于動作的計算樹邏輯ACTL表示安全性質(zhì)的語言片段在CLLp中進(jìn)行編碼的問題

6、。該研究在理論上保證了CLLp具有描述安全性質(zhì)的表達(dá)能力，同時將判定進(jìn)程是否滿足（表示安全性的）ACTL公式的模型檢測問題歸約為判定進(jìn)程之間是否具有精化關(guān)系的驗證問題。由于遞歸算子的使用，該工作所提供的編碼極大簡化了L(u)ttgen和Vogler的原有編碼。
　　總之，上述研究將LLTS框架上原有的工作演算化（未包括隱藏算子)，在此基礎(chǔ)上較深入研究了L(u)ttgen和Vogler原有工作中沒有涉及的若干重要的理論問題，包括：遞