Knowledge-Aware Cyber-Physical Systems

This poster showcases progress on the NSF Knowledge-Aware Cyber-Physical Systems project. We have identified a case study to be used as a stepping stone in the study of Air France Flight 447, and have started using it to understand and show-case the features of the logic under development. It highlights the important distinction between observable and unobservable events, and has led to a better representation of pilot intuition while flying. We also report major advances in the critical substitution lemma, which is a sine qua non of dynamic logics, and which is on the verge of being proven.