In this paper, we discuss the weakness of current action languages for sensing actions with respect to modeling domains with multi-valued fluents. To address this problem, we propose a language with sensing actions and multi-valued fluents, called AMK, provide a transition function based semantics for the language, and demonstrate its use through several examples from the literature. We then define the entailment relationship between action theories and queries in AMK, denoted by ⊧AMK, and discuss some properties about AMK.

We present a representation for reasoning and planning with an incomplete state description (open-world) called PSIPLAN-S. The presented formalism has several properties critical for application domains with a large degree of incompleteness in the state description, particularly, in domains with a large or unknown set of all objects. The formalism offers (1) considerably expressive state and goal description language, that includes limited universal quantification, (2) representation of sensing actions and knowledge goals, (3) a correct and complete state update procedure, and (...) (4) complete reasoning within a substantial subset of the language. The approach is illustrated by examples from a working system. (shrink)

Planning with incomplete knowledge becomes a very active research area since late 1990s. Many logical formalisms introduce sensing actions and conditional plans to address the problem. The action language $\mathcal{A}_{K}$ invented by Son and Baral is a well-known framework for this purpose. In this paper, we propose so-called cautious and weakly cautious semantics for $\mathcal{A}_{K}$ , in order to allow an agent to generate and execute reliable plans in safety-critical environments. Intuitively speaking, cautious and weakly cautious semantics enable the agent (...) to know exactly what happens after the execution of an action. Computational complexity analysis shows that cautious semantics reduces the reasoning complexity of $\mathcal{A}_{K}$ , it is also worth to point out that many useful domains could still be expressed with this setting. Another important contribution of our work is the development of Hoare style proof systems. These proof systems are served as inference mechanisms for the verification of conditional plans, and proved to be sound and complete. In addition, they could also be used for plan generation, in the sense that constructing a derivation is indeed a procedure to finding a plan. We point out that the proof systems posses a nice property for off-line planning, that is, the agent could generate and store short proofs in her spare time, and perform quick plan query by easily constructing a long proof from the stored shorter ones (under the assumption that sufficient proofs are stored). (shrink)