Contract automata | Artificial Intelligence and Law Skip to main content
Springer Nature Link
Log in

Contract automata

An operational view of contracts between interactive parties

  • Published:
Artificial Intelligence and Law Aims and scope Submit manuscript

Abstract

Deontic logic as a way of formally reasoning about norms, an important area in AI and law, has traditionally concerned itself about formalising provisions of general statutes. Despite the long history of deontic logic, given the wide scope of the logic, it is difficult, if not impossible, to formalise all these notions in a single formalism, and there are still ongoing debates on appropriate semantics for deontic modalities in different contexts. In this paper, we restrict our attention to contracts between interactive parties, which are both general enough to be an interesting object of study but specific enough so as to narrow down the debates regarding the meaning of modalities, and present a formalism for reasoning about them.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Notes

  1. Multi-actions are necessary, since it would otherwise be impossible not to violate a contract which enforces two different obligations at the same time.

  2. Although we have no notion of reparation yet, we introduce this possible state to be used in Sect. 4.

  3. An asterisk \(*\) on a transition is used to denote that any action set not matching any other outgoing transition from the source state would follow this transition. Formally, it would be a set of transitions, one for each uncatered for action set.

  4. The expression ok is used to denote that none of the clauses in the source state are violated by either of the parties.

  5. We represent a stack in the following way: \((H,q_{{\mathscr {C}}\!{\mathscr {A}}}):hs\), where \((H,q_{{\mathscr {C}}\!{\mathscr {A}}})\) is the item on top of the stack, \(q_{{\mathscr {C}}\!{\mathscr {A}}}\) is the current state in automaton H and hs is the rest of the stack.

  6. We do not present the trivial cases of actions 0 and 1; they are omitted in the rest of the paper.

References

  • Arnold A (2002) Nivat’s processes and their synchronization. Theor Comput Sci 281:31–36

    Article  MATH  Google Scholar 

  • Azzopardi S (2014) Extending contract automata with reparation, hypothetical and conditional clauses. Technical report University of Malta

  • Azzopardi S, Pace GJ, Schapachnik F (2014) Contract automata with reparations. In: Legal knowledge and information systems—JURIX 2014: the twenty-seventh annual conference, Jagiellonian University, Krakow, Poland, 10–12 December 2014, Frontiers in artificial intelligence and applications, vol 271, pp 49–54. IOS Press

  • Basile D, Degano P, Ferrari GL (2014) Automata for analysing service contracts. In: Trustworthy global computing—9th international symposium, TGC 2014, Rome, Italy, 5–6 Sept, 2014. Revised Selected Papers, Lecture notes in computer science, vol 8902, pp 34–50. Springer

  • Bench-Capon TJM (2014) Analysing norms with transition systems. In: Legal knowledge and information systems—JURIX 2014: the twenty-seventh annual conference, Jagiellonian University, Krakow, Poland, 10–12 Dec 2014, Frontiers in artificial intelligence and applications, vol 271, pp 29–38. IOS Press

  • Díaz G, Cambronero ME, Martínez E, Schneider G (2011) Timed automata semantics for visual e-contracts. In: 5th international workshop on formal languages and analysis of contract-oriented software (FLACOS’11), electronic proceedings in theoretical computer science, vol 68, pp 7–21. Málaga, Spain

  • Díaz G, Cambronero ME, Martínez E, Schneider G (2013) Specification and verification of normative texts using C-O diagrams. IEEE Trans Softw Eng 99:1

    Google Scholar 

  • Fasli M (2002) On commitments, roles, and obligations. In: Revised papers from the second international workshop of central and eastern Europe on multi-agent systems: from theory to practice in multi-agent systems, CEEMAS ’01, pp 93–102. Springer

  • Fenech S, Pace GJ, Schneider G (2009) Automatic conflict detection on contracts. In: ICTAC’09, LNCS, vol 5684, pp 200–214. Springer

  • Fenech S, Pace GJ, Schneider G (2009) CLAN: a tool for contract analysis and conflict discovery. In: ATVA’09, LNCS, vol 5799, pp 90–96. Springer

  • Flood MD, Goodenough OR (2014) Contract as automaton: the computational representation of financial agreements. Available at SSRN 2538224

  • Governatori G (2005) Representing business contracts in RuleML. Int J Coop Inf Syst 14(2–3):181–216

    Article  Google Scholar 

  • Governatori G, Milosevic Z (2005) Dealing with contract violations: formalism and domain specific language. In: EDOC enterprise computing conference, 2005 ninth IEEE international, pp 46–57. IEEE

  • Hage J (2001) Contrary to duty obligations—a study in legal ontology. In: Legal knowledge and information systems (JURIX 2001)

  • Herrestad H, Krogh C (1995) Deontic logic relativised to bearers and counterparties. Anniv Anthol Comput Law 453–522

  • Hohfeld W (1913) Some fundamental legal conceptions as applied in judicial reasoning. Yale Lj 23:16

    Article  Google Scholar 

  • Kanger S, Kanger H (1966) Rights and parliamentarism. Theoria 32(2):85–115

    Article  Google Scholar 

  • Kripke S (1963) Semantical considerations on modal logic. Acta Philos Fenn 16:83–94

    MathSciNet  MATH  Google Scholar 

  • Kyas M, Prisacariu C, Schneider G (2008) Run-time monitoring of electronic contracts. In: 6th international symposium on automated technology for verification and analysis (ATVA’08), LNCS, vol 5311. Springer, Seoul, pp 397–407

  • Leucker M, Schallhart C (2009) A brief account of runtime verification. J Log Algebr Program 78(5):293–303

    Article  MATH  Google Scholar 

  • Lindahl L (1977) Position and change: a study in law and logic, vol 112. Springer, Berlin

    Book  Google Scholar 

  • Makinson D (1986) On the formal representation of rights relations. J Philos Log 15(4):403–425

    Article  MathSciNet  MATH  Google Scholar 

  • Marjanovic O, Milosevic Z (2001) Towards formal modeling of e-contracts. In: Proceedings of the 5th IEEE international conference on enterprise distributed object computing, EDOC ’01, pp 59–68. IEEE Computer Society, Washington

  • Martínez E, Díaz G, Cambronero M (2011) Contractually compliantservice compositions. In: Proceedings of the 9th international conference on service-oriented computing (ICSOC’11), Lecture notes in computer science, vol 7084, pp 636–644. Springer, Berlin, Paphos

  • Martínez E, Díaz G, Cambronero ME, Schneider G (2010) A modelfor visual specification of e-contracts. In: The 7th IEEE international conference on services computing (IEEE SCC’10), pp 1–8. IEEE Computer Society, Miami

  • McNamara P (2006) Deontic logic. In: Gabbay DM, Woods J (eds) Handbook of the history of logic, vol 7. North-Holland Publishing, Amsterdam, pp 197–289

    Google Scholar 

  • Mikk E, Lakhnech Y, Siegel M (1997) Hierarchical automata as model for statecharts. In: Third Asian computing science conference. Advances in computing science—ASIAN’97, Lecture notes in computer science, vol 1345. Springer

  • Pace GJ, Schapachnik F (2011) Permissions in contracts, a logical insight. In: The 24th international conference on legal knowledge and information systems (JURIX’11), Frontiers in artificial intelligence and applications, vol 235. IOS Press, University of Vienna, Austria

  • Pace GJ, Schapachnik F (2011) Permissions in contracts, a logical insight. In: JURIX, pp 140–144

  • Pace GJ, Schapachnik F (2012) Contracts for interacting two-party systems. In: FLACOS’12, ENTCS, vol 94

  • Pace GJ, Schapachnik F (2012) Types of rights in two-party systems: a formal analysis. In: Legal knowledge and information systems—JURIX 2012: the twenty-fifth annual conference, University of Amsterdam, The Netherlands, 17–19 Dec 2012, Frontiers in artificial intelligence and applications, vol 250, pp 105–114. IOS Press

  • Pace GJ, Schapachnik F (2013) Synthesising implicit contracts. In:ICAIL’13. ACM, New York, pp 217–221

  • Pardo R, Colombo C, Pace G, Schneider G (2016) An automata-based approach to evolving privacy policies for social networks. In: 16th international conference on runtime verification (RV) (Madrid, Spain, 2016), LNCS

  • Prisacariu C, Schneider G (2007) A formal language for electronic contracts. In: FMOODS, LNCS, vol 4468, pp 174–189. Springer

  • Prisacariu C, Schneider G (2009) CL: an action-based logic for reasoning about contracts. In: WOLLIC’09, LNCS, vol 5514, pp 335–349. Springer

  • Prisacariu C, Schneider G (2012) A dynamic deontic logic for complex contracts. J Log Algebr Program 81(4):458–490

    Article  MathSciNet  MATH  Google Scholar 

  • Ryu Y (1998) Specification of contractual obligations in formal business communication. Data Knowl Eng 26(3):309–326

    Article  MATH  Google Scholar 

  • Salcianu A, Rinard M (2001) Pointer and escape analysis for multithreaded programs. In: ACM SIGPLAN notices, vol 36, pp 12–23. ACM

  • Santos F, Jones A, Carmo J (1997) Action concepts for describing organised interaction. In: Proceedings of the thirtieth Hawaii international conference on system sciences, 1997, vol 5, pp 373–382. IEEE

  • Surdan H (2012) Computable contracts. UCDL Rev 46:629

    Google Scholar 

  • Tan YH, Thoen W (1998) A logical model of directed obligations and permissions to support electronic contracting. Int J Electron Commer 3:87–104

    Article  Google Scholar 

  • Von Wright G (1999) Deontic logic: a personal view. Ratio Juris 12:26–38

    Article  Google Scholar 

  • Xu L (2004) A multi-party contract model. SIGecom Exch 5(1):13–23

    Article  Google Scholar 

Download references

Acknowledgments

This research has been partially supported by: UBACyT 20020130200032BA, the European ICT COST Action IC1402 (ARVI: Runtime Verification beyond Monitoring), and the Swedish Research Council under Grants Nr. 2012-5746 (ReMU: Reliable Multilingual Digital Communication: Methods and Applications) and Nr. 2015-04154 (PolUser: Rich User-Controlled Privacy Policies).

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Malta, Msida, Malta

    Shaun Azzopardi & Gordon J. Pace

  2. Departamento de Computación, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina

    Fernando Schapachnik

  3. Department of Computer Science and Engineering, University of Gothenburg, Gothenburg, Sweden

    Gerardo Schneider

Authors
  1. Shaun Azzopardi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gordon J. Pace
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Fernando Schapachnik
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Gerardo Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Fernando Schapachnik.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Azzopardi, S., Pace, G.J., Schapachnik, F. et al. Contract automata. Artif Intell Law 24, 203–243 (2016). https://doi.org/10.1007/s10506-016-9185-2

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10506-016-9185-2

Keywords

Search

Navigation