To verify program specifications, rather than generic safety properties, it will be necessary to integrate verification into the process of programming. Program proving is unlike theorem proving in mathematics mathema...
详细信息
ISBN:
(纸本)9780769545066
To verify program specifications, rather than generic safety properties, it will be necessary to integrate verification into the process of programming. Program proving is unlike theorem proving in mathematics mathematical conjectures may give no hint as to how they could be proved, but programs are written by programmers, who must understand informally why their programs work. the job of verification is not to explore some immense search space, but to formalize the programmer's intuitions until any faults are revealed. this requires specifications and proofs that are succinct and intelligible which in turn require logics that go be yond predicate calculus (the assembly language of program proving). In this talk, I will recount and illustrate several steps, old and new, towards this goal - particularly in the treatment of arrays.
OSEK/VDX Operating System Specification is a standard in automotive industry with a long history. Dozens of mature industrial operating systems are based on this specification and widely applied in the products of maj...
详细信息
the proceedings contain 42 papers. the topics discussed include: causality, responsibility, and blame: a structural-model approach;fuzzy logic, annotation domains and semantic web languages;logicprogramming and uncer...
ISBN:
(纸本)9783642239625
the proceedings contain 42 papers. the topics discussed include: causality, responsibility, and blame: a structural-model approach;fuzzy logic, annotation domains and semantic web languages;logicprogramming and uncertainty;probabilistic logic networks in a nutshell;dynamics of beliefs;fuzzy classifiers: opportunities and challenges;a brief overview of research in argumentation systems;a brief overview of research in argumentation systems;argumentation frameworks as constraint satisfaction problems;on the equivalence of logic-based argumentation systems;bipolarity in argumentation graphs: towards a better understanding;handling enthymemes in time-limited persuasion dialogs;argumentation frameworks with necessities;a heuristics-based pruning technique for argumentation trees;on warranted inference in argument trees based framework;and uncertainty handling in quantitative BDD-based fault-tree analysis by interval computation.
In this paper, we introduce argumentation frameworks with necessities (AFNs), an extension of Dung's argumentation frameworks (AFs) taking into account a necessity relation as a kind of support relation between ar...
详细信息
ISBN:
(纸本)9783642239625;9783642239632
In this paper, we introduce argumentation frameworks with necessities (AFNs), an extension of Dung's argumentation frameworks (AFs) taking into account a necessity relation as a kind of support relation between arguments (an argument is necessary for another). We redefine the acceptability semantics for these extended frameworks and we show how the necessity relation allows a direct and easy correspondence between a fragment of logic programs (LPs) and AFNs. We introduce then a further generalization of AFNs that extends the necessity relation to deal with sets of arguments. We give a natural adaptation of the acceptability semantics to this new context and show that the generalized frameworks allow to encode arbitrary logic programs.
the aim of this paper is to offer an argumentation-based defeasible logicthat enables temporal forward reasoning. We extend the DeLP logical framework by associating temporal parameters to literals. A temporal logic ...
详细信息
ISBN:
(纸本)9783642239625;9783642239632
the aim of this paper is to offer an argumentation-based defeasible logicthat enables temporal forward reasoning. We extend the DeLP logical framework by associating temporal parameters to literals. A temporal logic program is a set of temporal literals and durative rules. these temporal facts and rules combine into durative arguments representing temporal processes, that permit us to reason defeasibly about future states. the corresponding notion of logical consequence, or warrant, is defined slightly different from that of DeLP, due to the temporal aspects. As usual, this notion takes care of inconsistencies, and in particular we prove the consistency of any logical program whose strict part is consistent. Finally, we define and study a sub-class of arguments that seem appropriate to reason with natural processes, and suggest a modification to the framework that is equivalent to restricting the logic to this class of arguments.
We present a probabilistic logicprogramming framework to reinforcement learning, by integrating reinforcement learning, in POMDP environments, with normal hybrid probabilistic logic programs with probabilistic answer...
详细信息
ISBN:
(纸本)9783642239625
We present a probabilistic logicprogramming framework to reinforcement learning, by integrating reinforcement learning, in POMDP environments, with normal hybrid probabilistic logic programs with probabilistic answer set semantics, that is capable of representing domain-specific knowledge. We formally prove the correctness of our approach. We show that the complexity of finding a policy for a reinforcement learning problem in our approach is NP-complete. In addition, we show that any reinforcement learning problem can be encoded as a classical logic program with answer set semantics. We also show that a reinforcement learning problem can be encoded as a SAT problem. We present a new high level action description language that allows the factored representation of POMDP. Moreover, we modify the original model of POMDP so that it be able to distinguish between knowledge producing actions and actions that change the environment.
Many-core parallel computing and programming is a new challenge for formal specification and verification. this paper presents a semantic model for many-core parallel computing systems so that the systems can be model...
详细信息
ISBN:
(纸本)9783642226151
Many-core parallel computing and programming is a new challenge for formal specification and verification. this paper presents a semantic model for many-core parallel computing systems so that the systems can be modeled and verified in a manageable way. the model is called Cylinder Computation Model (CCM) which is based on projection constructs in Projection Temporal logic (PTL) and Modeling, Simulation and Verification Language (MSVL). To this end, the syntax and semantics of CCM are presented in details. Further, some logic laws regarding CCM are given and the normal form of CCM programs is formalized and proved. Moreover, the operational semantics of CCM and an algorithm for implementing CCM programs with MSVL are also formalized. Finally, an example, simple word processor, is given to show how CCM works under MSVL paradigm.
Automatic understanding of GUI (Graphic User Interfaces) is vitally important for applications such as quality assurance, user monitoring, speech activated devices, automatic generation of GUI for application accessib...
详细信息
ISBN:
(纸本)9780769544922
Automatic understanding of GUI (Graphic User Interfaces) is vitally important for applications such as quality assurance, user monitoring, speech activated devices, automatic generation of GUI for application accessibility, and GUI design. Likewise, automatic understanding of visually structured documents (e.g. PDF files) is vitally important for data mining purposes. Current GUI parsers share two major shortcomings: First, instead of representing the user experience, they are tightly coupled to the underlying object model of the GUI. Second, from a linguistic point of view, they are either too restrictive to describe enough GUIs, or too permissive, in which case, the language structure itself becomes very fragile. We designed and implemented a new GUI parsing language which avoids these problems. It is easy to maintain, robust to changes in the input, and finally - as a computer program - decidable and fast to parse.
In recent papers [13,14,15], we demonstrated a methodology for developing correct-by-design programs from temporal logic specification using genetic programming. Model checking the temporal specification is used to ca...
详细信息
ISBN:
(纸本)9783642192364
In recent papers [13,14,15], we demonstrated a methodology for developing correct-by-design programs from temporal logic specification using genetic programming. Model checking the temporal specification is used to calculate the fitness function for candidate solutions, which directs the search from initial randomly generated programs towards correct solutions. this method was successfully demonstrated by constructing solutions for the mutual exclusion problem;later, we also imposed some realistic constraints on access to variables. While the results were encouraging for using the genetic synthesis method, the mutual exclusion example includes some limitations that;fit well withthe constraints of model checking: the goal was finding a fixed finite state program, and its state space was moderately small. Here, in a more realistic setting, we challenge the problem of synthesizing a solution for the well known "leader election" problem;under this problem, a circular, unidirectional network with message passing is seeking the identity of a process with a maximal value. this identity, once found, can be used for synchronization, breaking symmetry and other network applications. the problem is challenging since it is parametric, and the state space of the solutions grows up exponentially withthe number of processes.
the deployment of knowledge representation formalisms to the Web has created the need for hybrid formalisms that combine heterogeneous knowledge bases. the aim of this research is to improve the reasoning efficiency o...
详细信息
暂无评论