Delay considerttion has been a major issue in design and test of high performance digital circuits . The assumption of input signal change occurring only when all internal nodes are stable restricts the increase of clock frequency. It is no longer true for wave pipelining circuits. However, previous logical delay models are based on the assumption. In addition, the stable time of a robust delay test generally depends on the longest sensitizable path delay. Thus , a new delay model is desirable. This paper e…

With the rapid development and wide applicatioos of computing systems on which more reliance hu been put, a dependable syatem will be much more important than ever. This paper is hrst aimed at giving informal but precise definitions characterizing the various attributes of dependability of computing sys- tems and then the importance of (and the relationshipa among) all the attributes are explained . Dependability is first introduced as a global concept which subsumes the usual attributea of reliability, ava…

In this paper, the relationship between the second order typed - calculus 2 and its higher order version is discussed . A purely syntactic proof of the conservativity of over 2 is given.

We use a many-sorted language to remove commutativity from phase semantics of linear logic and show that pure noncommutative intuitionistic linear propositional logic plus two classical rules enjoys the soundness and complete- ness with respect to completely noncommutative phue semantics.

Receatly, Giordano and Martelli ( 1994) proposed two new cumu- lative variants of Reiter's default logic (DL) : Commitment to Assumptions Default Logic (CADL) and Quasi-Default Logic (QDL). They have only given quasi-inductive characterizations of extensions for the two variants. In this paper, finite characteri- zatioas of extensions for CADL and QDL by applying notions of (joint) compatibility are presented respectively. And corresponding algorithms and complexity results for reasoning are obtairfed.

A new approach to deciding quasi-reducibility is proposed by intro- ducing witnesses. Furthermore, an algorithm for constructing witnessed test sets of lelh-linear rewrite systems h. been designed. Compared with the standard test set approach presented by Kapur, Narendran and Zhang, the method proposed generates test sets of smaller size and therefore has more efficient applications .

A fast and efficient parallel algorithm for finding a maximal edge matching in an undirected graph G(V,E) is proposed. It runs in O(logn) time with O(m/log+n+n) processors on an EREW PRAM for a class of graph set Ⅱ, where n=V, m = E and Ⅱ includes at leut (i) planar graphs; (ii) graphs of bounded genus; and (iii) graphs of bounded maximum degree and so on. Our algorithm improves the previoualy known best algoritbms by a factor of logn in the time complexity…

In common sense reasoning two typical types of defaults are encoun- tered. One is of the form "All birds can fly except b1, b2,…, and bm(m>1)" , and the other "All birds can fly, but there exist exceptiona" . The first type of defaults is readily formalized but the other, as some researchers have noticed, is difficult to deal witb. This paper establisbes a geaeral scheme for formalising defaults of the two typea, the key to which is the introduction of a two-argument predicate ab(I,S) to represent exception…

Refutation methods based on the resolution principle are generally applied to a (finite) set of sentences, which must have a series of pre-transformations (prenex normalization, Skolemization and conjunction normalization) before starting the refutation. In this paper, the authors first generalize the concept of abatract consistency class to the most general form-universal abstract consistency class, and prove its universal unifying principle. Then, based on the R-refutation, a universal refutation method i…

Mean Value Calculus ( MVC) is a real-time logic which can be used to specify and verify real-time systems . As a conservative extension of Duration Calculus (DC) , MVC increases the expressive power but keeps the properties of DC . ln this paper we present decidability results of MVC . An interesting result is that propositional MVC with chop star operator is still decidable, which develops the results or and .

This paper presents a new interconnection net work topology ,called The twisted-cube connected network is a variant of the hypercube, and it has a better recursive structure . The regularity, connectivities, subgraphs of the twisted- cube conaected aetwork are studied . The twisted-cube connected network is proved to be a 3-cube-free network, which is the essential difference from the hypercube and variants of the hypercube. An efficient routing algorithm is proposed, and the diameter of n-dimensional twist…

This paper proposes a new approach to modeling multimedia data. The new approach is the multimedia data model bued on temporal logic and XYZ System. lt supports the formal specifications in a multimedia system. Using this model, we can not only speci. information units but also design and script a multi. media title ia an unified framework. Based on this model, an interactive multimedia authoring environment has beea developed .