A logic-based agent that plans for extended reachability goals

Planning to reach a goal is an essential capability for rational agents. In general, a goal specifies a condition to be achieved at the end of the plan execution. In this article, we introduce nondeterministic planning for extended reachability goals (i.e., goals that also specify a condition to be preserved during the plan execution). We show that, when this kind of goal is considered, the temporal logic CTL turns out to be inadequate to formalize plan synthesis and plan validation algorithms. This is mainly due to the fact that the CTL`s semantics cannot discern among the various actions that produce state transitions. To overcome this limitation, we propose a new temporal logic called alpha-CTL. Then, based on this new logic, we implement a planner capable of synthesizing reliable plans for extended reachability goals, as a side effect of model checking.

A pointcut-based coverage analysis approach for aspect-oriented programs

Aspect-oriented programming (AOP) is a promising technology that supports separation of crosscutting concerns (i.e., functionality that tends to be tangled with, and scattered through the rest of the system). In AOP, a method-like construct named advice is applied to join points in the system through a special construct named pointcut. This mechanism supports the modularization of crosscutting behavior; however, since the added interactions are not explicit in the source code, it is hard to ensure their correctness. To tackle this problem, this paper presents a rigorous coverage analysis approach to ensure exercising the logic of each advice - statements, branches, and def-use pairs - at each affected join point. To make this analysis possible, a structural model based on Java bytecode - called PointCut-based Del-Use Graph (PCDU) - is proposed, along with three integration testing criteria. Theoretical, empirical, and exploratory studies involving 12 aspect-oriented programs and several fault examples present evidence of the feasibility and effectiveness of the proposed approach. (C) 2010 Elsevier Inc. All rights reserved.

Disorder-based graphene spintronics

The use of the spin of the electron as the ultimate logic bit-in what has been dubbed spintronics-can lead to a novel way of thinking about information flow. At the same time single-layer graphene has been the subject of intense research due to its potential application in nanoscale electronics. While defects can significantly alter the electronic properties of nanoscopic systems, the lack of control can lead to seemingly deleterious effects arising from the random arrangement of such impurities. Here we demonstrate, using ab initio density functional theory and non-equilibrium Green`s functions calculations, that it is possible to obtain perfect spin selectivity in doped graphene nanoribbons to produce a perfect spin filter. We show that initially unpolarized electrons entering the system give rise to 100% polarization of the current due to random disorder. This effect is explained in terms of different localization lengths for each spin channel which leads to a new mechanism for the spin filtering effect that is disorder-driven.

Texture analysis based on maximum contrast walker

Recently, the deterministic tourist walk has emerged as a novel approach for texture analysis. This method employs a traveler visiting image pixels using a deterministic walk rule. Resulting trajectories provide clues about pixel interaction in the image that can be used for image classification and identification tasks. This paper proposes a new walk rule for the tourist which is based on contrast direction of a neighborhood. The yielded results using this approach are comparable with those from traditional texture analysis methods in the classification of a set of Brodatz textures and their rotated versions, thus confirming the potential of the method as a feasible texture analysis methodology. (C) 2010 Elsevier B.V. All rights reserved.

Analytic Methods for the Logic of Proofs

The logic of proofs (lp) was proposed as Gdels missed link between Intuitionistic and S4-proofs, but so far the tableau-based methods proposed for lp have not explored this closeness with S4 and contain rules whose analycity is not immediately evident. We study possible formulations of analytic tableau proof methods for lp that preserve the subformula property. Two sound and complete tableau decision methods of increasing degree of analycity are proposed, KELP and preKELP. The latter is particularly inspired on S4-proofs. The crucial role of proof constants in the structure of lp-proofs methods is analysed. In particular, a method for the abduction of proof constant specifications in strongly analytic preKELP proofs is presented; abduction heuristics and the complexity of the method are discussed.