CL: An Action-Based Logic for Reasoning about Contracts

摘要

This paper presents a new version of the CL contract specification language. CL combines deontic logic with propositional dynamic logic but it applies the modalities exclusively over structured actions. CL features synchronous actions, conflict relation, and an action negation operation. The CL version that we present here is more expressive and has a cleaner semantics than its predecessor. We give a direct semantics for CL in terms of normative structures. We show that CL respects several desired properties from legal contracts and is decidable. We relate this semantics with a trace semantics of CL which we used for run-time monitoring contracts.