Reasoning about actions with loops via Hoare logic

Plans with loops are more general and compact than classical sequential plans, and gaining increasing atten- tions in artificial intelligence （AI）. While many existing ap- proaches mainly focus on algorithmic issues, few work has been devoted to the semantic foundations on planning with loops. In this paper, we first develop a tailored action lan- guage , together with two semantics for handling do- mains with non-deterministic actions and loops. Then we propose a sound and （relative） complete Hoare-style proof system for efficient plan generation and verification under O- approximation semantics, which uses the so-called idea off- line planning and on-line querying strategy in knowledge compilation, i.e., the agent could generate and store short proofs as many as possible in the spare time, and then per- form quick query by constructing a long proof from the stored shorter proofs using compositional rule. We argue that both our semantics and proof system could serve as logical foun- dations for reasoning about actions with loops.

The M-computations induced by accessibility relations in nonstandard models M of Hoare logic

Hoare logic is a logic used as a way of specifying semantics of programming languages, which has been extended to be a separation logic to reason about mutable heap structure. In a model M of Hoare logic, each program α induces an M-computable function fα M on the universe of M; and the M-recursive functions are defined on M. It will be proved that the class of all the M-computable functions fα M induced by programs is equal to the class of all the M- recursive functions. Moreover, each M-recursive function is ∑ 1 NM -definable in M, where the universal quantifier is a num- ber quantifier ranging over the standard part of a nonstandard model M.

Extending Hoare Logic with an Infinite While-Rule

In this paper we generalize the while-rule in Hoare calculus to an infinite one and then present a sufficient condition much weaker than the expressiveness for Cook's relative completeness theorem with respect to our new axiomatic system. Using the extended Hoare calculus we can derive true Hoare formulas which contain while- statements free of loop invariants. It is also pointed out that the weak condition is a first order property and therefore provides a possible approach to the characterization of relative completeness which is also a first-order property.

A measurable refinement method of design and verification for micro-kernel operating systems in communication network

A secure operating system in the communication network can provide the stable working environment,which ensures that the user information is not stolen.The micro-kernel operating system in the communication network retains the core functions in the kernel,and unnecessary tasks are implemented by calling external processes.Due to the small amount of code,the micro-kernel architecture has high reliability and scalability.Taking the microkernel operating system in the communication network prototype VSOS as an example,we employ the objdump tool to disassemble the system source code and get the assembly layer code.On this basis,we apply the Isabelle/HOL,a formal verification tool,to model the system prototype.By referring to the mathematical model of finite automata and taking the process scheduling module as an example,the security verification based on the assembly language layer is developed.Based on the Hoare logic theory,each assembly statement of the module is verified in turn.The verification results show that the scheduling module of VSOS has good functional security,and also show the feasibility of the refinement framework.