Pervasive - Specification and Verification of Complex Location Events with Panoramic