Actor-oriented system specification with dynamic logic

In this paper, we extend dynamic logic with the concept of an actor in order to be able to specify who takes the initiative of an action, who makes a choice, or who controls a synchronization of actions. We give two examples of application of this idea. First, we show how to generalize an approach taken up by De Nicola and Hennessy, who eliminate tau from CCS in favor of internal and external choice. We show that this generalization allows a more accurate specification of system behavior than is possible without it. Second, deontic logic has been used by several researchers as a system specification language. In the course of this application, a number of paradoxes of classical deontic logic have been resolved, except the paradox of free choice permission. We show that actors can be used to resolve this paradox as well.