Abstract
One 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.