检索结果-内蒙古大学图书馆

constraints-driven design space exploration for distributed embedded systems

JOURNAL OF SYSTEMS ARCHITECTURE 2001年第3-4期47卷 241-261页

作者： Kuchcinski, K Lund Inst Technol Dept Comp Sci Lund Sweden

This paper presents a new method for design space exploration for distributed embedded systems. The method is based on constraint logic programming (CLP) and make it possible to model distributed embedded systems and design requirements using finite domain constraints. Design space exploration tools can then use this model to find different solutions satisfying constraints. An advantage of this method is its flexibility to defined design constraints and ability to mix both manual design decisions and automatic optimization methods. The solution of the set of constraints provides a final system implementation which, by definition, satisfies all imposed design constraints. Both algorithms guaranteeing optimal solutions and heuristic methods can be used in the optimization phase. (C) 2001 Elsevier Science B.V. All rights reserved.

关键词： embedded systems distributed systems design space exploration constraint logic programming

来源：评论

学校读者我要写书评

暂无评论

Optimal placement of valves in a water distribution network with CLP(FD)

引用

THEORY AND PRACTICE OF logic programming 2011年第4-5期11卷 731-747页

作者： Cattafi, Massimiliano Gavanelli, Marco Nonato, Maddalena Alvisi, Stefano Franchini, Marco Univ Ferrara Dept Engn I-44122 Ferrara Italy

This paper presents a new application of logic programming to a real-life problem in hydraulic engineering. The work is developed as a collaboration of computer scientists and hydraulic engineers, and applies constraint logic programming to solve a hard combinatorial problem. This application deals with one aspect of the design of a water distribution network, i.e., the valve isolation system design. We take the formulation of the problem by Giustolisi and Savic (2008 Optimal design of isolation valve system for water distribution networks. In Proceedings of the 10th Annual Water Distribution Systems Analysis Conference WDSA2008, J. Van Zyl, A. Ilemobade, and H. Jacobs, Eds.) and show how, thanks to constraint propagation, we can get better solutions than the best solution known in the literature for the Apulian distribution network. We believe that the area of the so-called hydroinformatics can benefit from the techniques developed in constraint logic programming and possibly from other areas of logic programming, such as Answer Set programming.

关键词： constraint logic programming hydraulic engineering valve placement graph partitioning

来源：评论

学校读者我要写书评

暂无评论

A semantics for modular general logic programs

引用

THEORETICAL COMPUTER SCIENCE 1998年第1-2期206卷 51-80页

作者： Etalle, S Univ Amsterdam Fac WINS NL-1098 SJ Amsterdam Netherlands Univ Genoa Dept Comp Sci I-16126 Genoa Italy

Modular programs are built as a combination of separate modules, which may be developed and verified separately. Therefore, in order to reason over such programs, compositionality plays a crucial role: the semantics of the whole program must be obtainable as a simple function from the semantics of its individual modules. In the field of logic programming, the need for a compositional semantics has been long recognized, however, while for definite (i.e. negation-free) logic programs a few such semantics have been proposed, in the literature of normal logic programs (programs which employ the negation operator), compositionality has received scarce attention. This is mainly due to the fact that normal programs typically have a nonmonotonic behavior, which is difficult to fit in a compositional framework. Here we propose a declarative compositional semantics for general logic programs. First, a compositional semantics for first-order modules is presented and proved correct wrt the set of logical consequences of the module in three-valued logic. In a second stage, the obtained results are applied to modular normal logic programs, obtaining a semantics which is correct with respect to the set of logical consequences of the completion of the program and - in contrast with the other approaches - which is always computable. This semantics might be regarded as a compositional counterpart of Kunen's semantics. Finally we discuss and show how these results have to be modified in order to be applied to normal constraint logic programs. (C) 1998-Elsevier Science B.V. All rights reserved.

关键词： logic programming modularity open programs negation semantics constraint logic programming

来源：评论

学校读者我要写书评

暂无评论

Independence in CLP languages

引用

ACM TRANSACTIONS ON programming LANGUAGES AND SYSTEMS 2000年第2期22卷 296-339页

作者： De la Banda, MG Hermenegildo, M Marriott, K Monash Univ Melbourne Vic 3004 Australia Tech Univ Madrid UPM Madrid Spain

Studying independence of goals has proven very useful in the context of logic programming. In particular, it has provided a formal basis for powerful automatic parallelization tools, since independence ensures that two goals may be evaluated in parallel while preserving correctness and efficiency. We extend the concept of independence to constraint logic programs (CLP) and prove that it also ensures the correctness and efficiency of the parallel evaluation of independent goals. Independence for CLP languages is more complex than for logic programming as search space preservation is necessary but no longer sufficient for ensuring correctness and efficiency Two additional issues arise. The first is that the cost of constraint solving may depend upon the order constraints are encountered. The second is the need to handle dynamic scheduling. We clarify these issues by proposing various types of search independence and constraint solver independence, and show how they can be combined to allow different optimizations, from parallelism to intelligent backtracking. Sufficient conditions for independence which can be evaluated "a priori" at run-time are also proposed. Our study also yields new insights into independence in logic programming languages. In particular, we show that search space preservation is not only a sufficient but also a necessary condition for ensuring correctness and efficiency of parallel execution.

关键词： languages performance constraint logic programming independence parallelism

来源：评论

学校读者我要写书评

暂无评论

On the algebraic structure of declarative programming languages

引用

THEORETICAL COMPUTER SCIENCE 2009年第46期410卷 4626-4671页

作者： Amato, Gianluca Lipton, James McGrail, Robert Univ G dAnnunzio Dipartimento Sci I-65127 Pescara Italy Wesleyan Univ Dept Math Middletown CT 06459 USA Bard Coll Annandale on Hudson NY USA

We develop an algebraic framework, logic programming Doctrines, for the syntax, proof theory, operational semantics and model theory of Horn Clause logic programming based on indexed premonoidal categories. Our aim is to provide a uniform framework for logic programming and its extensions capable of incorporating constraints, abstract data types, features imported from other programming language paradigms and a mathematical description of the state space in a declarative manner. We define a new way to embed information about data into logic programming derivations by building a sketch-like description of data structures directly into an indexed category of proofs. We give an algebraic axiomatization of bottom-up semantics in this general setting, describing categorical models as fixed points of a continuous operator. (C) 2009 Elsevier B.V. All rights reserved.

关键词： Categorical logic Indexed categories logic programming Abstract data types constraint logic programming

来源：评论

学校读者我要写书评

暂无评论

SMT solving for the validation of B and Event-B models

引用

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER 2022年第6期24卷 1043-1077页

作者： Schmidt, Joshua Leuschel, Michael Univ Dusseldorf Inst Informat Univ Str 1 D-40225 Dusseldorf Germany

ProB provides a constraint solver for the B-method written in Prolog and can make use of different backends based on SAT and SMT solving. One such backend translates B and Event-B operators to SMT-LIB using the Z3 solver. This translation uses quantifiers to axiomatize some operators, which are not well-handled by Z3. Several relational constraints such as the transitive closure are not supported by this translation. In this article, we substantially improve the translation to SMT-LIB by employing a more constructive rather than axiomatized style using Z3's lambda function. Thereby, we are able both to translate more B and Event-B operators to SMT-LIB and improve the overall performance. We further extend ProB's interface to Z3 to run different solver configurations in parallel. In addition, we present a direct implementation of SMT solving in Prolog using ProB's constraint solver as a theory solver. We hereby aim to combine the strengths of conflict-driven clause learning for identifying contradictions with ProB's constraint solver for finding solutions. We deem this implementation to be worthwhile since ProB's constraint solver is tailored toward solving B and Event-B constraints, and we herewith avoid the dependency on an external SMT solver. Empirical results show that the new integration of Z3 has improved performance of constraint solving and enables to solve several constraints which cannot be solved by ProB's constraint solver. Furthermore, the direct implementation of SMT solving in ProB shows benefits compared to ProB's constraint solver and the integration of Z3.

关键词： SMT solving Z3 constraint logic programming ProB B-method Event-B

来源：评论

学校读者我要写书评

暂无评论

Global analysis of constraint logic programs

引用

ACM TRANSACTIONS ON programming LANGUAGES AND SYSTEMS 1996年第5期18卷 564-614页

作者： DeLaBanda, MG Hermenegildo, M Bruynooghe, M Dumortier, V Janssens, G Simoens, W KATHOLIEKE UNIV LEUVEN DEPT COMP SCIB-3001 HEVERLEEBELGIUM

This article presents and illustrates a practical approach to the dataflow analysis of constraint logic programming languages using abstract interpretation. It is first argued that, from the framework point of view, it suffices to propose relatively simple extensions of traditional analysis methods which have already been proved useful and practical and for which efficient fixpoint algorithms exist. This is shown by proposing a simple extension of Bruynooghe's traditional framework which allows it to analyze constraint logic programs. Then, and using this generalized framework, two abstract domains and their required abstract functions are presented: the first abstract domain approximates definiteness information and the second one freeness. Finally, an approach for combining those domains is proposed. The two domains and their combination have been implemented and used in the analysis of CLP(R) and Prolog-III applications. Results from this implementation showing its performance and accuracy are also presented.

关键词： languages abstract interpretation constraint logic programming global program analysis program analysis

来源：评论

学校读者我要写书评

暂无评论

CLP(χ) for automatically proving program properties

引用

JOURNAL OF logic programming 1998年第1-3期37卷 77-93页

作者： Mesnard, F Hoarau, S Maillard, A Univ Reunion Iremia F-97715 St Denis 9 France

Various proof methods have been proposed to solve the implication problem, i.e. proving that properties of the form: For All(P --> Q) - where P and Q denote conjunctions of atoms - are logical consequences of logic programs. Nonetheless, it is commonplace to say that it is still quite a difficult problem. Besides, the advent of the constraint logic programming scheme constitutes not only a major step towards the achievement of efficient declarative logic programming systems but also a new held to explore. By recasting and simplifying the implication problem in the constraint logic programming (CLP) framework, we define a generic proof method for the implication problem, which we prove sound from the algebraic point of view. We present four examples using CLP(N), CLP(RT), CLP(Sigma*) and RISC-CLP(R). The logical point of view of the constraint logic programming scheme enables the automation of the proof method. At last, we prove the unsolvability of the implication problem, we point out the origins of the incompleteness of the proposed proof method and we identify two classes of programs for which we give a decision procedure for the implication problem. (C) 1998 Elsevier Science Inc. All rights reserved.

关键词： constraint logic programming verifying and reasoning about programs proof theory

来源：评论

学校读者我要写书评

暂无评论

Controlling Polyvariance for Specialization-based Verification

引用

FUNDAMENTA INFORMATICAE 2013年第4期124卷 483-502页

作者： Fioravanti, Fabio Pettorossi, Alberto Proietti, Maurizio Senni, Valerio Univ G dAnnunzio I-65127 Pescara Italy Univ Roma Tor Vergata I-00133 Rome Italy IASI CNR I-00185 Rome Italy IMT Inst Adv Studies Lucca I-55100 Lucca Italy

Program specialization has been proposed as a means of improving constraint-based analysis of infinite state reactive systems. In particular, safety properties can be specified by constraint logic programs encoding (backward or forward) reachability algorithms. These programs are then transformed, before their use for checking safety, by specializing them with respect to the initial states (in the case of backward reachability) or with respect to the unsafe states (in the case of forward reachability). By using the specialized reachability programs, we can considerably increase the number of successful verifications. An important feature of specialization algorithms is the so called polyvariance, that is, the number of specialized variants of the same predicate that are introduced by specialization. Depending on this feature, the specialization time, the size of the specialized program, and the number of successful verifications may vary. We present a specialization framework which is more general than previous proposals and provides control on polyvariance. We demonstrate, through experiments on several infinite state reactive systems, that by a careful choice of the degree of polyvariance we can design specialization-based verification procedures that are both efficient and precise.

关键词： Program specialization constraint logic programming polyvariance generalization verification of infinite state reactive systems unfold/fold transformation

来源：评论

学校读者我要写书评

暂无评论

Improving PARMA trailing

引用

THEORY AND PRACTICE OF logic programming 2006年第0期6卷 609-644页

作者： Schrijvers, Tom Demoen, Bart De la Banda, Maria Garcia Stuckey, Peter J. Katholieke Univ Leuven Dept Comp Sci Louvain Belgium Monash Univ Sch Comp Sci & Software Engn Clayton Vic 3168 Australia Univ Melbourne Dept Comp Sci & Software Engn NICTA Victoria Lab Parkville Vic 3052 Australia

Taylor introduced a variable binding scheme for logic variables in his PARMA system, that uses cycles of bindings rather than the linear chains of bindings used in the standard WAM representation. Both the HAL and dProlog languages make use of the PARMA representation in their Herbrand constraint solvers. Unfortunately, PARMA's trailing scheme is considerably more expensive in both time and space consumption. The aim of this paper is to present several techniques that lower the cost. First, we introduce a trailing analysis for HAL using the classic PARMA trailing scheme that detects and eliminates unnecessary trailings. The analysis, whose accuracy comes from HAL's determinism and mode declarations, has been integrated in the HAL compiler and is shown to produce space improvements as well as speed improvements. Second, we explain how to modify the classic PARMA trailing scheme to halve its trailing cost. This technique is illustrated and evaluated both in the context of dProlog and HAL. Finally, we explain the modifications needed by the trailing analysis in order to be combined with our modified PARMA trailing scheme. Empirical evidence shows that the combination is more effective than any of the techniques when used in isolation.

关键词： constraint logic programming program analysis trailing

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：