n-精化关系及其相关研究

南京航空航天大学计算机科学与技术学院 施晓静 邢惠丽 张晋津

n-精化关系及其相关研究

南京航空航天大学计算机科学与技术学院 施晓静 邢惠丽 张晋津

精化关系是研究反应式系统的重要内容之一。本文在n-互模拟的基础上提出了分层精化精化关系，探究n-精化关系与分层互模拟关系之间的区别与联系，定义n-精化模态逻辑语言并给出相关的永真式。

n-精化；n-互模拟，n-精化模态逻辑

1.前言

反应式系统的研究内容之一是讨论进程之间的行为等价或者精化关系，一般而言前者是一个等价关系而后者是一个前序关系，在进程代数理论发展过程中人们提出了许多概念用来描述进程之间的行为等价或精化关系，Van Glabbeek及Luca Aceto分别对这些概念之间的联系做了较为系统的总结[1][2]。Hans van Ditmarsch等人引入了未来事件逻辑[3]（future event logic），将精化模态逻辑（refinement modal logic）看作是未来事件逻辑的抽象[4]，用于描述与所给的信息状态相匹配的信息事件。研究最初定义的模态算子仅仅是时间意义上的，因此被称作未来事件。然而随着研究的深入学者们逐渐意识到，在不同的模态逻辑下用结构转换来解释这个算子具有更广泛的意义，由此，Laura Bozzelli等人在Hans van Ditmarsch的研究基础上，提出精化关系以及多agent的精化模态逻辑。精化关系是研究与所给信息相匹配的信息事件的这类匹配关系，然而，在实际应用中只需考虑这种匹配关系是否在两模型之间上的状态点上有限步内保持即可，因此我们需要对精化关系作有限层次的限制，从而产生分层精化关系(n-refnement)。

基于Laura Bozzelli等人的工作研究，本文将着眼于n-精化关系的概念及其数学性质，给出其与分层互模拟之间的联系。

全文安排如下：第二节主要介绍本文所用标记等预备知识；第三节引入n-精化关系，研究其相关数学性质并给出n-精化和n-互模拟之间的联系；第四节定义n-精化模态逻辑语言，并给出其对应的永真式。

2.预备知识

本文采用如下记号：A表示一个有限的agent集合，P表示命题变元的可数集合，N表示自然数集合。一般情况下，表示P中元素。

本文采用如下记号：A表示有限的agent集合，P表示可数的命题变元集合，N表示自然数集。一般情况下，用表示A中的元素，表示P中元素。

模型M是一个三元组(S,R,V)，其中S是一个非空集合，R是一个从A到的可达关系函数，V表示从P到的指派函数。可达关系函数R对每一个定义了相应的可达关系。指派函数V对于每个命题变元进行了赋值，V(p)是满足p的所有状态形成的集合，点模型（Pointed Model）Ms是由模型M和一个状态点构成的有序对。

3.n-精化关系

下面参考n-互模拟[11]引入分层精化的概念。

证明：由引理4不难得证。

4.n-精化模态逻辑

下面将给出n-精化模态逻辑的语法和语义。

证明：(1)(2)(3)均可由命题2即可得证。

5.结论

本文主要介绍了n-精化关系，在此基础上探究了n-精化关系的数学性质，给出其与n-互模拟关系之间的联系，Hans van Ditmarsch等人探究了互模拟量化逻辑和精化模态逻辑之间的联系并且在文献[7]中给出精化模态逻辑到互模拟量化逻辑的翻译。基于现有的研究基础，我们可以进一步研究n-精化模态逻辑与互模拟量化逻辑之间的关系。根据n-精化逻辑语言的语法和语义我们进一步研究其公理化系统及其相应的可靠性与完备性。

[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]朱梧槚．数理逻辑引论[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－），女，硕士生，主要研究方向为形式化方法。

The National Natural Science Foundations of China under Grant Nos．11426136, 60973045(国家自然科学基金); the Natural Science Foundation of Jiangsu Higher Education Institutions under Grant No．61602249 (江苏省高校自然科学基金)。