# Questions tagged [model-checking]

Model checking refers to the following problem: given a model of a system, test automatically whether this model meets a given specification.

16 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
143 views

### Introduction to bounded model checking that describes model generation

Most of the tutorials I have found on model checking and bounded model checking start with, the model is given as a Kripke Structure M = (S,I,T,L) where S is a set of states, I is a set of initial ...
46 views

### How the $EX(f)$ is evaluated in symbolic model checking?

I was reading the symbolic model checking, So there it has mentioned that we can represent the set of states and transition relations of any transition system with the help of ROBDDs. I was trying to ...
31 views

32 views

### How Model Checking works with User Interaction

In order to understand how to apply Model Checking, I am wondering how to apply it to a pseudo-realistic async program. Say I have the following pseudocode: ...
46 views

### CTL satisfied by Kripke Structure

given a Kripke Structure I want to check if a CTL formula is satisfied or not. the CTL is: $$AG(c \vee AX\neg E((a\vee b)Uc))$$ I have read that it is better to write to CTL in terms of $\wedge$ ...
44 views

### How to Construct Kripke Structure States from Nested Functions

Say I have these defined functions: ...
58 views

### Understanding a Single Step in the Model Checking Algorithm

This answer explains roughly how to convert a nested boolean function into a Binary Decision Diagram (BDD). This question is about how to structure the states for the BDD. Now in this question I am ...
76 views

### Importance of Needham–Schroeder Protocol

I'm working on a paper about model checking on cryptographic protocols and many of the papers I have read, base their approaches in the Needham-Schroeder protocol. I undestand this was one of the ...