Goal-directed semantics for dynamic logic

Abstract

The general definition of an algorithm contains information about actions and the order in which they are performed to achieve specific goals, which can be represented by some description. In the semantics of dynamic logic, the emphasis is on actions that must be performed in a certain sequence, and the goal pursued remains outside the scope of analysis, it is assigned the role of meta-information in relation to the algorithm itself. On the other hand, the same goal can be achieved in different ways. If the goal for which the algorithm is compiled and executed is primarily important for the acting agent, then its specific implementation is not so important, since the invariant of all specific implementations is precisely the goal being pursued. The article shows how it is possible to construct the semantics of dynamic logic in terms of goals rather than actions performed. Goal-oriented semantics is applicable not only to the analysis of algorithms performed in the world of abstract mathematical objects, but also in the physical world, in which the concept of algorithm is synonymous with the concept of purposeful behavior. Since the concept of goal refers to a future state of affairs that has not yet been realized and is therefore meaningful only within the framework of the accepted time model, the semantics of goal-oriented logic is based on the semantics of the Occamist temporal logic of tree-branching time. At the same time, the agent executing the algorithm must also have some freedom in choosing the actions it performs. While in the standard semantics of dynamic logic, elementary actions are interpreted through unmediated transitions between possible worlds, in goal-oriented semantics, actions are interpreted by segments of possible event paths, at the end point of which the goal for which the action is being performed is true, and at all previous moments is false. In terms of the proposed semantics, it is possible, with some variations, to define all the standard operators of dynamic logic, plus one more special operator for accessing processes occurring in the external physical world.