the proceedings contain 9 papers. the topics discussed include: fundamentals of concern manipulation;requirement enforcement by transformation automata;typing for a minimal aspect language: preliminary report;towards ...
详细信息
the proceedings contain 9 papers. the topics discussed include: fundamentals of concern manipulation;requirement enforcement by transformation automata;typing for a minimal aspect language: preliminary report;towards a type system for detecting never-matching pointcut compositions;on the relation of aspects and monads;on bytecode slicing and aspectJ interferences;specializing continuations a model for dynamic join points;and aspects and modular reasoning in nonmonotoniclogic;and aspect-oriented programming with type classes.
logicprogramming under the answer-set semantics nowadays deals with numerous different notions of equivalence between programs. this is due to the fact that equivalence for substitution (known as strong equivalence),...
详细信息
logicprogramming under the answer-set semantics nowadays deals with numerous different notions of equivalence between programs. this is due to the fact that equivalence for substitution (known as strong equivalence), which holds between programs P and Q iff P can faithfully be replaced by Q within any context R, is a different concept than ordinary equivalence between P and Q, which holds if P and Q have the same answer sets. Notions inbetween strong and ordinary equivalence have therefore been obtained by either restricting the syntactic structure of R or bounding the set of atoms allowed to occur in R (relativized equivalence). For the former approach, however, it turned out that any "reasonable" syntactic restriction to R either coincides with strong equivalence or collapses to uniform equivalence where R ranges over arbitrary sets of facts. In this paper, we propose a parameterization for equivalence notions which takes care of both such kinds of restrictions simultaneously by bounding, on the one hand, the atoms which are allowed to occur in the rule heads of R and, on the other hand, the atoms which are allowed to occur in the rule bodies of R. We introduce a semantical characterization including known ones as SE-models or UE-models as special cases. Moreover, we provide complexity bounds for the problem in question.
LODE is a logic-based web tool for Italian deaf children. It aims at stimulating global reasoning on e-stories written in a verbal language. Presently, we are focusing on temporal reasoning, that is, LODE stimulates c...
详细信息
ISBN:
(纸本)9783540749691
LODE is a logic-based web tool for Italian deaf children. It aims at stimulating global reasoning on e-stories written in a verbal language. Presently, we are focusing on temporal reasoning, that is, LODE stimulates children to reason with global temporal relations between events possibly distant in a story. this is done through apt exercises and withthe support of a constraint programming system. Children can also reinvent the e-story by rearranging its events along a new temporal order;it is the task of the constraint system to determine the consistency of the temporally reorganised story and provide children with feedback. To the best of our knowledge, LODE is the first e-learning tool for Italian deaf children that aims at stimulating global reasoning on whole e-stories.
the structural semantics of UML-based metamodeling were recently explored[l], providing a characterization of the models adhering to a metamodel. In particular, metamodels can be converted to a set of constraints expr...
详细信息
ISBN:
(纸本)9783540752080
the structural semantics of UML-based metamodeling were recently explored[l], providing a characterization of the models adhering to a metamodel. In particular, metamodels can be converted to a set of constraints expressed in a decidable subset of first-order logic, an extended Horn logic. We augment the constructive techniques found in logicprogramming, which are also based on an extended Horn logic, to produce constructive techniques for reasoning about models and metamodels. these methods have a number of practical applications: At the meta-level, it can be decided if a (composite) metamodel characterizes a non-empty set of models, and a member can be automatically constructed. At the model-level, it can be decided if a submodel has an embedding in a well-formed model, and the larger model can be constructed. this amounts to automatic model construction from an incomplete model. We describe the concrete algorithms for constructively solving these problems, and provide concrete examples.
Model checking is a technique for verifying that a finite-state concurrent system is correct with respect to its specification. In bounded model checking (BMC), the system is unfolded until a given depth, and translat...
详细信息
ISBN:
(纸本)9783540730989
Model checking is a technique for verifying that a finite-state concurrent system is correct with respect to its specification. In bounded model checking (BMC), the system is unfolded until a given depth, and translated into a CNF formula. A SAT solver is then applied to the CNF formula, to find a satisfying assignment. Such a satisfying assignment, if found, demonstrates an error in the model of the concurrent system. Description logic (DL) is a family of knowledge representation formalisms, for which reasoning is based on tableaux techniques. We show how Description logic can serve as a natural setting for representing and solving a BMC problem. We formulate a bounded model checking problem as a consistency problem in the DL dialect ACCI. Our formulation results in a compact representation of the model, one that is linear in the size of the model description, and does not involve any unfolding of the model. Experimental results, using the DL reasoner FaCT(++), significantly improve on a previous approach that used DL reasoning for model checking.
An important open question in the semantic Web is the precise relationship between the RDF(S) semantics and the semantics of standard knowledge representation formalisms such as logicprogramming and description logic...
详细信息
ISBN:
(纸本)9783540762973
An important open question in the semantic Web is the precise relationship between the RDF(S) semantics and the semantics of standard knowledge representation formalisms such as logicprogramming and description logics. In this paper we address this issue by considering embeddings of RDF and RDFS in logic. Using these embeddings, combined with existing results about various fragments of logic, we establish several novel complexity results. the embeddings we consider show how techniques from deductive databases and description logics can be used for reasoning with RDF(S). Finally, we consider querying RDF graphs and establish the data complexity of conjunctive querying for the various RDF entailment regimes.
Probabilistic logic Learning (PLL) aims at learning probabilistic logical frameworks on the basis of data. Such frameworks combine expressive knowledge representation formalisms withreasoning mechanisms grounded in p...
详细信息
ISBN:
(纸本)9783540738466
Probabilistic logic Learning (PLL) aims at learning probabilistic logical frameworks on the basis of data. Such frameworks combine expressive knowledge representation formalisms withreasoning mechanisms grounded in probability theory. Numerous frameworks have already addressed this issue. therefore, there is a real need to compare these frameworks in order to be able to unify them. this paper provides a comparison of Relational Markov Models (RMMs) and Bayesian logic Programs (BLPs). We demonstrate relations between BLPs' and RMMs' semantics, arguing that RMMs encode the same knowledge as a sub-class of BLPs. We fully describe a translation from a sub-class of BLPs into RMMs and provide complexity results which demonstrate an exponential expansion in formula size, showing that RMMs are less compact than their equivalent BLPs with respect to this translation. the authors are unaware of any more compact translation between BLPs and RMMs. A full implementation has already been realized, consisting of meta-interpreters for both BLPs and RMMs and a translation engine. the equality of BLPs' and corresponding RMMs' probability distributions has been proven on practical examples.
the need for a more autonomous management of distributed systems and networks has driven research and industry to look for management frameworks that go beyond the direct manipulation of network devices and systems. O...
详细信息
ISBN:
(纸本)9783540721994
the need for a more autonomous management of distributed systems and networks has driven research and industry to look for management frameworks that go beyond the direct manipulation of network devices and systems. One approach towards this aim is to build policy-based management systems. Policy-based computing refers to a software paradigm developed around the concept of building autonomous systems that provide system administrators and decision makers with interfaces that let them set general guiding principles and policies to govern the behavior and interactions of the managed systems. Although many of the tasks are still carried out manually and ad hoc, instances of limited policy-based systems can be found in areas such as Internet service management, privacy, security and access management, management of quality of service and service level agreements in networks. Policies can be specified at many levels of abstraction, from natural language specifications to more elementary condition-action rule specifications. From these specifications policy systems need to come up with implementations. Some of these implementations can be done automatically, others require manual steps. In some cases policies impose legal commitments and systems should be able to demonstrate compliance. there are also situations in which policies are in conflict with each other and a system cannot implement them simultaneously without providing methods for conflict resolution. In this presentation I will review a few policy systems, applications and specification languages. then I will provide a more formal characterization of policies and their computational model. I will show a simple policy language in the style of the action description language A. I will discuss current solutions to policy conflicts, discuss the problem of policy refinement, i.e. transformations from high level specifications to lower level specifications, current approaches to refinement and provide a partial formal
Modelling is becoming a necessity in studying biological signalling pathways, because the combinatorial complexity of such systems rapidly overwhelms intuitive and qualitative forms of reasoning. Yet, this same combin...
详细信息
ISBN:
(纸本)9783540744061
Modelling is becoming a necessity in studying biological signalling pathways, because the combinatorial complexity of such systems rapidly overwhelms intuitive and qualitative forms of reasoning. Yet, this same combinatorial explosion makes the traditional modelling paradigm based on systems of differential equations impractical. In contrast, agent-based or concurrent languages, such as kappa. [1,2,3] or the closely related BioNetGen language [4,5,6,7,8,9,10], describe biological interactions in terms of rules, thereby avoiding the combinatorial explosion besetting differential equations. Rules are expressed in an intuitive graphical form that transparently represents biological knowledge. In this way, rules become a natural unit of model building, modification, and discussion. We illustrate this with a sizeable example obtained from refactoring two models of EGF receptor signalling that are based on differential equations [11,12]. An exciting aspect of the agent-based approach is that it naturally lends itself to the identification and analysis of the causal structures that deeply shape the dynamical, and perhaps even evolutionary, characteristics of complex distributed biological systems. In particular, one can adapt the notions of causality and conflict, familiar from con-currency theory, to kappa, our representation language of choice. Using the EGF receptor model as an example, we show how causality enables the formalization of the colloquial concept of pathway and, perhaps more surprisingly, how conflict can be used to dissect the signalling dynamics to obtain a qualitative handle on the range of system behaviours. By taming the combinatorial explosion, and exposing the causal structures and key kinetic junctures in a model, agent- and rule-based representations hold promise for making modelling more powerful, more perspicuous, and of appeal to a wider audience.
State of the art analyzers in the logicprogramming (LP) paradigm are nowadays mature and sophisticated. they allow inferring a wide variety of global properties including termination, bounds on resource consumption, ...
ISBN:
(纸本)9783540696087
State of the art analyzers in the logicprogramming (LP) paradigm are nowadays mature and sophisticated. they allow inferring a wide variety of global properties including termination, bounds on resource consumption, etc. the aim of this work is to automatically transfer the power of such analysis tools for LP to the analysis and verification of Java bytecode (jvml). In order to achieve our goal, we rely on well-known techniques for meta-programming and program specialization. More precisely, we propose to partially evaluate a jvml interpreter implemented in LP together with (an LP representation of) a jvml program and then analyze the residual program. Interestingly, at least for the examples we have studied, our approach produces very simple LP representations of the original jvml programs. this can be seen as a decompilation from jvml to high-level LP source. By reasoning about such residual programs, we can automatically prove in the CiaoPP system some non-trivial properties of jvml programs such as termination, run-time error freeness and infer bounds on its resource consumption. We are not aware of any other system which is able to verify such advanced properties of Java bytecode.
暂无评论