Formal Foundations for Situation Awareness based on Dependent Type Theory