We describe a parameterized framework with which users can take advantage of unification over analysis variables to implement efficient or precise analyses, or even both. To be illustrative we instantiate the framewor...
详细信息
ISBN:
(纸本)9783540787686
We describe a parameterized framework with which users can take advantage of unification over analysis variables to implement efficient or precise analyses, or even both. To be illustrative we instantiate the framework with reaching definition analysis and conduct a systematic evaluation of performance and precision of the analysis. We compare our result withthat of a state-of-the-art solver, the Succinct Solver and show our solver is at least 10-times faster than the Succinct Solver. On some benchmarks linearity is reached by the use of unification. Although the result of unification is often imprecise, a heuristic study is conducted to detect where the loss of precision may happen. We apply the heuristics on benchmarks and achieve not only efficient but also precise analysis.
the increasing availability of smart objects demands for flexible mechanisms to orchestrate different types of these objects to smart environments. As smart objects are typically not aware of each other, an orchestrat...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
the increasing availability of smart objects demands for flexible mechanisms to orchestrate different types of these objects to smart environments. As smart objects are typically not aware of each other, an orchestrating platform has to manage common resources, to harmonize the individual behavior of the acting objects, and to combine their activities to an intelligent team work. this paper presents a corresponding framework to implement such an orchestrating platform. It provides a concurrent programming language representing states in Description logics and state transitions as logical updates enabling deductive support to infer non-explicitly represented knowledge. It uses temporal logic to suspend execution of a process for a particular evolution of the global state that is specified by a LTL formula. Since a process can fork into subprocesses this provides a mechanism for runtime verification by splitting a process into a subprocess executing some critical program and another parallel subprocess monitoring the first one by waiting for the desired evolution of states specified in its LTL formula.
An offline approach to narrowing-driven partial evaluation (a partial evaluation scheme for first-order functional and functional logicprograms) has recently been introduced. In this approach, program annotations (i....
详细信息
ISBN:
(纸本)9783540714095
An offline approach to narrowing-driven partial evaluation (a partial evaluation scheme for first-order functional and functional logicprograms) has recently been introduced. In this approach, program annotations (i.e., the expressions that should be generalised at partial evaluation time to ensure termination) are based on a simple syntactic characterisation of quasi-terminating programs. this work extends the previous offline scheme by introducing a new annotation strategy which is based on a combination of size-change graphs and binding-time analysis. Preliminary experiments point out that the number of program annotations is significantly reduced compared to the previous approach, which means that faster residual programs are often produced.
We provide an approach to formally analyze the computational behavior of coroutines in logicprograms and to compile these computations into new programs, not requiring any support for coroutines. the problem was alre...
详细信息
ISBN:
(纸本)9783319178226;9783319178219
We provide an approach to formally analyze the computational behavior of coroutines in logicprograms and to compile these computations into new programs, not requiring any support for coroutines. the problem was already studied near to 30 years ago, in an analysis and transformation technique called Compiling Control. However, this technique had a strong ad hoc flavor: the completeness of the analysis was not well understood and its symbolic evaluation was also very ad hoc. We show how Abstract Conjunctive Partial Deduction, introduced by Leuschel in 2004, provides an appropriate setting to redefine Compiling Control. Leuschel's framework is more general than the original formulation, it is provably correct, and it can easily be applied for simple examples. We also show that the Abstract Conjunctive Partial Deduction framework needs some further extension to be able to deal with more complex examples.
Reactive synthesis transforms a specification of a reactive system, given in a temporal logic, into an implementation. the main advantage of synthesis is that it is automatic. the main disadvantage is that the impleme...
详细信息
ISBN:
(数字)9783030591526
ISBN:
(纸本)9783030591526;9783030591519
Reactive synthesis transforms a specification of a reactive system, given in a temporal logic, into an implementation. the main advantage of synthesis is that it is automatic. the main disadvantage is that the implementation is usually very difficult to understand. In this paper, we present a new synthesis process that explains the synthesized implementation to the user. the process starts with a simple version of the specification and a corresponding simple implementation. then, desired properties are added one by one, and the corresponding transformations, repairing the implementation, are explained in terms of counterexample traces. We present SAT-based algorithms for the synthesis of repairs and explanations. the algorithms are evaluated on a range of examples including benchmarks taken from the SYNTCOMP competition.
the traditional stepwise refinement basedprogram derivation methodologies are primarily top-down. Strictly following the top-down program derivation approach may require backtracking resulting in rework. Moreover, th...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
the traditional stepwise refinement basedprogram derivation methodologies are primarily top-down. Strictly following the top-down program derivation approach may require backtracking resulting in rework. Moreover, the top down approach does not directly help in suggesting the next course of action in case of a failed derivation attempt. In this work we seamlessly incorporate a bottom up assumption propagation technique into a primarily top down derivation methodology. We present new tactics for back-propagating the assumptions made during the top-down phase. these tactics help in reducing the guesswork during the derivations. We have implemented these tactics in a program derivation system. Withthe help of simple examples, we show how this approach is useful for avoiding backtracking thereby simplifying the derivations.
Among other objectives, rewriting programs serves as a useful technique to improve numerical accuracy. However, this optimization is not intuitive and this is why we switch to automatic transformation techniques. We a...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
Among other objectives, rewriting programs serves as a useful technique to improve numerical accuracy. However, this optimization is not intuitive and this is why we switch to automatic transformation techniques. We are interested in the optimization of numerical programs relying on the IEEE754 floating-point arithmetic. In this article, our main contribution is to study the impact of optimizing the numerical accuracy of programs on the time required by numerical iterative methods to converge. To emphasize the usefulness of our tool, we make it optimize several examples of numerical methods such as Jacobi's method, Newton-Raphson's method, etc. We show that significant speedups are obtained in terms of number of iterations, time and flops.
In this paper, we suppose an agent which has a knowledge base represented by a logicprogram under the answer set semantics. We then consider the following two problems: given two programs P-1 and P-2, which have the ...
详细信息
ISBN:
(纸本)9783540714095
In this paper, we suppose an agent which has a knowledge base represented by a logicprogram under the answer set semantics. We then consider the following two problems: given two programs P-1 and P-2, which have the sets of answer sets AS(P-1) and AS(P-2), respectively;(i) find a program Q which has the answer sets as the minimal elements of {S boolean AND T vertical bar S is an element of AS(P-1) and T is an element of AS(P-2) };(ii) find a program R which has the answer sets as the maximal elements of the above set. A program Q satisfying (i) is called minimal consensus between P-1 and P-2;and R satisfying (ii) is called maximal consensus between P-1 and P-2. Minimal/maximal consensus extracts common beliefs that are included in an answer set of every program. Consensus provides a method of program development under a specification of constructing a programthat reflects the meaning of two or more programs. In application, it contributes to a theory of building consensus in multi-agent systems.
We present an extended framework for unfold/fold transformation of stratified logicprograms. We extend our previous transformation system which contains, among others, negative unfolding with a new application condit...
详细信息
ISBN:
(纸本)9783642205507
We present an extended framework for unfold/fold transformation of stratified logicprograms. We extend our previous transformation system which contains, among others, negative unfolding with a new application condition, by introducing extended negative unfolding. the application of extended negative unfolding allows an unfolding clause to have existential variables in its body, while conventional negative unfolding does not. Moreover, we complement our previous transformation system with another two transformation rules, simultaneous folding and negative folding. the correctness of the extended transformation system withthese three rules is shown in the sense of the perfect model semantics. We also examine the use of simultaneous folding for proving properties of programs in literature. We show by examples that our unfold/fold transformation system with extended negative unfolding, when used together with Lloyd-Topor transformation, can be used for verifying recursively defined properties of programs. the example illustrated in the paper shows that, although such properties are provable by using simultaneous folding, our inductive proof method can solve them in a simpler and more intuitive manner.
Co-logicprogramming is an extension of the conventional logicprogramming language, by allowing each predicate to be annotated as either inductive or coinductive. To define its procedural semantics as well as an alte...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
Co-logicprogramming is an extension of the conventional logicprogramming language, by allowing each predicate to be annotated as either inductive or coinductive. To define its procedural semantics as well as an alternating fixpoint semantics, the stratification restriction, a condition on predicate dependency in programs, has been imposed on co-logicprograms (co-LPs). In this paper, we first consider dual programs in co-logicprogramming: Given a program P, its dual program P* is a program such that it defines the "complement" of P, i.e., for any ground atom p((t) over bar), it computes its negation inverted left perpendiculatp((t) over bar). When we consider co-LPs with negation, we show that the stratification restriction becomes too restrictive in general, and that the Horn-calculus by Charatonik et al. can be used as an extension of co-logicprogramming for handling "non stratified" co-LPs. We then consider some applications of non-stratified co-LPs to Answer Set programming (ASP) and the well-founded semantics (WFS). In particular, we give new iterated fixpoint characterizations of answer sets as well as the WFS via dual programs. We also discuss some applications of non-stratified co-LPs to programtransformation such as partial deduction, and a proof procedure for the WFS.
暂无评论