A dynamic logic of action (Q1337608)

The paper deals with various extensions of propositional dynamic logic (PDL) to logics for reasoning about action types. The basic extended formalism, DLA, incorporates names for states and time points. In the semantics, transition relations do not just relate states but rather pairs \(\langle s, t\rangle\), where \(s\) is a state and \(t\) is an instant. Moreover, the language of DLA contains an action program \(a\) representing all performances of atomic actions executable by the agent in the given context and an external influence program \(e\) representing the transitions which are beyond the influence of the agent. As an additional powerful technical device a universal program \(u\) is included representing the universal transition relation. DLA is then enlarged by further formula and action type forming operations. The three resulting extensions, \(\text{DLA}_ R\), \(\text{DLA}_ A\) and \(\text{DLA}_ P\), allow certain reasoning about the results of actions, abilities and parallel performances of actions, respectively. Each extension of DLA is carefully motivated by drawing on widely accepted conceptual analyses of action theorists, in particular G. H. von Wright. The paper is clearly written. The systems presented might at first sight appear to be rather complex, both syntactically and semantically. However, the suggested axiom schemata and inference rules as well as the semantical models seem intuitively plausible, and, moreover, the sketches of the completeness proofs follow a familiar pattern. When compared to pure PDL, DLA and its extensions provide a considerable increase of expressiveness, which, without doubt, will prove to be useful for a logical analysis of human action.