Show simple item record

dc.contributor.authorCranefield, Stephenen_NZ
dc.contributor.authorWinikoff, Michaelen_NZ
dc.date.available2011-04-07T03:11:46Z
dc.date.copyright2010-10-27en_NZ
dc.identifier.citationCranefield, 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/exq055en
dc.identifier.issn1465-363Xen_NZ
dc.identifier.urihttp://hdl.handle.net/10523/1240
dc.descriptionThis is a pre-copy-editing, author-produced PDF of an article accepted for publication in the Journal of Logic and Computation following peer review. Free access to the definitive publisher-authenticated version (Stephen Cranefield and Michael Winikoff, Verifying social expectations by model checking truncated paths, J Logic Computation, 21 (6): 1217-1256, 2011) is available via this link: (Please copy and paste into web browser) http://logcom.oxfordjournals.org/content/early/2010/10/27/logcom.exq055.full.pdf?ijkey=LvGK8L9zt9j9IWv&keytype=refen_NZ
dc.description.abstractOne 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.en_NZ
dc.format.mimetypeapplication/pdf
dc.publisherUniversity of Otagoen_NZ
dc.relation.ispartofJournal of Logic and Computationen_NZ
dc.relation.replaces945en_NZ
dc.subjectsocial expectationsen_NZ
dc.subjectmodel checkingen_NZ
dc.subjectmulti-agent systemsen_NZ
dc.subject.lcshQA Mathematicsen_NZ
dc.subject.lcshQA75 Electronic computers. Computer scienceen_NZ
dc.subject.lcshQA76 Computer softwareen_NZ
dc.subject.lcshQA76 Computer softwareen_NZ
dc.titleVerifying social expectations by model checking truncated pathsen_NZ
dc.typeJournal Articleen_NZ
otago.date.accession2010-11-02 20:24:56en_NZ
otago.schoolInformation Scienceen_NZ
otago.relation.issue6
otago.relation.volume21
dc.identifier.doi10.1093/logcom/exq055en_NZ
otago.bitstream.endpage1256
otago.bitstream.startpage1217
otago.openaccessOpen
otago.place.publicationDunedin, New Zealanden_NZ
dc.identifier.eprints994en_NZ
dc.description.refereedPeer Revieweden_NZ
otago.school.eprintsSoftware Engineering & Collaborative Modelling Laboratoryen_NZ
otago.school.eprintsInformation Scienceen_NZ
 Find in your library

Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record

VersionItemEditorDateSummary

*Selected version