He, L.; Liu, G. Verifying Computation Tree Logic of Knowledge via Knowledge-Oriented Petri Nets and Ordered Binary Decision Diagrams. Comput. Inform. 2021, 40, 1174–1196.