These are the notes I take on Clarke et al.’s Model Checking. I haven’t finished reading the book yet, so there will be more posts about it (and that’s why I assign a number in the title). In the first post, I introduce some basic concepts from model theory and briefly describe the models used in model checking.