A Petri net-based model for verification of obligations and accountability in cooperative systems

Yu Yue Du, Chang Jun Jiang, Meng Chu Zhou

Research output: Contribution to journalArticlepeer-review

66 Scopus citations


In cooperative systems (CSs), participants cannot usually ensure the correct behavior of their partners. Obligations and proofs of participants have to be performed together to achieve a common goal in a real cooperation. Without adequate accountability assurances of actions, there is no means of reliably enforcing punitive measures against fraudulent participants. However, the existing formal methods for analyzing CSs cannot properly deal with accountability and obligations. As such, this paper proposes a new class of labeled Petri net (LPN) models. The behavior of each partner is represented by an LPN, while a CS is modeled by the combination of all partners' LPN models. The behavioral properties of an overall modeled system can be well verified only by analyzing each individual LPN. LPNs provide the integration of formal notations with graphical notations and formal proofs with commonly used verification techniques. The obligations are verified based on LPN languages and the nonblocking properties of action sequences, while accountability can be proved by the network conditions and local action sequences on each partner's side. The proposed approaches are illustrated with the modeling and analysis of a Purchase transaction using the Internet Open Trading Protocol.

Original languageEnglish (US)
Pages (from-to)299-308
Number of pages10
JournalIEEE Transactions on Systems, Man, and Cybernetics Part A:Systems and Humans
Issue number2
StatePublished - 2009

All Science Journal Classification (ASJC) codes

  • Software
  • Information Systems
  • Human-Computer Interaction
  • Electrical and Electronic Engineering
  • Control and Systems Engineering
  • Computer Science Applications


  • Accountability
  • Cooperative systems
  • Discrete event system
  • Formal model
  • Obligations
  • Petri nets


Dive into the research topics of 'A Petri net-based model for verification of obligations and accountability in cooperative systems'. Together they form a unique fingerprint.

Cite this