this extended abstract provides an overview of my research towards a dissertation thesis in the context of programming cognitive agents with non-monotonic reasoning capabilities.
this extended abstract provides an overview of my research towards a dissertation thesis in the context of programming cognitive agents with non-monotonic reasoning capabilities.
Formal methods can in principle provide the highest levels of assurance of code safety by providing formal proofs as explicit evidence for the assurance claims. However, the proof, are often complex and difficult to r...
详细信息
ISBN:
(纸本)9783540876977
Formal methods can in principle provide the highest levels of assurance of code safety by providing formal proofs as explicit evidence for the assurance claims. However, the proof, are often complex and difficult to relate to the code, in particular if it has been generated automatically. they may also be based on assumptions and reasoning principles that are not Justified. this causes concerns about the trustworthiness of the proofs and thus the assurance claims. Here we present an approach to systematically construct safety cases from information collected during a formal verification of the code, in particular from the construction of the logical annotations necessary for a formal, Hoare-style safety certification. Our approach combines a generic argument that is instantiated with respect to the certified safety property (i.e., safety claims) with a detailed, program-specific argument that can be derived systematically because its structure directly follows the Course the annotation construction takes through the code. the resulting safety cases make explicit the formal and informal reasoning principles, and reveal the top-level assumptions and external dependencies that must be taken into account. However, the evidence still comes from the formal safety proofs. Our approach is independent of the given safety property and program, and consequently also independent of the underlying code generator. Here, we illustrate it for the AutoFilter system developed at NASA Ames.
Rules are the basis of decision-making in the combat simulation execution. In event driven mode, when a certain event occurs, many rules are chosen and bring in different results in combat simulation process. Analyses...
详细信息
Rules are the basis of decision-making in the combat simulation execution. In event driven mode, when a certain event occurs, many rules are chosen and bring in different results in combat simulation process. Analyses the representation and execution of production rules, studies the rule priority based reasoning, defines two kinds of rule priority, default priority and user defined priority. It presents a method of sifting of multiple rules priority and designed system architecture and military rules database.
Based on analyzing of the common activity and content of modeling, this paper concluded the common essence and rules of modeling in every domain, and established the architecture of modeling theory in Simulation Scien...
详细信息
Based on analyzing of the common activity and content of modeling, this paper concluded the common essence and rules of modeling in every domain, and established the architecture of modeling theory in Simulation Science & Technology (SS&T), which is formed by general theory of model, model construction theory and modeling methodology. Moreover, the concept of model, the common characteristics and theories about common questions of model were set forth; all existing model construct theories were summed-up and their function and character was differentiated; according to modeling process, most existing modeling methods were regularized withtheir function and their relations between each other. All these made modeling theory more clearly.
A spatial computer is a distributed multi-agent system that is embedded in a geometric space. A key challenge is engineering local agent interaction rules that enable spatial computers to robustly achieve global compu...
ISBN:
(纸本)9780981738116
A spatial computer is a distributed multi-agent system that is embedded in a geometric space. A key challenge is engineering local agent interaction rules that enable spatial computers to robustly achieve global computational tasks. this paper develops a principled approach to global-to-local programming, for pattern formation problems in a one-dimensional multi-agent model. We present theoretical analysis that addresses the existence, construction, and resource tradeoffs of robust local rule solutions to global patterns, and which together form a "global-to-local compiler".
Systematics is a specification language designed for automatic code generation. Systematics uniquely provides auto-provability by virtue of the inclusion of ldquosystem timerdquo as an inherent characteristic of infor...
详细信息
Systematics is a specification language designed for automatic code generation. Systematics uniquely provides auto-provability by virtue of the inclusion of ldquosystem timerdquo as an inherent characteristic of information. A code generator based on Systematics is described which, unlike other code generators, requires no computing expertise on the part of the user, and is not limited to any specific type of generated application. the generator stores the specification in tabular form, in terms of 8 basic concepts. the generated system includes a pre-written ldquoauto-navigationrdquo function which is called to produce outputs on receipt of stimuli. the Systematics generator has initially been implemented in Microsoft Access to provide ldquoProof of Principlerdquo. A generic version of the Systematics Generator is currently being developed by the Systematics Research Group. this version will be independent of any proprietary database product, but withthe ability to ldquofront-endrdquo any such product, and will also allow automatic optimisation of the database.
Composable simulation is powerful in developing modeling and simulation system that is capable to assemble component models agilely and to construct simulation application rapidly on demands. To meet the requirements ...
详细信息
Composable simulation is powerful in developing modeling and simulation system that is capable to assemble component models agilely and to construct simulation application rapidly on demands. To meet the requirements of composability, reusability, and interoperability, composable simulation model can be defined and described on the conceptual, pragmatic, semantic, syntactic, and technical level respectively. With explicitly, strictly, and completely defined model structure, a multilevel model specification proposed in this paper can make a steady support to describe simulation components on different levels and to analyze composability of simulation models. Five minutely discussed patterns of model composition can express the assembling mechanisms of composable components of system. the thoroughly defined concepts of compatibility and substitutability present an effective approach to qualify and calculate the degree of composability of system model. Based on all above mentioned researches, a multilevel conceptual framework of composable simulation is formed completely and meaningfully.
In this paper we propose an explicit form of knowledge-based programming. Our initial motivation is the distributed implementation of game-theoretical algorithms, but we abstract away from the game-theoretical details...
详细信息
ISBN:
(纸本)9780981738123
In this paper we propose an explicit form of knowledge-based programming. Our initial motivation is the distributed implementation of game-theoretical algorithms, but we abstract away from the game-theoretical details and describe a general scenario, where a group of agents each have some initially private bits of information which they can then communicate to each other. We draw on existing literature to give a formal model using modal logic to represent the knowledge of the agents as well as how that knowledge changes as they communicate. We sketch an implementation which enables processes in a distributed system to explicitly evaluate knowledge formulae. then we prove that the implementation captures the formal model, and therefore correctly reflects the general scenario. Finally we look at how our approach lends itself to generalisations, and discuss application perspectives.
Intelligent agents designed to work in complex, dynamic environments must respond robustly and flexibly to environmental and circumstantial changes. An agent must be capable of deliberating about appropriate courses o...
详细信息
ISBN:
(纸本)9780981738109
Intelligent agents designed to work in complex, dynamic environments must respond robustly and flexibly to environmental and circumstantial changes. An agent must be capable of deliberating about appropriate courses of action, which may include reprioritising goals, aborting particular tasks, or scheduling tasks in a particular order. this paper investigates the incorporation of a mechanism to suspend and reconsider tasks within a BDI-style architecture. Such an ability provides an agent designer greater flexibility to direct agent operation, and it offers a generic means for handling conflicts between tasks. We investigate conditions under which a goal or a plan may be suspended, the process for suspending it, and the appropriate behaviours upon resumption. We give an operational semantics for suspending tasks in terms of the abstract agent language CAN, thus providing a general mechanism that can be incorporated into any BDI-based agent programming language.
In the last few years, argumentation frameworks have been successfully applied to multi agent systems. Recently, argumentation has been used to provide a framework for reasoning about coalition formation. At the same ...
详细信息
ISBN:
(纸本)9780981738116
In the last few years, argumentation frameworks have been successfully applied to multi agent systems. Recently, argumentation has been used to provide a framework for reasoning about coalition formation. At the same time alternating-time temporal logic has been used to reason about the behavior and abilities of coalitions of agents. However, ATL operators account only for the existence of successful strategies of coalitions. they do not consider whether coalitions can be actually *** paper is an attempt to combine both frameworks and to develop a logicthrough which we can reason at the same time (1) about abilities of coalitions of agents and (2) about the formation of coalitions. We provide a formal extension of ATL, ATLc, in which the actual computation of the coalition is modelled in terms of argumentation semantics. We show that ATLc's proof theory can be understood as a natural extension of the model checking procedure used in ATL.
暂无评论