Run-Time Monitoring of Electronic Contracts

  • Marcel Kyas
  • Cristian Prisacariu
  • Gerardo Schneider
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5311)


Electronic inter-organizational relationships are governed by contracts regulating their interaction, therefore it is necessary to run-time monitor the contracts, as to guarantee their fulfillment. The present work shows how to obtain a run-time monitor for contracts written in \(\mathcal {CL}\), a formal specification language which allows to write conditional obligations, permissions, and prohibitions over actions. The trace semantics of \(\mathcal {CL}\) formalizes the notion of a trace fulfills a contract. We show how to obtain, for a given contract, an alternating Büchi automaton which accepts exactly the traces that fulfill the contract. This automaton is the basis for obtaining a finite state machine which acts as a run-time monitor for \(\mathcal {CL}\) contracts.


Deontic Logic Dynamic Logic Concurrent Action Propositional Dynamic Logic Deontic Modality 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260–272. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  2. 2.
    Chandra, A.K., Kozen, D., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114–133 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. Formal Methods in System Design 24(2), 101–127 (2004)CrossRefzbMATHGoogle Scholar
  4. 4.
    Fischer, M.J., Ladner, R.E.: Propositional modal logic of programs. In: STOC 1977, pp. 286–294. ACM, New York (1977)Google Scholar
  5. 5.
    Göller, S., Lohrey, M., Lutz, C.: PDL with Intersection and Converse Is 2 EXP-Complete. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 198–212. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  6. 6.
    Harel, D., Tiuryn, J., Kozen, D.: Dynamic Logic. MIT Press, Cambridge (2000)zbMATHGoogle Scholar
  7. 7.
    Kozen, D.: A completeness theorem for kleene algebras and the algebra of regular events. Information and Computation 110(2), 366–390 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312–360 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Manna, Z., Pnueli, A.: Specification and verification of concurrent programs by ∀-automata. In: POPL 1987, pp. 1–12 (1987)Google Scholar
  10. 10.
    Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: LICS 1988, pp. 422–427 (1988)Google Scholar
  11. 11.
    Pratt, V.R.: Process logic. In: POPL 1979, pp. 93–100. ACM Press, New York (1979)Google Scholar
  12. 12.
    Prisacariu, C., Schneider, G.: A formal language for electronic contracts. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 174–189. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  13. 13.
    Prisacariu, C., Schneider, G.: CL: A Logic for Reasoning about Legal Contracts – Semantics. Technical Report 371, Univ. Oslo (2008)Google Scholar
  14. 14.
    Prisacariu, C., Schneider, G.: Run-time Monitoring of Electronic Contracts – theoretical results. Technical report, Univ. Oslo (2008)Google Scholar
  15. 15.
    Stolz, V., Bodden, E.: Temporal Assertions Using AspectJ. In: RV 2005. ENTCS, vol. 144, pp. 109–124. Elsevier, Amsterdam (2006)Google Scholar
  16. 16.
    Vardi, M.Y.: Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 191–206. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  17. 17.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS 1986, pp. 332–344 (1986)Google Scholar
  18. 18.
    von Wright, G.H.: Deontic logic. Mind 60, 1–15 (1951)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Marcel Kyas
    • 1
  • Cristian Prisacariu
    • 1
  • Gerardo Schneider
    • 1
  1. 1.Department of InformaticsUniversity of OsloBlindernNorway

Personalised recommendations