An Efficient Model Checking Method of Agent Knowledge under Dynamic Environments

摘要

We study the problem of deciding what knowledge an agent in a dynamic environment with finite states has after a series of events. van der Meyden formalized this as the model checking problem of modal formulas by representing the environment as a synchronous distributed system with perfect recall. He showed that the time complexity of his decision algorithm is linear in r, where r is the length of a run r (i.e., the number of events). But the time complexity depends on ]Wl, where W is the number of states' We show that the worst case time complexity increases in at least exponential order with respect to W. We present that it can be decided in time polynomial in lWI and linear in r if we restrict modal formulas to cases where 'not knowing' cannot be represented.