Department of Informatics,
University of Oslo
4pm Tuesday 17th July 2007
Room 2511, JCMB, King's Buildings
In this talk I will describe CL, a language for writing (electronic) contracts with semantics in an extension of the mu-calculus. The language allows to write (conditional) obligations, permissions and prohibitions, and to represent the so-called contrary-to-duty (CTD) and contrary-to-prohibition (CTP). CTDs and CTPs are useful to establish what happens in case an obligation, respectively a prohibition, is not respected. The approach is action-based, meaning that the above normative notions are defined on actions and not on state-of-affairs.
I will then describe the main limitations of the language, and sketch some initial work on model checking contracts. I will also describe research directions we intend to pursue, including extensions of the language with timing constraints, and further development of theoretical foundations to analyse contracts.