def nk(fsm, agent, phi):
    """
    Return the set of states of fsm satisfying nK<'agent'> phi
    
    fsm -- a MAS representing the system
    agent -- the (str) name of an agent of fsm
    phi -- a BDD representing the set of states of fsm satisfying phi
    """
    return fsm.equivalent_states(phi & fsm.reachable_states, frozenset({agent})
        ) & fsm.reachable_states
