CL: An Action-Based Logic for Reasoning about Contracts
Cristian Prisacariu, Gerardo Schneider · 2009
Abstract. This paper presents a new version of the CL contract speci-fication 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 nega-tion operation. The CL version that we present here is more expressive and has a cleaner semantics than its predecessor. We give a direct seman-tics 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. 1