Temporalised Epistemic Logic for Reasoning about Agent-Based Systems

For modelling and verifying agent systems, many researchers have proposed different logical systems. Since agent-based systems are designed to operate in dynamic environments such as the Internet, it is also important to model the temporal aspects of such systems in a systematic way. In this paper, we use a temporalised epistemic logic called TEL for formalising agent-based systems. We also propose a labelled tableau system and a model checking method for this logic. With logic TEL and its associated proof system, we are able to reason about, and verify agent systems operating in dynamic environments.