Encapsulated abstractions are fundamental in object-oriented programming. A single class may employ multiple abstractions to achieve its purpose. Such abstractions are often related and combined in disciplined ways. T...
详细信息
ISBN:
(纸本)9781450302036
Encapsulated abstractions are fundamental in object-oriented programming. A single class may employ multiple abstractions to achieve its purpose. Such abstractions are often related and combined in disciplined ways. this paper explores ways to express, verify and rely on logical relationships between abstractions. It introduces two general specification mechanisms: export clauses for relating abstractions in individual classes, and axiom clauses for relating abstractions in a class and all its descendants. MultiStar, an automatic verification tool based on separation logic and abstract predicate families, implements these mechanisms in a multiple inheritance setting. Several verified examples illustrate MultiStar's underlying logic. To demonstrate the flexibility of our approach, we also used MultiStar to verify the core iterator hierarchy of a popular data structure library.
We study strategy improvement algorithms for mean-payoff and parity games. We describe a structural property of these games, and we show that these structures can affect the behaviour of strategy improvement. We show ...
详细信息
ISBN:
(纸本)9783642175107
We study strategy improvement algorithms for mean-payoff and parity games. We describe a structural property of these games, and we show that these structures can affect the behaviour of strategy improvement. We show how awareness of these structures can be used to accelerate strategy improvement algorithms. We call our algorithms non-oblivious because they remember properties of the game that they have discovered in previous iterations. We show that non-oblivious strategy improvement algorithms perform well on examples that are known to be hard for oblivious strategy improvement. Hence, we argue that previous strategy improvement algorithms fail because they ignore the structural properties of the game that they are solving.
Because of their self-x properties Organic Computing systems are hard to verify. Nevertheless in safety critical domains one may want to give behavioral guarantees. One technique to reduce complexity of the overall ve...
详细信息
ISBN:
(纸本)9783642165757
Because of their self-x properties Organic Computing systems are hard to verify. Nevertheless in safety critical domains one may want to give behavioral guarantees. One technique to reduce complexity of the overall verification task is applying composition theorem. In this paper we present a technique for formal specification and compositional verification of Organic Computing systems. Separation of self-x and functional behavior has amongst others, advantages for the formal specification. We present how the specification of self-x behavior can be integrated into an approach for compositional verification of concurrent systems, based on Interval Temporal logic. the presented approach has full tool support withthe KIV interactive theorem prover.
Jerabek showed in 2008 that cuts in propositional-logic deep-inference proofs can be eliminated in quasipolynomial time. the proof is an indirect one relying on a result of Atserias, Galesi and Pudlak about monotone s...
详细信息
ISBN:
(纸本)9783642175107
Jerabek showed in 2008 that cuts in propositional-logic deep-inference proofs can be eliminated in quasipolynomial time. the proof is an indirect one relying on a result of Atserias, Galesi and Pudlak about monotone sequent calculus and a correspondence between this system and cut-free deep-inference proofs. In this paper we give a direct proof of Jerabek's result: we give a quasipolynomial-time cut-elimination procedure in propositional-logic deep inference. the main new ingredient is the use of a computational trace of deep-inference proofs called atomic flows, which are both very simple (they trace only structural rules and forget logical rules) and strong enough to faithfully represent the cut-elimination procedure.
Probabilistic conditionals are a powerful means for expressing uncertain knowledge. In this paper, we describe a system implemented in Java performing probabilistic reasoning at optimum entropy. It provides nonmonoton...
详细信息
ISBN:
(纸本)9783642042379
Probabilistic conditionals are a powerful means for expressing uncertain knowledge. In this paper, we describe a system implemented in Java performing probabilistic reasoning at optimum entropy. It provides nonmonotonic belief change operations like revision and up-date and supports advanced querying facilities including diagnosis and what-if-analysis.
We summarize the salient features of the current version of the answer set solver clasp, focusing oil the progress made since version RC4 of clasp. Apart from enhanced preprocessing and search-supporting techniques, a...
详细信息
ISBN:
(纸本)9783642042379
We summarize the salient features of the current version of the answer set solver clasp, focusing oil the progress made since version RC4 of clasp. Apart from enhanced preprocessing and search-supporting techniques, a particular emphasis lies on advanced reasoning modes, Such as cautious and brave reasoning, optimization, solution projection, and incremental solving.
this note summarizes the use of Answer Set programming to solve various computational problems to inter phylogenetic trees and phylogenetic networks, and discusses its applicability and effectiveness on some real taxa.
ISBN:
(纸本)9783642042379
this note summarizes the use of Answer Set programming to solve various computational problems to inter phylogenetic trees and phylogenetic networks, and discusses its applicability and effectiveness on some real taxa.
Belief logicprogramming (BLP) is a novel form of quantitative logicprogramming in the presence of uncertain and inconsistent, information, which was designed to be able to combine and correlate evidence obtained fro...
详细信息
ISBN:
(纸本)9783642042379
Belief logicprogramming (BLP) is a novel form of quantitative logicprogramming in the presence of uncertain and inconsistent, information, which was designed to be able to combine and correlate evidence obtained from non-independent information sources. BLP has non-monotonic semantics based on the concepts of belief combination functions and is inspired by Dempster-Shafer theory of evidence. Most importantly, unlike the previous efforts to integrate uncertainty and logicprogramming, BLP can correlate structural information contained in rules and provides more accurate certainty estimates. the results are illustrated via simple, yet, realistic examples of rule-based Web service integration.
this paper reports oil the Second Answer Set programming Competition. the competitions in areas of Satisfiability checking, Pseudo-Boolean constraint solving and Quantified Boolean Formula evaluation have proven to be...
详细信息
ISBN:
(纸本)9783642042379
this paper reports oil the Second Answer Set programming Competition. the competitions in areas of Satisfiability checking, Pseudo-Boolean constraint solving and Quantified Boolean Formula evaluation have proven to be a strong driving force for a community to develop better performing systems. Following this experience, the Answer Set programming competition series was set up in 2007, and ran as part of the internationalconference oil logicprogramming and nonmonotonicreasoning (LPNMR). this second competition, held in conjunction with LPNMR 2009, differed from the first one in two important ways. First, while the original competition was restricted to systems designed for the answer set programming language, the sequel was open to systems designed for other modeling languages, as well. Consequently, among the contestants of the second competition were a CLP(FD) team and three model generation systems for (extensions of) classical logic. Second, this latest competition covered not only satisfiability problems but also optimization ones. We present and discuss the set-up and the results of the competition.
暂无评论