Characterizing causal action theories and their implementations in answer set programming

We consider a simple language for writing causal action theories, and postulate several properties for the state transition models of these theories. We then consider some possible embeddings of these causal action theories in some other action formalisms, and their implementations in logic programs with answer set semantics. In particular, we propose to consider what we call permissible translations from these causal action theories to logic programs. We identify two sets of properties, and prove that for each set, there is only one permissible translation, under strong equivalence, that can satisfy all properties in the set. We also show that these two sets of conditions are minimal in that removing any condition from each of them will result in multiple permissible mappings. Furthermore, as it turns out, for one set, the unique permissible translation is essentially the same as Balduccini and Gelfond's translation from Gelfond and Lifschitz's action language B to logic programs. For the other, it is essentially the same as Lifschitz and Turner's translation from the action language C to logic programs. This work provides a new perspective on understanding, evaluating and comparing action languages by using sets of properties instead of examples. The results in this paper provide a characterization of two representative action languages B and C in terms of permissible mappings from our causal action theories to logic programs. It will be interesting to see if other action languages can be similarly characterized, and whether new action formalisms can be defined using different sets of properties.