Verifying Social Expectations by Model Checking Truncated Paths
S. Cranefield, and M. Winikoff. Coordination, Organizations, Institutions and Norms in Agent Systems IV, volume 5428 of Lecture Notes in Computer Science, Springer, Berlin / Heidelberg, (2009)
DOI: 10.1007/978-3-642-00443-8_14
Abstract
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 extending the MCLITE and MCFULL algorithms of the Hybrid Logics Model Checker.
%0 Book Section
%1 springerlink:10.1007/978-3-642-00443-8_14
%A Cranefield, Stephen
%A Winikoff, Michael
%B Coordination, Organizations, Institutions and Norms in Agent Systems IV
%C Berlin / Heidelberg
%D 2009
%E Hübner, Jomi
%E Matson, Eric
%E Boissier, Olivier
%E Dignum, Virginia
%I Springer
%K agents myown
%P 204-219
%R 10.1007/978-3-642-00443-8_14
%T Verifying Social Expectations by Model Checking Truncated Paths
%U http://dx.doi.org/10.1007/978-3-642-00443-8_14
%V 5428
%X 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 extending the MCLITE and MCFULL algorithms of the Hybrid Logics Model Checker.
%@ 978-3-642-00442-1
@incollection{springerlink:10.1007/978-3-642-00443-8_14,
abstract = {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 extending the MCLITE and MCFULL algorithms of the Hybrid Logics Model Checker.},
added-at = {2011-09-29T04:44:49.000+0200},
address = {Berlin / Heidelberg},
affiliation = {University of Otago Department of Information Science Dunedin New Zealand},
author = {Cranefield, Stephen and Winikoff, Michael},
biburl = {https://www.bibsonomy.org/bibtex/27829fb1238f30cb1dcd23777d3cba914/scranefield},
booktitle = {Coordination, Organizations, Institutions and Norms in Agent Systems IV},
doi = {10.1007/978-3-642-00443-8_14},
editor = {Hübner, Jomi and Matson, Eric and Boissier, Olivier and Dignum, Virginia},
interhash = {4ac18ee5fb66ab1cd69884c0963d4ac6},
intrahash = {7829fb1238f30cb1dcd23777d3cba914},
isbn = {978-3-642-00442-1},
keywords = {agents myown},
pages = {204-219},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
timestamp = {2011-09-29T04:44:49.000+0200},
title = {Verifying Social Expectations by Model Checking Truncated Paths},
url = {http://dx.doi.org/10.1007/978-3-642-00443-8_14},
volume = 5428,
year = 2009
}