JavaScript is disabled for your browser. Some features of this site may not work without it.
This is the latest version of this item.
Verifying social expectations by model checking truncated paths
Cranefield, Stephen; Winikoff, Michael
Cite this item in APA:Cranefield, S., & Winikoff, M. (2010). Verifying social expectations by model checking truncated paths. Journal of Logic and Computation, 21(6), 1217–1256. doi:10.1093/logcom/exq055
One approach to moderating the expected 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. This paper presents a logical account of the fulfilment and violation of social expectations modelled as conditional rules over a hybrid linear propositional temporal logic. Our semantics captures the intuition that the fulfilment or violation of an expectation must be determined without recourse to information from later states. We define a means of updating expectations from one state to the next based on formula progression, and show how conformance checking was implemented by combining the MCFULL model checking algorithm of Franceschet and de Rijke and the semantics for LTL over truncated paths proposed by Eisner et al. We present algorithms for both traditional offline model checking, where the complete model is available at once, and online model checking, where states are added to the model sequentially at run-time.
Notes:
This is the accepted manuscript of the paper (i.e., draft post-refereeing but prior to final editing). Changes may have been made to this work since it was submitted for publication. The definitive version is available from the publisher's web site as linked above. The paper is currently only available online, details of the volume and number will be added when the paper is published in hard copy.