A dynamic deontic logic for complex contracts

We present a dynamic deontic logic for specifying and reasoning about complex contracts. The concepts that our contract logic CL captures are drawn from legal contracts, as we consider that these are more general and expressive than what is usually found in computer science (like in software contracts, web services specifications, or communication protocols). CL is intended to be used in specifying complex contracts found in computer science. This influences many of the design decisions behind CL. We adopt an ought-to-do approach to deontic logic and apply the deontic modalities exclusively over complex actions. On top, we add the modalities of dynamic logic so to be able to reason about what happens after an action is performed. CL can reason about regular synchronous actions capturing the notion of actions done at the same time. CL incorporates the notions of contrary-to-duty and contrary-to-prohibition by attaching to the deontic modalities explicitly a reparation which is to be enforced in case of violations. Results of decidability and tree model property are given as well as specific properties for the modalities.