Two classical semantical approaches to studying logics which combine time and modality are the T x W-frames and Kamp-frames (see thomason, 84). In this paper we study a new kind of frame that extends the one introduce...
详细信息
ISBN:
(纸本)0769514758
Two classical semantical approaches to studying logics which combine time and modality are the T x W-frames and Kamp-frames (see thomason, 84). In this paper we study a new kind of frame that extends the one introduced in [Burrieza and P. de Guzman(2002)]. the motivation is twofold: theoretical, i.e., representing properties of the basic theory of functions (definability);and practical, their use in computational applications (considering time-flows as memory of computers connected in a net, each computer with its own clock). Specifically, we present a temporal x modal (labelled) logic, whose semantics are given by ind-functional frames in which accessibility functions are used in order to interconnect time-flows. this way, we can: (i) specify to what time-flow we want to go;(ii) carry out different comparisons among worlds with different time measures, and (iii) define properties of certain kinds of functions (in particular, of total, injective, surjective, constant, increasing and decreasing functions), without the need to resort to second-order theories. In addition, we define a minimal axiomatic system and give the completeness theorem (Henkin-style).
the importance of highly fault-tolerant computing systems has widely been recognized In this paper we propose FPGA architecture with degrading strategy to increase fault-tolerance in a CPU. Previously, duplication and...
详细信息
ISBN:
(纸本)0769518524
the importance of highly fault-tolerant computing systems has widely been recognized In this paper we propose FPGA architecture with degrading strategy to increase fault-tolerance in a CPU. Previously, duplication and substitution methods have been proposed, but former methods waste redundant circuits and later methods increase computing speed as faults occur We propose a re-constitution method with FPGA technology. Using our method, execution speed of the CPU gradually decreases as permanent faults occur the CPU consists of functional Blocks(FB), that is re-configurable logic blocks. When a fault occures, the broken FB is discarded. As the number of valid FB decreases, function units of it is scaled down, therefore, exection time increases. In our simulation, speed degradation is less than 100% when 70% of whole FBs are broken. Compared with previous methods, speed degradation is smaller in case that many permanent faults occure.
In functional languages such as OBJ*, CafeOBJ, and Maude, symbols are given strategy annotations which specify (the order in) which subterms are evaluated. Syntactically, they are given either as lists of natural numb...
详细信息
ISBN:
(数字)9783540360780
ISBN:
(纸本)3540000100
In functional languages such as OBJ*, CafeOBJ, and Maude, symbols are given strategy annotations which specify (the order in) which subterms are evaluated. Syntactically, they are given either as lists of natural numbers or as lists of integers associated to function symbols whose (absolute) values refer to the arguments of the corresponding symbol. A positive index enables the evaluation of an argument whereas a negative index means "evaluate on-demand". While strategy annotations containing only natural numbers have been implemented and received some recent investigation endeavor (regarding, e.g., termination and completeness), fully general annotations (also called on-demand strategy annotations), which have been proposed to support laziness in OBJ-like languages, are disappointingly under-explored to date. In this paper, we first point out a number of problems of current proposals for handling on-demand strategy annotations. then, we propose a solution to these problems which is based on a suitable extension of the E-evaluation strategy of OBJ-like languages (that only considers annotations given as natural numbers) to on-demand strategy annotations. Our strategy incorporates a better treatment of demandness and also exhibits good computational properties;in particular, we show how to use it for computing (head-)normal forms. We also introduce a transformation for proving termination of the new evaluation strategy by using standard techniques.
functional languages have proven substantially useful for hosting embedded domain-specific languages. they provide an infrastructure rich enough to define both a convenient syntax for the embedded language, a type sys...
详细信息
Recent works by the authors address the problem of automating the selection of a candidate norm for the purpose of termination analysis. these works illustrate a powerful technique in which a collection of simple type...
详细信息
ISBN:
(纸本)3540442359
Recent works by the authors address the problem of automating the selection of a candidate norm for the purpose of termination analysis. these works illustrate a powerful technique in which a collection of simple type-based norms, one for each data type in the program, are combined together to provide the candidate norm. this paper extends these results by investigating type polymorphism. We show that by considering polymorphic types we reduce, without sacrificing precision, the number of type-based norms which should be combined to provide the candidate norm. Moreover, we show that when a generic polymorphic typed program component occurs in one or more specific type contexts, we need not reanalyze it. All of the information concerning its termination and its effect on the termination of other predicates in that context can be derived directly from the context independent analysis of that component based on norms derived from the polymorphic types.
We study the connection between algorithmic techniques for symbolic model checking [ACJT96,FS98,AJ99], and declarative and operational aspects of linear logicprogramming [And92,AP90]. Specifically, we show that the c...
详细信息
ISBN:
(纸本)3540417397
We study the connection between algorithmic techniques for symbolic model checking [ACJT96,FS98,AJ99], and declarative and operational aspects of linear logicprogramming [And92,AP90]. Specifically, we show that the construction used to decide verification problems for Timed Petri Nets [AJ99] can be used to define a new fixpoint semantics for the fragment of linear logic called LO [AP90]. the fixpoint semantics is based on an effective T-P operator. As an alternative to traditional top-down approaches [And92,AP90,APC93], the effective fixpoint operator. can be used to define a bottom-up evaluation procedure for first-order linear logic programs.
this paper describes LRoute, a novel router for the popular and scalable hierarchical Complex Programmable logic Devoices (CPLDs). CPLD routing has constraints om routing topologies due to architectural limitations an...
详细信息
ISBN:
(纸本)9781581133417
this paper describes LRoute, a novel router for the popular and scalable hierarchical Complex Programmable logic Devoices (CPLDs). CPLD routing has constraints om routing topologies due to architectural limitations and performance considerations. these constraints make the problem quite different from FPGA routing and render the routing problem more complicated. Extensions of popular FPGA routers like the maze router performs poorly on such CPLDs. there is also little published work on CPLD routing. LRoute uses a different paradigm based on the Lagrangian Relaxation framework in the theory of mathematical programming. It respects the topology constraints imposed and routes a circuit with minimum delay. We tested this router on a set of industry problems that commercial software failed to route. Our router was able to route all of them very quickly.
When Prolog programs that manipulate lists to manage a collection of resources are rewritten to take advantage of the linear logic resource management provided by the logicprogramming language Lolli, they can obtain ...
详细信息
the ability to tolerate defects in semiconductor devices has the potential for both increasing yields of devices being manufactured and making it economically feasible to manufacture even larger devices. While FPGA de...
详细信息
ISBN:
(纸本)9781581133417
the ability to tolerate defects in semiconductor devices has the potential for both increasing yields of devices being manufactured and making it economically feasible to manufacture even larger devices. While FPGA devices appear to be well suited to providing defect tolerance, practical application of existing research and techniques has been somewhat elusive. One barrier to acceptance is that existing defect tolerance techniques for FPGAs have tended to rely on either modifications to device architectures or modifications to design tools. We describe a software-based technique for providing defect tolerance which requires neither changes to device hardware or software tools. this approach uses the Xilinx JBits(tm) toolkit and operates at the core library level. Addressing defect tolerance locally using core library elements rather than taking a global approach helps provide direct support for run-time reconfiguration. Circuits may be configured and reconfigured rapidly in the presence of these defects. this rapid configuration also provides a path for practical use in more traditional manufacturing environments.
暂无评论