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.
this study presents a penalized probabilistic First-Order Inductive Learning (pFOIL) approach to error diagnosis for Chinese as a Second Language (CSL) learners. the pFOIL approach is first proposed to characterize a ...
详细信息
this study presents a penalized probabilistic First-Order Inductive Learning (pFOIL) approach to error diagnosis for Chinese as a Second Language (CSL) learners. the pFOIL approach is first proposed to characterize a sentence using multi-type background knowledge which contains the morphological, syntactic and semantic relations among the words in a sentence and quantized background knowledge with discrete values of multi-type relations. Afterwards, a decomposition-based testing mechanism which decomposes a sentence into the background knowledge regarding each error type is proposed to infer all potential error types and causes of the sentence. Withthe proposed pFOIL method, not only the error type but also the error cause and word position can be provided to the CSL learners. Experiment results reveal that the proposed pFOIL method outperforms the C4.5, maximum entropy and Naïve Bayes classifiers in error classification.
this paper describes basic features of a client library called Persistence API that provides access point to knowledge repositories based on RDF standard. Persistence API (P-API) has been implemented within FP6 IST pr...
详细信息
ISBN:
(纸本)9781424438013
this paper describes basic features of a client library called Persistence API that provides access point to knowledge repositories based on RDF standard. Persistence API (P-API) has been implemented within FP6 IST project called Knowledge Practices Laboratory in order to separate business logic from data representation in RDF. this approach enables simple integration and communication between end-user applications and knowledge repository. the development of P-API is still ongoing, with new features such as support for Search services implemented in recent releases.
We discuss a new concept of agent programs that combines logicprogramming with reasoning about actions. these agent logic programs are characterized by a clear separation between the specification of the agent's ...
详细信息
ISBN:
(纸本)9783642042218
We discuss a new concept of agent programs that combines logicprogramming with reasoning about actions. these agent logic programs are characterized by a clear separation between the specification of the agent's strategic behavior and the underlying theory about the agent's actions and their effects. this makes it a generic, declarative agent programming language, which can be combined with an action representation formalism of one's choice. We present a declarative semantics for agent logic programs along with (two versions of) a sound and complete operational semantics, which combines the standard inference mechanisms for (constraint) logic programs with reasoning about actions.
We give a case study for a Satisfiability Modulo theories (SMT) solver usage in functional verification of a real world operating system. In particular, we present a view of the E-matching pattern annotations on quant...
详细信息
ISBN:
(纸本)9781605584843
We give a case study for a Satisfiability Modulo theories (SMT) solver usage in functional verification of a real world operating system. In particular, we present a view of the E-matching pattern annotations on quantified formulas as a kind of logicprogramming language, used to encode semantics of the programming language undergoing verification. We postulate a few encoding patterns to be benchmark problems for a possible E-matching alternative. We also describe features required from the SMT solver in deductive software verification scenarios. Copyright 2009 ACM.
the paper proposes a novel solution to the problem of exceptional scope (ES) of (in)definites, exemplified by the widest and intermediate scope readings of the sentence Every student of mine read every poem that a fam...
详细信息
ISBN:
(纸本)9783642006647
the paper proposes a novel solution to the problem of exceptional scope (ES) of (in)definites, exemplified by the widest and intermediate scope readings of the sentence Every student of mine read every poem that a famous Romanian poet wrote. We propose that the ES readings have two sources: (i) discourse anaphora to particular sets of entities and quantificational dependencies between these entities that restrict the domain of quantification of the two universal determiners and the indefinite article;(ii) non-local accommodation of the discourse referent that restricts the quantificational domain of the indefinite article. Our account, formulated within a compositional dynamic system couched in classical type logic, relies on two independently motivated assumptions: (a) the discourse context stores not only (sets of) individuals, but also quantificational dependencies between them, and (b) quantifier domains are always contextually restricted. Under this analysis, (in)definites are unambiguous and there is no need for special choice-functional variables to derive exceptional scope readings.
functional and non-functional concerns require different programming effort, different techniques and different methodologies when attempting to program efficient parallel/distributed applications. In this work we pre...
详细信息
ISBN:
(纸本)9783642041662
functional and non-functional concerns require different programming effort, different techniques and different methodologies when attempting to program efficient parallel/distributed applications. In this work we present a "programmer oriented" methodology based on formal tools that permits reasoning about parallel/distributed program development and refinement. the proposed methodology is semi-formal in that it does not require the exploitation of highly formal tools and techniques, while providing a palatable and effective support to programmers developing parallel/distributed applications, in particular when handling non-functional concerns.
the proceedings contain 23 papers. the topics discussed include: building SMT-based software model checkers: an experience report;combining nonmonotonic knowledge bases with external sources;combining description logi...
ISBN:
(纸本)364204221X
the proceedings contain 23 papers. the topics discussed include: building SMT-based software model checkers: an experience report;combining nonmonotonic knowledge bases with external sources;combining description logics, description graphs, and rules;unification modulo homomorphic encryption;argument filterings and usable rules for simply typed dependency pairs;DL-Lite with temporalised concepts, rigid axioms and roles;axiomatization and completeness of lexicographic products of modal logics;taming the complexity of temporal epistemic reasoning;a declarative agent programming language based on action theories;combinations of theories for decidable fragments of first-order logic;improving coq propositional reasoning using a lazy CNF conversion scheme;efficient combination of decision procedures for MUS computation;and learning to integrate deduction and search in reasoning about quantified Boolean formulas.
We describe a new method to induce functional programs from small sets of non-recursive equations representing a subset of their input-output behaviour. Classical attempts to construct functional Lisp programs from in...
详细信息
ISBN:
(纸本)9783642005145
We describe a new method to induce functional programs from small sets of non-recursive equations representing a subset of their input-output behaviour. Classical attempts to construct functional Lisp programs from input/output-examples are analytical, i.e., a Lisp program belonging to a strongly restricted program class is algorithmically derived from examples. More recent approaches enumerate candidate programs and only test them against the examples until a program which correctly computes the examples is found. theoretically, large program classes can be induced generate-and-test based, yet this approach suffers from combinatorial explosion. We propose a combination of search and analytical techniques. the method described in this paper is search based in order to avoid strong a-priori restrictions as imposed by the classical analytical approach. Yet candidate programs are computed based on analytical techniques from the examples instead of being generated independently from the examples. A prototypical implementation shows first that programs are inducible which are not in scope of classical purely analytical techniques and second that the induction times are shorter than in recent generate-and-test based methods.
暂无评论