Distributed runtime verification by past-CTL and the field calculus

Recent trends in the engineering of software-intensive systems increasingly promote the adoption of computation at the edge of the network, in the proximity of where sensing and actuation are performed. Applications are executed directly in IoT devices deployed in the physical environment, possibly with the aid of edge servers: there, interactions are essentially based on physical proximity, and communication with the cloud is sporadic if not absent.