基于不变式生成的循环停机性验证

循环的停机性验证是程序验证中的一个难点。程序不变式用来描述程序变量的取值关系,其中线性不变式可以帮助描述程序变量间的线性关系,循环不变式能够有效刻画循环中的变量关系。本文基于线性不变式和多项式循环不变式的生成,将循环的停机性验证转化为求解一个最优化问题,给出了一个实用的程序停机性验证框架。基于该框架可以自动地验证程序的停机性,并给出循环的复杂度上界。实验结果说明了该方法的实用性。     

Matrix Interpretations for Proving Termination of Term Rewriting

We present a new method for automatically proving termination of term rewriting. It is based on the well-known idea of interpretation of terms where every rewrite step causes a decrease, but instead of the usual natural numbers we use vectors of natural numbers, ordered by a particular nontotal well-founded ordering. Function symbols are interpreted by linear mappings represented by matrices. This method allows us to prove termination and relative termination. A modification of the latter, in which strict steps are only allowed at the top, turns out to be helpful in combination with the dependency pair transformation. By bounding the dimension and the matrix coefficients, the search problem becomes finite. Our implementation transforms it to a Boolean satisfiability problem (SAT), to be solved by a state-of-the-art SAT solver.     

Towards a Systematic Method for Proving Termination of Graph Transformation Systems

We describe a method for proving the termination of graph transformation systems. The method is based on the fact that infinite reductions must include infinite ‘creation chains’, that is chains of edges in different graphs of the reduction sequence, such that each edge is involved in creating the next edge. In our approach, the length of such creation chains is recorded by associating with each edge label a creation depth, which denotes the minimal length of a creation chain from an edge in the initial graph to that edge. We develop an algorithm which can prove the absence of such infinite chains (and therefore termination), analyse problems of the approach and propose possible solutions.     

Termination for Hybrid Tableaus

This article extends and improves work on tableau-based decisionmethods for hybrid logic by Bolander and Braüner. Theirpaper gives tableau-based decision procedures for basic hybridlogic (with unary modalities) and the basic logic extended withthe global modality. All their proof procedures make use ofloop-checks to ensure termination.  Here we take a closer look at termination for hybrid tableaus.We cover both types of system used in hybrid logic: prefixedtableaus and internalized tableaus. We first treat prefixedtableaus. We prove a termination result for the basic language(with n-ary operators) that does not involve loop-checks. Wethen successively add the global modality and n-ary inversemodalities, show why various different types of loop-check arerequired in these cases, and then re-prove termination. Followingthis we consider internalized tableaus. At first sight, suchsystems seem to be more complex. However, we define a internalizedsystem which terminates without loop-checks. It is simpler thanpreviously known internalized systems (all of which requireloop-checks to terminate) and simpler than our prefix systems(no non-local side conditions on rules are required).     

项重写系统弱基终止性的归纳证明

1.引言项重写系统是一种受到广泛研究和应用的形式计算模型。一个项重写系统由一组称为重写规则的定向等式组成。例如,下面的R是一个由五个重写规则组成的、定义用({0,s})表示的自然数集N上的两倍函数d(x)=2×n:N→N的项重写系统:     

Theorem Proving Techniques for View Deletion in Databases

In this paper, we show how techniques from first-order theorem proving can be used for efficient deductive database updates. The key idea is to transform the given database, together with the update request, into a (disjunctive) logic program and to apply the hyper-tableau calculus (Baumgartner et al. 1996) to solve the original update problem. The resulting algorithm has the following properties: it works goal-directed (i.e. the search is driven by the update request), it is rational in the sense that it satisfies certain rationality postulates stemming from philosophical works on belief dynamics, and, unlike comparable approaches, it is of polynomial space complexity. To obtain soundness and completeness results, the hyper-tableau calculus is slightly modified for minimal model reasoning. Besides a direct proof we give an alternate proof which gives insights into the relation to previous approaches. As a by-product we thereby derive a soundness and completeness result of hyper-tableaux for computing minimal abductive explanations.     

An Algorithmic Toolbox for Network Calculus

Network calculus offers powerful tools to analyze the performances in communication networks, in particular to obtain deterministic bounds. This theory is based on a strong mathematical ground, notably by the use of (min,+) algebra. However, the algorithmic aspects of this theory have not been much addressed yet. This paper is an attempt to provide some efficient algorithms implementing network calculus operations for some classical functions. Some functions which are often used are the piecewise affine functions which ultimately have a constant growth. As a first step towards algorithmic design, we present a class containing these functions and closed under the main network calculus operations (min, max, +, −, convolution, subadditive closure, deconvolution): the piecewise affine functions which are ultimately pseudo-periodic. They can be finitely described, which enables us to propose some algorithms for each of the network calculus operations. We finally analyze their computational complexity.

Single Step Tableaux for Modal Logics

Single Step Tableaux (SST) are the basis of a calculus for modal logics that combines different features of sequent and prefixed tableaux into a simple, modular, strongly analytic, and effective calculus for a wide range of modal logics.The paper presents a number of the computational results about SST (confluence, decidability, space complexity, modularity, etc.) and compares SST with other formalisms such as translation methods, modal resolution, and Gentzen-type tableaux. For instance, it discusses the feasibility and infeasibility of deriving decision procedures for SST and translation-based methods by replacing loop checking techniques with simpler termination checks.The complexity of searching for validity and logical consequence with SST and other methods is discussed. Minimal conditions on SST search strategies are proven to yield Pspace (and NPtime for S5 and KD45) decision procedures. The paper also presents the methodology underlying the construction of the correctness and completeness proofs.     

几种量子程序终止的有效验证

基于文献巨18口提出的量子程序验证方法,讨论了单量子比特系统上比特翻转、去极化、幅值阻尼、相位阻尼等 信道刻画的量子程序的验证,通过选取不同的可观测算子对程序终止的情况进行了详细的讨论。研究表明,由这些量 子信道所描述的量子程序的终止情况不仅依赖于输入态的选取,还依赖于可观测算子的选取。     

群决策支持系统中的一致性分析技术

提出一些在群决策支持系统（ＧＤＳＳ）中支持协调员引导群体意见趋向一致的技术和方法。协调员利用决策群体成员所表达的模糊偏好数据计算出广义距离等一些软评价指标，能够获得群体意见一致程度和群体意见分歧程度等信息，发现“联盟”的子群体和存在严重意见分歧的决策备选对象等，从而掌握决策过程并引导群体意见趋向一致。结合一个应用实例说明如何使用该分析技术优化群决策过程。     

Proof Complexity of the Cut-free Calculus of Structures

We investigate the proof complexity of analytic subsystems ofthe deep inference proof system SKSg (the calculus of structures).Exploiting the fact that the cut rule (i) of SKSg correspondsto the ¬-left rule in the sequent calculus, we establishthat the ‘analytic'system KSg+c has essentially the samecomplexity as the monotone Gentzen calculus MLK. In particular,KSg+c quasipolynomially simulates SKSg, and admits polynomial-sizeproofs of some variants of the pigeonhole principle.     

Mechanizing Weakly Ground Termination Proving of Term Rewriting Systems by Structural and Cover-Set Inductions

The paper presents three formal proving methods for generalized weakly ground terminating property, i.e., weakly terminating property in a restricted domain of a term rewriting system, one with structural induction, one with cover-set induction, and the third without induction, and describes their mechanization based on a meta-computation model for term rewriting systems-dynamic term rewriting calculus. The methods can be applied to non-terminating, non-confluent and/or non-left-linear term rewriting systems. They can do "forward proving" by applying propositions in the proof, as well as "backward proving" by discovering lemmas during the proof.     

Some structural properties of SAT

The following four conjectures about structural of SAT are studied in this paper.(1) SAT∈P^SPARSE∩NP;(2)SAT∈SRTDtt;(3)SAT∈Ptt^bAPP;(4)FPtt^SAT=FTlog^SAT.It is proved that some pairs of these conjectures imply P=NP ,for example,if SAT∈P^SPARSE∩NP and SAT∈Ptt^bAPP,or if SAT∈SRTDtt and SAT∩PttbAPP,then P=NP.This improves previous results in literature.     

Complexity Measures for Process Evolution

The foundation for process evolution research is the modelling of process structural complexity. With such a model, process systems can be directed toward acquiring good maintainability attributes according to the principles of engineering. In this paper a process management (PM) model is developed to acquire directly from the target process codes the knowledge hidden among and within components of process systems. With the knowledge acquired by the PM model, process structural complexity measures in terms of partitioning, restructuring and rewriting criteria are developed; a systematic process remodularization schema is derived, and algorithms for scheduling process changes are presented. These criteria and mechanisms are used to guide the process production chain.     

A Guided Tour through some Extensions of the Event Calculus

Kowalski and Sergot's Event Calculus (EC) is a simple temporal formalism that, given a set of event occurrences, derives the maximal validity intervals (MVIs) over which properties initiated or terminated by these events hold. In this paper, we conduct a systematic analysis of EC by which we gain a better understanding of this formalism and determine ways of augmenting its expressive power. The keystone of this endeavor is the definition of an extendible formal specification of its functionalities. This formalization has the effects of casting determination of MVIs as a model checking problem, of setting the ground for studying and comparing the expressiveness and complexity of various extensions of EC, and of establishing a semantic reference against which to verify the soundness and completeness of implementations. We extend the range of queries accepted by EC, which is limited to Boolean combinations of MVI verification or computation requests, to support arbitrary quantification over events and modal queries. We also admit specifications based on preconditions. We demonstrate the added expressive power by encoding a number of diagnosis problems. Moreover, we provide a systematic comparison of the expressiveness and complexity of the various extended event calculi against each other. Finally, we propose a declarative encoding of these enriched event calculi in the logic programming language λProlog and prove the soundness and completeness of the resulting logic programs.     

Linear-Time Self-Interpretation of the Pure Lambda Calculus

We show that linear-time self-interpretation of the pure untyped lambda calculus is possible, in the sense that interpretation has a constant overhead compared to direct execution under various execution models. The present paper shows this result for reduction to weak head normal form under call-by-name, call-by-value and call-by-need.We use a self-interpreter based on previous work on self-interpretation and partial evaluation of the pure untyped lambda calculus.We use operational semantics to define each reduction strategy. For each of these we show a simulation lemma that states that each inference step in the evaluation of a term by the operational semantics is simulated by a sequence of steps in evaluation of the self-interpreter applied to the term (using the same operational semantics).By assigning costs to the inference rules in the operational semantics, we can compare the cost of normal evaluation and self-interpretation. Three different cost-measures are used: number of beta-reductions, cost of a substitution-based implementation (similar to graph reduction) and cost of an environment-based implementation.For call-by-need we use a non-deterministic semantics, which simplifies the proof considerably.