Compliance through Model Checking

In this short note, we describe part of a case study about Singapore’s Personal Data Protection Act, which we first presented informally, then formally as interacting Timed Automata. From these, we derive desiderata on a language and verification framework for reasoning about compliance.