Model Checking Temporal Epistemic Logic under Bounded Recall

We study the problem of verifying multi-agent systems under the assumption of bounded recall. We introduce the logic CTLKBR, a bounded-recall variant of the temporal-epistemic logic CTLK. We define and study the model checking problem against CTLK specifications under incomplete information and bounded recall and present complexity upper bounds. We present an extension of the BDD-based model checker MCMAS implementing model checking under bounded recall semantics and discuss the experimental results obtained.

A Survey on Entropy and Economic Behaviour

Entropy plays a significant role in the study of games and economic behaviour in several ways. A decision maker faced with an n-fold repetition of a decision-making problem needs to apply strategies that become increasingly complex as n increases. When several players are involved in selecting strategies in interactive games, bounds on the memories and cognitive capacities of the players can affect possible outcomes. A player who can recall only the last k periods of history is said to have bounded recall of capacity k. We present here a brief survey of results of games played by players with different bounded recall capacities, in particular those indicating surprisingly strong relations between memory and entropy in the study of the min-max values of repeated games with bounded recall. In addition, we consider uses of entropy in measuring the value of information of noisy signal structures, also known as experiments. These are represented by stochastic matrices, with the rows representing states of the world and the columns possible signals. The classic ordering of experiments, due to David Blackwell and based on decision-making criteria, is a partial ordering, which has led to attempts to extend this ordering to a total ordering. If a decision maker has a prior distribution over the states, receipt of a signal yields a posterior. The difference between the entropy of a prior and the expected entropy of the set of possible posteriors has been proposed as a natural extension of the Blackwell ordering. We survey this alongside the theory of rational inattention, which posits that, since individuals have limited attention, they do not always follow every single piece of economic news in planning their economic behaviour. By modelling attention limits as finite channel capacity in the sense of Shannon, economists have developed a theory that explains a range of observed economic behavioural phenomena well.