南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院 施曉靜 邢惠麗 張晉津

n-精化關(guān)系及其相關(guān)研究

南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院 施曉靜 邢惠麗 張晉津

精化關(guān)系是研究反應(yīng)式系統(tǒng)的重要內(nèi)容之一。本文在n-互模擬的基礎(chǔ)上提出了分層精化精化關(guān)系，探究n-精化關(guān)系與分層互模擬關(guān)系之間的區(qū)別與聯(lián)系，定義n-精化模態(tài)邏輯語(yǔ)言并給出相關(guān)的永真式。

n-精化；n-互模擬，n-精化模態(tài)邏輯

1.前言

反應(yīng)式系統(tǒng)的研究?jī)?nèi)容之一是討論進(jìn)程之間的行為等價(jià)或者精化關(guān)系，一般而言前者是一個(gè)等價(jià)關(guān)系而后者是一個(gè)前序關(guān)系，在進(jìn)程代數(shù)理論發(fā)展過(guò)程中人們提出了許多概念用來(lái)描述進(jìn)程之間的行為等價(jià)或精化關(guān)系，Van Glabbeek及Luca Aceto分別對(duì)這些概念之間的聯(lián)系做了較為系統(tǒng)的總結(jié)[1][2]。Hans van Ditmarsch等人引入了未來(lái)事件邏輯[3]（future event logic），將精化模態(tài)邏輯（refinement modal logic）看作是未來(lái)事件邏輯的抽象[4]，用于描述與所給的信息狀態(tài)相匹配的信息事件。研究最初定義的模態(tài)算子僅僅是時(shí)間意義上的，因此被稱作未來(lái)事件。然而隨著研究的深入學(xué)者們逐漸意識(shí)到，在不同的模態(tài)邏輯下用結(jié)構(gòu)轉(zhuǎn)換來(lái)解釋這個(gè)算子具有更廣泛的意義，由此，Laura Bozzelli等人在Hans van Ditmarsch的研究基礎(chǔ)上，提出精化關(guān)系以及多agent的精化模態(tài)邏輯。精化關(guān)系是研究與所給信息相匹配的信息事件的這類匹配關(guān)系，然而，在實(shí)際應(yīng)用中只需考慮這種匹配關(guān)系是否在兩模型之間上的狀態(tài)點(diǎn)上有限步內(nèi)保持即可，因此我們需要對(duì)精化關(guān)系作有限層次的限制，從而產(chǎn)生分層精化關(guān)系(n-refnement)。

基于Laura Bozzelli等人的工作研究，本文將著眼于n-精化關(guān)系的概念及其數(shù)學(xué)性質(zhì)，給出其與分層互模擬之間的聯(lián)系。

全文安排如下：第二節(jié)主要介紹本文所用標(biāo)記等預(yù)備知識(shí)；第三節(jié)引入n-精化關(guān)系，研究其相關(guān)數(shù)學(xué)性質(zhì)并給出n-精化和n-互模擬之間的聯(lián)系；第四節(jié)定義n-精化模態(tài)邏輯語(yǔ)言，并給出其對(duì)應(yīng)的永真式。

2.預(yù)備知識(shí)

本文采用如下記號(hào)：A表示一個(gè)有限的agent集合，P表示命題變?cè)目蓴?shù)集合，N表示自然數(shù)集合。一般情況下，表示P中元素。

本文采用如下記號(hào)：A表示有限的agent集合，P表示可數(shù)的命題變?cè)?，N表示自然數(shù)集。一般情況下，用表示A中的元素，表示P中元素。

模型M是一個(gè)三元組(S,R,V)，其中S是一個(gè)非空集合，R是一個(gè)從A到的可達(dá)關(guān)系函數(shù)，V表示從P到的指派函數(shù)?？蛇_(dá)關(guān)系函數(shù)R對(duì)每一個(gè)定義了相應(yīng)的可達(dá)關(guān)系。指派函數(shù)V對(duì)于每個(gè)命題變?cè)M(jìn)行了賦值，V(p)是滿足p的所有狀態(tài)形成的集合，點(diǎn)模型（Pointed Model）Ms是由模型M和一個(gè)狀態(tài)點(diǎn)構(gòu)成的有序?qū)Α?/p>

3.n-精化關(guān)系

下面參考n-互模擬[11]引入分層精化的概念。

證明：由引理4不難得證。

4.n-精化模態(tài)邏輯

下面將給出n-精化模態(tài)邏輯的語(yǔ)法和語(yǔ)義。

證明：(1)(2)(3)均可由命題2即可得證。

5.結(jié)論

本文主要介紹了n-精化關(guān)系，在此基礎(chǔ)上探究了n-精化關(guān)系的數(shù)學(xué)性質(zhì)，給出其與n-互模擬關(guān)系之間的聯(lián)系，Hans van Ditmarsch等人探究了互模擬量化邏輯和精化模態(tài)邏輯之間的聯(lián)系并且在文獻(xiàn)[7]中給出精化模態(tài)邏輯到互模擬量化邏輯的翻譯?；诂F(xiàn)有的研究基礎(chǔ)，我們可以進(jìn)一步研究n-精化模態(tài)邏輯與互模擬量化邏輯之間的關(guān)系。根據(jù)n-精化邏輯語(yǔ)言的語(yǔ)法和語(yǔ)義我們進(jìn)一步研究其公理化系統(tǒng)及其相應(yīng)的可靠性與完備性。

[1]Van Glabbeek R J．The linear time-branching timespectrum I[C]//The semantics of Concrete Sequential Processes．Hand-book of Process Algebra．Elsevier, 2001:3-9．

[2]Aceto L,De Frutos Escig D,Gregorio-Rodriguez C,et al．Axiomatizatizing weak simultion semantics over BCCSP[J]．Theoretical Computer Science 2014,537:42-71．

[3]H．van Ditmarsch,T．French, Simulation and information[J]． Broersen,J．-J．Meyer (Eds．), Knowledge Representation for Agents and Multi-Agent．

[4]H． van Ditmarsch, T． French, S． Pinchinat, Future event logic-axioms and complexity,[J] Moscow, vol． 8, College Publications, 2010, pp． 77–99.

[5]P．Blackburn,M．de Rijke,Y．Venema,Modal Logic[M] Cambridge Tracts in Theoretical Computer Science,vol．53, Cambridge University Press,Cambridge,2001．

[6]Laura Bozzelli,Hans van Ditmarsch,,Tim French,James Hales,Sophie Pinchinat,Refinement modal logic[J],in Information and Computation．

[7]G．d’Agostino, G．Lenzi, An axiomatization of bisimulation quantifiers via the u-calculus, [J] Theor．Comput．Sci．338 (1–3) (2005) 64–95．

[8]M．Bilkova,A．Palmigiano,Y．Venema, Proof systems for the coalgebraic cover modality, in: Carlos Areces,[M] Robert Goldblatt, Advances in Modal Logic, College Publications,2008,pp．1–21．

[9]C．Kupke,A．Kurz,Y．Venema,Completeness of the finitary moss logic[J]．C．Areces,R．Goldblatt (Eds．), Advances in Modal Logic 7,College Publications,2008,pp．193–217．

[10]Y．Venema, Lecture notes on the modal u-calculus, [M] Draft, 2012．

[11]T．French, Bisimulation quantifiers for modal logic, [M] PhD thesis, University of Western Australia, 2006．

[12]G．d’Agostino,M．Hollenberg,Logical questions concerning the u-calculus: interpolation[J]．Lyndon and Los-Tarski．Symb．Log．65 (1)(2000) 310–332．

[13]J．Hales, Refinement quantifiers for logics of belief and knowledge,[J] Honours Thesis, University of Western Australia, 2011．

[14]J．Hales,T．French,R．Davies, Refinement quantified logics of knowledge[J]．Electron．Notes Theor．Comput．Sci．278 (2011) 85–98．

[15]朱梧槚．?dāng)?shù)理邏輯引論[M]．(2008)．

Investigation on the n-refnement relations

SHI Xiao Jing1,Xing Hui Li,Jin Jin Zhang
(School of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, China)1

The refnement relations is one of the important contents of studying reactive systems. This paper introducing the notion of nrefnement by the defnition of n-bisimulation, studying the the differences between the n-refnement and n-bisimulation, as well as defning nrefnement modal logic language and giving relevant validities.

n-refnement; n-bisimulation; n-refnement modal logic

施曉靜（1990－），女，碩士生，主要研究方向?yàn)樾问交椒ā?/p>

The National Natural Science Foundations of China under Grant Nos．11426136, 60973045(國(guó)家自然科學(xué)基金); the Natural Science Foundation of Jiangsu Higher Education Institutions under Grant No．61602249 (江蘇省高校自然科學(xué)基金)。