Title: Policy Monitoring with First-order Temporal Logic

Abstract:
In security and compliance, it is often necessary to ensure that agents and
systems comply to complex policies.  An example of such a policy from financial
reporting is the requirement that every transaction of a customer c, who has
within the last 30 days been involved in a suspicious transaction, must be
reported as suspicious within 2 days.  In this talk, I will give an overview of
our approach to automated compliance checking.  In particular, I will present
our monitoring algorithm for checking properties specified in a fragment of
metric first-order temporal logic.  I will also report on case studies,
conducted together with Nokia, in security and compliance monitoring and use
these to evaluate both the suitability of this fragment for expressing complex,
realistic policies and the efficiency of our tool MONPOLY, which implements our
monitoring algorithm.

Joint work with David Basin, Matus Harvan, Samuel Mueller, and Eugen Zalinescu.