Model Checking and Monitoring Norms defined by Interdependent Institutions

This project aims to conclude some research directions that have been partially explored during the Swiss National Science Foundation project "Artificial institutions: specification and verification of open distributed interaction frameworks". In particular, during this project we plan to extend FIEVeL, a language to model institutions, as follows:1) We will introduce new constructs to define norms characterized by complex temporal dimensions and which can be translated into automata capable of recognizing when agents fulfil or violate norms. As a consequence, we will provide designers with an expressive language to describe norms that can be exploited to automatically classify institutional states as legal or illegal.2) We will develop an automatic translation of FIEVeL axioms into Prolog to obtain a set of rules capable of determining the current institutional state and what violations are produced by the occurrence of an event. We will also investigating how to integrate a monitoring system of this kind with Jade and how agents can reason about norms to decide how to act.