弱共变-逆变模拟的公理刻画

进程代数是并发理论研究的主流方向,是分析和描述并发与分布式系统的重要工具之一。模拟是进程代数中刻画精化关系的核心概念。共变-逆变模拟派生于通常的模拟关系,它区分动作的类型,直观上,表达了状态的行为数目越多但并不一定越好的事实。然而,该模拟关系忽略了可观测动作与内动作的区别。因此,给出一种弱共变-逆变模拟关系及其相应的公理刻画,并且建立了该公理系统的可靠性与基完备性,进而证明了该公理系统亦是ω-完备的。     

移动进程演算中的开互模拟

该文就移动进程演算中的弱开同余关系进行了研究。文中考虑了一种简单的非确定性移动进程演算模型,证明了Milner的三条tau规则在有等名测试算子时不足以将强开同余关系的完全公理化系统提升到同余关系的完全公理化系统,文中提出了第四条tau规则,处理了在前缀操作下的等名测试算子,并证明了强开同余关系的完全公理化系统加上四条tau规则可得到弱开同余关系的完全公理化系统。该文的结论否定了关于Milner的三条tau规则足以将π－演算中的强同余关系的完全公理化系统提升到弱同余关系的完全公理化系统的猜想。     

带Mismatch算子的高阶π演算

主要研究带mismatch的高阶进程演算的公理化问题。首先,建立存在mismatch时高阶进程的开弱高阶互模拟理论,证明了等价关系、同余性等重要性质;其次,沿用线性的方法,构建得到带 mismatch 的有限进程上的公理系统;最后,基于对开弱高阶互模拟的刻画,证明了该公理系统的完备性定理。该工作为带 mismatch 的高阶进程上互模拟判定的有效算法的设计与实现,进而为相关的应用建模工作提供了理论借鉴。     

多态π演算的互模拟等价关系及其公理化

类型系统在分布式系统理论中有着非常重要的作用。在为π演算引入多态类型系统后,需要对新的环境下进程的等价关系进行研究。在多态类型系统下,环境只能得知进程中通道的抽象类型,而无法得知通道的具体类型,此时环境的区分能力被削弱,所得到的互模拟关系更为粗糙。本文在以往文献研究的基础上给出了多态π演算互模拟的一个公理系统,并证明了公理系统的一致性和完备性。     

一个移动进程演算的互模拟同余定义框架

并发计算模型是理论计算机科学研究的重要领域之一。以π演算为代表的移动进程演算是目前并发理论的研究热点。互模拟等价定义是移动进程演算研究中的核心概念和问题，而传名机制使得移动进程演算中的互模拟同余关系更加复杂和有趣。本文在分析了常见的互模拟同余定义的基础上，通过抽取定义的核心要素，提出了一个三维的互模拟同余定义模型，从而将一般文献中常见的互模拟定义纳入到一个统一的框架中来，加深了我们对移动进程演算中互模拟概念的理解；同时本文利用这个模型，系统分析了各种互模拟之阿的关系。模型的优点在于它的普适性和开放性。     

一种扩充的π-演算及事务性等价关系研究

为了保证Web服务事务获得正确的执行和一致的结果,对Web服务事务处理的形式化研究是很重要的.现有研究集中在事务的建模和协议验证上,对事务特性仍缺乏深入研究.已有的事务建模方法主要采用增加额外的操作算子来描述事务补偿语义,而过于复杂的语法和迁移规则不利于对事务特性的进一步分析.在不增加新的操作算子的前提下,引入事务膜的位置概念来表示事务作用域,将进程的交互动作与消息相对事务膜的传递过程相关联,对π-演算进行扩充.结合进程行为的事务依赖性,提出了一种弱事务性开互模拟,来刻画可见事务行为的等价关系,利用互模拟等价理论分析了弱事务性等价关系的基本性质,为研究Web服务的事务特性提供了理论基础.     

三分之二模拟拓扑

三分之二模拟为验证系统的实现满足其规范提供了抽象描述.为了刻画系统的实现逐渐接近于规范,该文利用网极限的观点,以三分之二模拟为基础,建立系统实现的收敛机制,说明系统规范是其实现的极限形式.首先提出三分之二极限模拟和三分之二模拟极限的定义,建立三分之二模拟的极限理论.其次,建立三分之二极限模拟的拓扑结构,包括子网闭包、尾闭包、自然延拓和复合,证明三分之二模拟极限构成一个收敛类,并诱导一个拓扑,给出三分之二模拟极限的拓扑理论.最后,证明三分之二模拟极限在各种复合算子下的拟同余性(pre-congruence),进而说明各种复合算子关于三分之二模拟极限的连续性.     

对象演算Ⅰ

对象演算是一个面向对象的逻辑演算系统,它建立在描述具有内部状态的动态演变实体的Trace演算之上.对象比一般意义下的动态实体具有更多和更好的特性,特别是封装性.为此,文章引入有效动作的概念,通过对象的有效动作来刻画对象的封装性,即只有对象的有效动作才能访问或修改对象的属性值,从而对Trace演算的语义模型加以限制,得到对象语义解释模型.作为逻辑系统,文章还讨论了对象演算的公理化,它是Trace演算公理系统的扩充.作为应用,文章结合实例给出了对象语义的描述及特性推理.     

非对称χ≠-演算的基同余

该文研究非对称χ^≠-演算的基同余．文中引入一组L-互模拟关系,并确定基互模拟就是由L-互模拟定义导出的12个互异的互模拟关系中的最小关系,给出了某些L-互模拟的开模拟性质,利用开模拟性质引入开基互模拟概念,并证明开基互模拟与基互模拟是一致的,构造了基于基同余的可靠和完备的等式系统,最后给出了基同余的完备性定理．     

Prototyping SOS Meta-theory in Maude

We present a prototype implementation of SOS meta-theory in the Maude term rewriting language. The prototype defines the basic concepts of SOS meta-theory (e.g., transition formulae, deduction rules and transition system specifications) in Maude. Besides the basic definitions, we implement methods for checking the premises of some SOS meta-theorems (e.g., GSOS congruence meta-theorem) in this framework. Furthermore, we define a generic strategy for animating programs and models for semantic specifications in our meta-language. The general goal of this line of research is to develop a general-purpose tool that assists language designers by checking useful properties about the language under definition and by providing a rapid prototyping environment for scrutinizing the actual behavior of programs according to the defined semantics.     

Semantics and expressiveness of ordered SOS

Structured Operational Semantics (SOS) is a popular method for defining semantics by means of transition rules. An important feature of SOS rules is negative premises, which are crucial in the definitions of such phenomena as priority mechanisms and time-outs. However, the inclusion of negative premises in SOS rules also introduces doubts as to the preferred meaning of SOS specifications.Orderings on SOS rules were proposed by Phillips and Ulidowski as an alternative to negative premises. Apart from the definition of the semantics of positive GSOS rules with orderings, the meaning of more general types of SOS rules with orderings has not been studied hitherto. This paper presents several candidates for the meaning of general SOS rules with orderings and discusses their conformance to our intuition for such rules.We take two general frameworks (rule formats) for SOS with negative premises and SOS with orderings, and present semantics-preserving translations between them with respect to our preferred notion of semantics. Thanks to our semantics-preserving translation, we take existing congruence meta-results for strong bisimilarity from the setting of SOS with negative premises into the setting of SOS with orderings. We further compare the expressiveness of rule formats for SOS with orderings and SOS with negative premises. The paper contains also many examples that illustrate the benefits of SOS with orderings and the properties of the presented definitions of meaning.     

GSOS for probabilistic transition systems: (extended abstract)

We introduce probabilistic GSOS, an operator specification format for (reactive) probabilistic transition systems which arises as an adaptation of the known GSOS format for labelled (nondeterministic) transition systems. Like the standard one, The format is well behaved in the sense that on all models bisimilarity is a congruence and the up-to-context proof principle is valid. Moreover, every specification has a final model which can be shown to offer unique solutions for guarded recursive equations. The format covers operator specifications from the literature, so that the well-behavedness results given for those arise as instances of our general one.The novel format was obtained via the following procedure: Turi and Plotkin have modelled specifications in the (standard) GSOS format and their models as natural transformations of a certain shape and a class of bialgebras identified by them. Several well-behavedness results for the concrete format can elegantly be proved in the categorical setting. Since the abstract framework is parametric in the type of system behaviour under consideration, it can be instantiated with that of probabilistic transition systems yielding a specification format for them, again in terms of specific natural transformations. The main contribution of this paper is the derivation of probabilistic GSOS as a rule-style representation of those.     

Variable binding operators in transition system specifications

In this paper the approach to structural operational semantics (SOS) using transition system specifications (TSSs) is extended to deal with variable binding operators and many-sortedness. Bisimulation and Verhoef's transition rule format, known as the panth format, generalize naturally to the new TSSs. It is shown that in this setting bisimulation is still a congruence for meaningful TSSs in panth format. Formats guaranteeing that bisimulation is a congruence are important for the application of TSSs to provide process calculi, and programming and specification languages, with an operational semantics. The new congruence result is relevant because in many of these applications, variable binding operators and many-sortedness are involved. It is also sketched how the presented approach can be further extended to deal with given sorts and parametrized transition relations. Given sorts are useful if the semantics of the terms of certain sorts has been given beforehand. This happens frequently in practice, as does the often related need of parametrized transition relations.     

A congruence rule format for name-passing process calculi

We introduce a GSOS-like rule format for name-passing process calculi. Specifications in this format correspond to theories in nominal logic. The intended models of such specifications arise by initiality from a general categorical model theory. For operational semantics given in this rule format, a natural behavioural equivalence—a form of open bisimilarity—is a congruence.     

A Congruence Rule Format with Universal Quantification

We investigate the addition of universal quantification to the meta-theory of Structural Operational Semantics (SOS). We study the syntax and semantics of SOS rules extended with universal quantification and propose a congruence rule format for strong bisimilarity that supports this new feature.     

SOS formats and meta-theory: 20 years after

In 1981 Structural Operational Semantics (SOS) was introduced as a systematic way to define operational semantics of programming languages by a set of rules of a certain shape [G.D. Plotkin, A structural approach to operational semantics, Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981]. Subsequently, the format of SOS rules became the object of study. Using so-called Transition System Specifications (TSS’s) several authors syntactically restricted the format of rules and showed several useful properties about the semantics induced by any TSS adhering to the format. This has resulted in a line of research proposing several syntactical rule formats and associated meta-theorems. Properties that are guaranteed by such rule formats range from well-definedness of the operational semantics and compositionality of behavioral equivalences to security-, time- and probability-related issues. In this paper, we provide an overview of SOS rule formats and meta-theorems formulated around them.     

A Hierarchy of SOS Rule Formats

In 1981 Structural Operational Semantics (SOS) was introduced as a systematic way to define operational semantics of programming languages by a set of rules of a certain shape [G.D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981. Also published in: Journal of Logic and Algebraic Programming 60–61 (2004) 17–140]. Subsequently, the format of SOS rules became the object of study. Using so-called Transition System Specifications (TSS's) several authors syntactically restricted the format of rules and showed several useful properties about the semantics induced by any TSS adhering to the format. This has resulted in a line of research proposing several syntactical rule formats and associated meta-theorems. Properties that are guaranteed by such rule formats range from well-definedness of the operational semantics and compositionality of behavioral equivalences to security- and probability-related issues. In this paper, we provide an initial hierarchy of SOS rules formats and meta-theorems formulated around them.     

A schematic axiom for open congruence

A schematic law dealing with localization operator is proposed for pi calculus. It is shown that the law renders the use of distinction unnecessary in the axiomatic theory of open congruence.     

Proof-Guided Test Selection from First-Order Specifications with Equality

This paper deals with test case selection from axiomatic specifications whose axioms are quantifier-free first-order formulas with equality. We first prove the existence of an ideal exhaustive test set to start the selection from. We then propose an extension of the test selection method called axiom unfolding, originally defined for algebraic specifications, to quantifier-free first-order specifications with equality. This method basically consists of a case analysis of the property under test (the test purpose) according to the specification axioms. It is based on a proof search for the different instances of the test purpose. Since the calculus is sound and complete, this allows us to provide a full coverage of this property. The generalisation we propose allows to deal with any kind of predicate (not only equality) and with any form of axiom and test purpose (not only equations or Horn clauses). Moreover, it improves our previous works with efficiently dealing with the equality predicate, thanks to the paramodulation rule.