This is not the latest version of this item. The latest version can be found at:

Show simple item record

dc.contributor.authorCranefield, Stephenen_NZ
dc.contributor.authorWinikoff, Michaelen_NZ
dc.identifier.citationCranefield, S., & Winikoff, M. (2007). Verifying social expectations by model checking truncated paths (Information Science Discussion Papers Series No. 2007/08). University of Otago. Retrieved from
dc.description.abstractOne approach to moderating the behaviour of agents in open societies is the use of explicit languages for defining norms, conditional commitments and/or social expectations, together with infrastructure supporting conformance checking and the identification and possible punishment of anti-social agents. This paper presents a logical account of the creation, fulfilment and violation of social expectations modelled as conditional rules over a hybrid propositional temporal logic. The semantics are designed to allow model checking over finite histories to be used to check for fulfilment and violation of expectations in both online and offline modes. For online checking, expectations are always considered at the last state in the history, but in the offline mode expectations in previous states are also checked. At each past state, the then active expectations must be checked for fulfilment without recourse to information from later states: the truth of a future-oriented temporal proposition φ at state s over the full history does not imply the fulfilment at s of an expectation with content φ. This issue is addressed by defining fulfilment and violation in terms of an extension of Eisner et al.’s weak/strong semantics for LTL over truncated paths. The update of expectations from one state to the next is based on formula progression and the approach has been implemented by extending the MCLITE and MCFULL algorithms of the Hybrid Logic Model Checker.en_NZ
dc.publisherUniversity of Otagoen_NZ
dc.relation.ispartofseriesInformation Science Discussion Papers Seriesen_NZ
dc.subject.lcshQA76 Computer softwareen_NZ
dc.titleVerifying social expectations by model checking truncated pathsen_NZ
dc.typeDiscussion Paperen_NZ
otago.schoolInformation Scienceen_NZ
otago.openaccessOpen, New Zealanden_NZ
dc.identifier.eprints770en_NZ Engineering & Collaborative Modelling Laboratoryen_NZ Scienceen_NZ
dc.description.references[1] M. Alberti, F. Chesani, M. Gavanelli, E. Lamma, P. Mello, and P. Torroni. Compliance verification of agent interaction: a logic-based software tool. In R. Trappl, editor, Cybernetics and Systems 2004, volume II, pages 570–575. Austrian Society for Cybernetics Studies, 2004. [2] F. Bacchus and F. Kabanza. Using temporal logics to express search control knowledge for planning. Artificial Intelligence, 116(1-2):123–191, 2000. [3] J. Bentahar, B. Moulin, J.-J. C. Meyer, and B. Chaib-draa. A logical model for commitment and argument network for agent communication. In Proceedings of the 3rd International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2004), pages 792–799. IEEE Computer Society, 2004. [4] P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge University Press, 2001. [5] U. Cortés. Electronic institutions and agents. AgentLink News, 15:14–15, September 2004. [6] S. Cranefield. A rule language for modelling and monitoring social expectations in multi-agent systems. In Coordination, Organizations, Institutions, and Norms in Multi-Agent Systems, volume 3913 of Lecture Notes in Computer Science, pages 246–258. Springer, 2006. [7] L. Dragone. Hybrid logics model checker., 2005. [8] C. Eisner, D. Fisman, J. Havlicek, Y. Lustig, A. McIsaac, and D. V. Campenhout. Reasoning with temporal logic on truncated paths. In Computer Aided Verification, volume 2725 of Lecture Notes in Computer Science, pages 27–39. Springer, 2003. [9] U. Endriss. Temporal logics for representing agent communication protocols. In Agent Communication II, volume 3859 of Lecture Notes in Computer Science, pages 15–29. Springer, 2006. [10] M. Franceschet and M. de Rijke. Model checking hybrid logics (with an application to semistructured data). Journal of Applied Logic, 4(3):279–304, 2006. [11] N. Markey and P. Schnoebelen. Model checking a path. In CONCUR 2003 – Concurrency Theory, volume 2761 of Lecture Notes in Computer Science, pages 251–265. Springer, 2003. [12] P. Spoletini and M. Verdicchio. Commitment monitoring in a multiagent system. In Proceedings of the 5th International Central and Eastern European Conference on Multi-Agent Systems, volume 4696 of Lecture Notes in Artificial Intelligence, pages 83–92. Springer, 2007. [13] M. Verdicchio and M. Colombetti. A logical model of social commitment for agent communication. In Proceedings of the 2nd International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2003), pages 528–535. ACM Press, 2003. [14] F. Viganò and M. Colombetti. Symbolic model checking of institutions. In ICEC ’07: Proceedings of the ninth international conference on Electronic commerce, pages 35–44. ACM Press, 2007. [15] P. Yolum and M. P. Singh. Commitment machines. In Intelligent Agents VIII: 8th International Workshop, ATAL 2001, volume 2333 of Lecture Notes in Computer Science, pages 235–247. Springer, 2002.en_NZ
 Find in your library

Files in this item


This item appears in the following Collection(s)

Show simple item record


*Selected version