行为时序逻辑与自反线性时序逻辑的关系

为了能够将哲学逻辑中的公理系统运用到行为时序逻辑的研究中。对行为时序逻辑公式的语义进行形式化定义．从语义和语法两方面研究行为时序逻辑公理系统和具有自反性质的线性时序逻辑公理系统之间的联系．提出并证明行为时序逻辑公式转换为自反线性时序逻辑公式的定理。按照集合论和模型论的思想,定义行为时序逻辑中项和行为时序逻辑原子公式的概念。定义Lesilie Lamport所提出的行为时序逻辑公式的语义。证明自反线性时序逻辑公理系统适用于行为时序逻辑公理系统．以此为基础证明行为时序逻辑的简单规则、基本规则和附加规则。     

一个统一的程序验证框架

本文提出了一个简单的方法，其中程序和其性质都由一个逻辑：时序逻辑中的公式表示．文中给出了一个程序的转换模块的定义，提出了时序执行语义的概念．它是一个时序公式，精确地说明了一个程序．将时序逻辑作为规范语言，程序正确性就意味着说明程序的公式蕴含说明性质的公式，其中蕴含即为一般的逻辑蕴含．因此，本文的方法为并发程序的规范及验证提供了一个统一的框架．它允许充分利用现有的用于证明并发系统时序性质的各种完全证明系统．一个缓冲系统的简单例子用来说明本文的方法．此例子表明本文的方法是可行的.     

一种基于线性逻辑的时间Petri网推理方法

针对传统分析方法的不足 ,提出了时间 Petri网的线性逻辑表示和时间推理方法 .基于线性逻辑 ,定义了时间 Petri网中变迁之间的各种触发规则 ,在这些规则的基础上 ,提出了时间 Petri网运行行为的证明方法 ,此方法能清楚地分析时间 Petri网的运行行为和进行时间推理 .     

悖论逻辑的表演算

悖论逻辑ＬＰ是一个超协调逻辑，发展超协调逻辑（ＬＰ）的目的是使得不会从矛盾推出任一命题，但它有一个主要缺点：就是一些在经典逻辑中有效的推理在ＬＰ中不再有效；极小悖论逻辑ＬＰｍ能克服这个缺点，使得在没有矛盾的直接影响下超协调逻辑等价于经典逻辑．ＬＰ和ＬＰｍ原来都只给出语义定义，虽然已有ＬＰ的证明论，但如何得到一个ＬＰｍ的证明论仍是一个未解问题．本文提出了一种可靠与完全的表演算作为ＬＰ与ＬＰｍ的证明论．     

一种基于线性逻辑的时间Retri网推理方法

针对传统分析方法的不足,提出了时间Petri网的线性逻辑表示和时间推理方法。基于线性逻辑,定义了时间Petri网中变迁之间的各种解发规则,在这些规则的基础上,提出了时间Petri网运行行为的证明方法,此方法能清楚地分析时间Petri网的运行行为和进行时间推理。     

交互作用网理论分析

交互作用网是Lafont于1990年在POPL会议上提出的一种程序设计语言.本文我们从证明和程序的关系出发,使用线性逻辑作为一种集成逻辑讨论交互作用网的理论性质,得到下述结论:·网上结点辅助端口的划分可表示成相应类型的张量积;·网上的计算等价于线性矢列演算中Principal-Cut的消去;·对于任何一个交互作用网,如果存在一个线性矢列演算与之对应,则该网是简单的.     

一类排污问题在树图上的线性算法

ＭＥＧＩＤＤＯ等人证明了图搜索问题的ＮＰ完全性并给出一个树图上的算法，可在Ｏ（ｎ）时间内求解树的搜索数，在Ｏ（ｎｌｏｇ（ｎ））时间内求解树搜索方案．本文通过引入搜索方案边序表示法给出一个线性算法，可在Ｏ（ｎ）时间内同时求得树的搜索数和搜索方案．     

基于标记逻辑的非单调推理（Ⅰ）

我们把标记逻辑定义在一个特殊双格上,通过比较标记选取结论,从而同时捕捉超协调（容错）推理和非单调推理．本文介绍标记逻辑程序的句法与语义构造,提出诱导序列及其极限的概念,给出极限存在的等价条件,并证明一个重要结果：诱导序列基本定理,它是后续讨论的基础．     

逻辑框架的语法、语用及语义——(I)新型逻辑框架的语法和语用*

逻辑框架是用以定义逻辑的类型系统．在爱丁堡逻辑框架ELF(Edinburgh logical frame-work)和马丁诺夫逻辑框架的基础上，本文提出了一个集两者优点于一身的新型逻辑框架．此逻辑框架特别适用于语义分析．文中还给出一些如何在此逻辑框架中表示目标语言的应用实例．     

Grzegorczyk分层的一种延伸

本文讨论某些递归函数类的分层问题．首先给出的是原始的Ｇｏｒｚｅｇｏｒｃｚｙｋ分层的一种较为简单的等价定义．然后，作为对Ａｃｋｅｒｍａｎｎ函数的一种推广，定义了一个递归函数序列｛Ａ_ｎ｝_ｎ∈ω．并以此作为分层函数列定义了一种新的递归分层｛Ｚ_ｎ｝_ｎ∈ω（即Ｚ—分层），这种分层涉及了比原始递归函数类更大的一个违归函数类．实际上，原始递归函数类仅是Ｚ—分层的第一层Ｚ_０．而且这种分层的任意的第ｎ＋１层都含     

Recursion from iteration

In a simply-typed, call-by-value (CBV) language with first-class continuations, the usual CBV fixpoint operator can be defined in terms of a simple, infinitely-looping iteration primitive. We first consider a natural but flawed definition, based on exceptions and “iterative deepening” of finite unfoldings, and point out some of its shortcomings. Then we present the proper construction using full first-class continuations, with both an informal derivation and a proof that the behavior of the defined operator faithfully mimics a “built-in” recursion primitive. In fact, given an additional uniformity assumption, the construction is a two-sided inverse of the usual definition of iteration from recursion. Continuing, we show that the CBV looping primitive is in fact the direct-style equivalent of a continuation-passing-style fixpoint, and that this correspondence extends all the way to traditional definitions of these operators in terms of reflexive types.     

The Quantization Property of Probability Distributions of the Characteristics of Dynamic Systems Observed in the Presence of Random Disturbances

The class of linear stochastic dynamic systems is defined, such that the laws of the probability distribution of values of output signals of a system are determined by its equations complying with the case of the absence of random disturbances. These distribution laws are found to be similar to the quantum laws of the distribution values of observable physical quantities. On this basis, a possibility of the definition of the quantum systems as systems of this class is investigated. It is shown that the theoretical proof of some axioms of quantum mechanics and new facts requiring the experimental verification follow from this definition.     

Dialectic proof procedures for assumption-based, admissible argumentation

We present a family of dialectic proof procedures for the admissibility semantics of assumption-based argumentation. These proof procedures are defined for any conventional logic formulated as a collection of inference rules and show how any such logic can be extended to a dialectic argumentation system.The proof procedures find a set of assumptions, to defend a given belief, by starting from an initial set of assumptions that supports an argument for the belief and adding defending assumptions incrementally to counter-attack all attacks.The proof procedures share the same notion of winning strategy for a dispute and differ only in the search strategy they use for finding it. The novelty of our approach lies mainly in its use of backward reasoning to construct arguments and potential arguments, and the fact that the proponent and opponent can attack one another before an argument is completed. The definition of winning strategy can be implemented directly as a non-deterministic program, whose search strategy implements the search for defences.     

Describing software architecture styles using graph grammars

We believe that software architectures should provide an appropriate basis for the proof of properties of large software. This goal can be achieved through a clearcut separation between computation and communication and a formal definition of the interactions between individual components. We present a formalism for the definition of software architectures in terms of graphs. Nodes represent the individual agents and edges define their interconnection. Individual agents can communicate only along the links specified by the architecture. The dynamic evolution of an architecture is defined independently by a “coordinator”. An architecture style is a class of architectures specified by a graph grammar. The class characterizes a set of architectures sharing a common communication pattern. The rules of the coordinator are statically checked to ensure that they preserve the constraints imposed by the architecture style     

优先级顶协议的形式化验证

优先级顶协议是一种优先级驱动的抢占式调度协议,它具有无死锁和单阻塞的性质.Dang Van Hung 和Philip Chan在文献[6]中形式地规范和验证了这两个性质.但他们没有对状态函数HiPripcp明确定义,这使得验证的细节较难理解.为了解决这个问题,提出了一种新的方法来验证优先级顶协议单阻塞的性质.通过时段演算的方法,对优先级顶协议进行了规范,并给出了状态函数HiPripcp的明确定义.根据优先级顶协议的规范,形式地验证了该协议的单阻塞性质.采用的验证方法更少地依赖于HiPripcp,这使得验证的细节更易于理解.此外,提出的验证方法可被应用于实时数据库系统中类似协议的形式化验证.     

Inductively Verifying Invariant Properties of Parameterized Systems

Verification of distributed algorithms can be naturally cast as verifying parameterized systems, the parameter being the number of processes. In general, a parameterized concurrent system represents an infinite family (of finite state systems) parameterized by a recursively defined type such as chains, trees. It is therefore natural to verify parameterized systems by inducting over this type. However, construction of such proofs require combination of model checking with deductive capability. In this paper, we develop a logic program transformation based proof methodology which achieves this combination. One of our transformations (unfolding) represents a single resolution step. Thus model checking can be achieved by repeated application of unfolding. Other transformations (such as folding) represent deductive reasoning and help recognize the induction hypothesis in an inductive proof. Moreover the unfolding and folding transformations can be arbitrarily interleaved in a proof, resulting in a tight integration of decision procedures (such as model checking) with deductive verification.Based on this technique, we have designed and implemented an invariant prover for parameterized systems. Our proof technique is geared to automate nested induction proofs which do not involve strengthening of induction hypothesis. The prover has been used to automatically verify invariant properties of parameterized cache coherence protocols, including broadcast protocols and protocols with global conditions. Furthermore, we have employed the prover for automatic verification of mutual exclusion in the Java Meta-Locking Algorithm. Meta-Locking is a distributed algorithm developed recently by designers in Sun Microsystems for ensuring secure access of Java objects by an arbitrary number of Java threads.     

RESTRICTING THE WEAK-GENERATIVE CAPACITY OF SYNCHRONOUS TREE-ADJOINING GRAMMARS

The formalism of synchronous tree-adjoining grammars, a variant of standard tree-adjoining grammars (TAG), was intended to allow the use of TAGs for language transduction in addition to language specification. In previous work, the definition of the transduction relation defined by a synchronous TAG was given by appeal to an iterative rewriting process. The rewriting definition of derivation is problematic in that it greatly extends the expressivity of the formalism and makes the design of parsing algorithms difficult if not impossible. We introduce a simple, natural definition of synchronous tree-adjoining derivation, based on isomorphisms between standard tree-adjoining derivations, that avoids the expressivity and implementability problems of the original rewriting definition. The decrease in expressivity, which would otherwise make the method unusable, is offset by the incorporation of an alternative definition of standard tree-adjoining derivation, previously proposed for completely separate reasons, thereby making it practical to entertain using the natural definition of synchronous derivation. Nonetheless, some remaining problematic cases call for yel more flexibility in the definition; the isomorphism requirement may have to be relaxed. It remains for future research to rune the exact requirements on the allowable mappings.     

Specification and Verification of Concurrent Programs Through Refinements

We present a framework for the specification and verification of reactive concurrent programs using general-purpose mechanical theorem proving. We define specifications for concurrent programs by formalizing a notion of refinements analogous to stuttering trace containment. The formalization supports the definition of intuitive specifications of the intended behavior of a program. We present a collection of proof rules that can be effectively orchestrated by a theorem prover to reason about complex programs using refinements. The proof rules systematically reduce the correctness proof for a concurrent program to the definition and proof of an invariant. We include automated support for discharging this invariant proof with a predicate abstraction tool that leverages the existing theorems proven about the components of the concurrent programs. The framework is integrated with the ACL2 theorem prover and we demonstrate its use in the verification of several concurrent programs in ACL2.