Some relationships among knowledge operators, the past temporal operator once, and the future temporal operators in multi-agent systems

We consider some relationships among the knowledge operators (Ki, Kj), the past temporal operator (the once operator), and the future temporal operators (the next operator, the eventually operator, the always operator) in multi-agent systems. These relationships describe agent properties in multi-agent systems (the properties relate knowledge of two agents): if agent i has known F: then agent j will know F in the next step; if agent i has known F, then agent j will eventually know F; if agent i has known F, then agent j will always know F; and if agent i has known F, then agent i knows F until agent j knows F. These properties can be helpful in analyzing the respective multi-agent system.