The model checking of higher-order recursion schemes (higher-order model checking for short) has been actively studied in the last decade, and has seen significant progress in both theory and practice. From a practica...
详细信息
ISBN:
(纸本)9780769544120
The model checking of higher-order recursion schemes (higher-order model checking for short) has been actively studied in the last decade, and has seen significant progress in both theory and practice. From a practical perspective, higher-order model checking provides a foundation for software model checkers for functional programming languages such as ML and Haskell. This short article aims to provide an overview of the recent progress in higher-order model checking and discuss future directions.
Information hiding and hierarchical decomposition are the corner stone of Software Engineering best practices. These principles have been applied in methods, architectures, programming languages, and run-time platform...
详细信息
Information hiding and hierarchical decomposition are the corner stone of Software Engineering best practices. These principles have been applied in methods, architectures, programming languages, and run-time platforms. It is therefore a big surprise to notice that the recent dynamic service platforms, like OSGi, do not make use of these principles. In OSGi, all services are visible; a client asking for an interface will be wired to any service, randomly selected and implementing that interface, which makes almost impossible protection and encapsulation. Nevertheless, OSGi is very successful for its almost unique capability to support dynamicity; and because the current practice is to run a single application per platform. Unfortunately, the future of gateways, like OSGi, is to manage the “discovery”, access and control of resources (logical as well as physical (sensors, devices)) shared by many applications. In the near future, OSGi will have to scale from a light weight mono-application gateway to a full-fledged dynamic platform. We have developed a layer on top of OSGi called APlication Abstract Machine (Apam) which provides OSGi dynamic capabilities, but also introduces a composite concept allowing multiple applications to cover the range isolation/collaboration from “black-box” (information hiding and hierarchical decomposition) to “scrambled eggs” as in service platforms, and through a variety of grey and white boxes with variable degrees of collaboration, sharing and control. The paper presents the state of practice, the challenges future dynamic platforms have to address, and how the Apam platform provides a solution to these issues. An assessment of the first Apam experimentations concludes the paper.
Weighted logicprogramming, a generalization of bottom-up logicprogramming, is a well-suited framework for specifying dynamic programming algorithms. In this setting, proofs correspond to the algorithm's output s...
详细信息
Weighted logicprogramming, a generalization of bottom-up logicprogramming, is a well-suited framework for specifying dynamic programming algorithms. In this setting, proofs correspond to the algorithm's output space, such as a path through a graph or a grammatical derivation, and are given a real-valued score (often interpreted as a probability) that depends on the real weights of the base axioms used in the proof. The desired output is a function over all possible proofs, such as a sum of scores or an optimal score. We describe the PRODUCT transformation, which can merge two weighted logic programs into a new one. The resulting program optimizes a product of proof scores from the original programs, constituting a scoring function known in machine learning as a "product of experts." Through the addition of intuitive constraining side conditions, we show that several important dynamic programming algorithms can be derived by applying PRODUCT to weighted logic programs corresponding to simpler weighted logic programs. In addition, we show how the computation of Kullback-Leibler divergence, an information-theoretic measure, can be interpreted using PRODUCT.
We introduce an approach to detecting inconsistencies in large biological networks by using answer set programming. To this end, we build upon a recently proposed notion of consistency between biochemical/genetic reac...
详细信息
We introduce an approach to detecting inconsistencies in large biological networks by using answer set programming. To this end, we build upon a recently proposed notion of consistency between biochemical/genetic reactions and high-throughput profiles of cell activity. We then present an approach based on answer set programming to check the consistency of large-scale data sets. Moreover, we extend this methodology to provide explanations for inconsistencies by determining minimal representations of conflicts. In practice, this can be used to identify unreliable data or to indicate missing reactions.
In this paper we propose an extension of Answer Set programming (ASP) to deal with (possibly partial) evaluable functions. To this aim, we start from the most general logical counterpart of ASP, Quantified Equilibrium...
详细信息
In this paper we propose an extension of Answer Set programming (ASP) to deal with (possibly partial) evaluable functions. To this aim, we start from the most general logical counterpart of ASP, Quantified Equilibrium logic (QEL), and propose a variant QEL(F)(=) where the set of functions is partitioned into Herbrand functions (or constructors) and evaluable functions (or operations). We show how this extension has a direct connection to Scott's logic of Existence, and introduce several useful derived operators, some of them directly borrowed from Scott's formalisation. Using this general framework for arbitrary theories, we proceed to focus on a syntactic subclass that corresponds to normal logic programs with evaluable functions and equality. We provide a translation of this class into function-free normal programs and consider a safety condition so that the resulting program is also safe, under the usual meaning in ASP. Finally, we also establish a formal comparison to Lin and Wang's approach (FASP) dealing with evaluable total functions.
Tabled evaluation is a recognized and powerful technique that overcomes some limitations of traditional Prolog systems in dealing with recursion and redundant subcomputations. We can distinguish two main categories of...
详细信息
Tabled evaluation is a recognized and powerful technique that overcomes some limitations of traditional Prolog systems in dealing with recursion and redundant subcomputations. We can distinguish two main categories of tabling mechanisms: suspension-based tabling and linear tabling. While suspension-based mechanisms are considered to obtain better results in general, they have more memory space requirements and are more complex and harder to implement than linear tabling mechanisms. Arguably, the SLDT and Dynamic Reordering of Alternatives (DRA) strategies are the two most successful extensions to standard linear tabled evaluation. In this work, we propose a new strategy, named dynamic reordering of solutions, and we present a framework, on top of the Yap system, that supports the combination of all these three strategies. Our implementation shares the underlying execution environment and most of the data structures used to implement tabling in Yap. We thus argue that all these common features allows us to make a first and fair comparison between these different linear tabling strategies and, therefore, better understand the advantages and weaknesses of each, when used solely or combined with the others.
Our goal is to study the feasibility of porting termination analysis techniques developed for one programming paradigm to another paradigm. In this paper, we show how to adapt termination analysis techniques based on ...
详细信息
Our goal is to study the feasibility of porting termination analysis techniques developed for one programming paradigm to another paradigm. In this paper, we show how to adapt termination analysis techniques based on polynomial interpretations-very well known in the context of term rewrite systems-to obtain new (nontransformational) termination analysis techniques for definite logic programs (LPs). This leads to an approach that can be seen as a direct generalization of the traditional techniques in termination analysis of LPs, where linear norms and level mappings are used. Our extension generalizes these to arbitrary polynomials. We extend a number of standard concepts and results on termination analysis to the context of polynomial interpretations. We also propose a constraint-based approach for automatically generating polynomial interpretations that satisfy the termination conditions. Based on this approach, we implemented a new tool, called Polytool, for automatic termination analysis of LPs.
Goal-level Independent and-parallelism (IAP) is exploited by scheduling for simultaneous execution of two or more goals, which will not interfere with each other at run time. This can be done safely even if such goals...
详细信息
Goal-level Independent and-parallelism (IAP) is exploited by scheduling for simultaneous execution of two or more goals, which will not interfere with each other at run time. This can be done safely even if such goals can produce multiple answers. The most successful IAP implementations to date have used recomputation of answers and sequentially ordered backtracking. While in principle simplifying the implementation, recomputation can be very inefficient if the granularity of the parallel goals is large enough and they produce several answers, while sequentially ordered backtracking limits parallelism. And, despite the expected simplification, the implementation of the classic schemes has proved to involve complex engineering, with the consequent difficulty for system maintenance and extension, while still frequently running into the well-known trapped goal and garbage slot problems. This work presents an alternative parallel backtracking model for IAP and its implementation. The model features parallel out-of-order (i.e., nonchronological) backtracking and relies on answer memoization to reuse and combine answers. We show that this approach can bring significant performance advantages. Also, it can bring some simplification to the important engineering task involved in implementing the backtracking mechanism of previous approaches.
Functional constraints and bi-functional constraints are an important constraint class in Constraint programming (CP) systems, in particular for Constraint logicprogramming (CLP) systems. CP systems with finite domai...
详细信息
Functional constraints and bi-functional constraints are an important constraint class in Constraint programming (CP) systems, in particular for Constraint logicprogramming (CLP) systems. CP systems with finite domain constraints usually employ Constraint Satisfaction Problem(s)-based solvers which use local consistency, for example, arc consistency. We introduce a new approach which is based instead on variable substitution. We obtain efficient algorithms for reducing systems involving functional and bi-functional constraints together with other nonfunctional constraints. It also solves globally any CSP where there exists a variable such that any other variable is reachable from it through a sequence of functional constraints. Our experiments on random problems show that variable elimination can significantly improve the efficiency of solving problems with functional constraints.
Nieuwenhuis et al. (2006. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM 53(6), 937977 showed how to describe enhancements of the Davis-Pu...
详细信息
Nieuwenhuis et al. (2006. Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM 53(6), 937977 showed how to describe enhancements of the Davis-Putnam-Logemann-Loveland algorithm using transition systems, instead of pseudocode. We design a similar framework for several algorithms that generate answer sets for logic programs: SMODELS, SMODELScc, asp-sat with Learning (CMODELS), and a newly designed and implemented algorithm sup. This approach to describe answer set solvers makes it easier to prove their correctness, to compare them, and to design new systems.
暂无评论