# 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.

17 questions
0answers
130 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 ...
0answers
43 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 ...
0answers
92 views

### Spot the formalism (some kind of process logic)

Consider the following specification technique. A specification consists of a finite set of triples $\langle C, A, C' \rangle$, where $A$ is the name of an action and $C, C'$ are conditions, that is, ...
0answers
135 views

### Equivalence preserving operator from CTL* to LTL

The question is about an operator that transforms any CTL* formula ${\psi}$ into a (not necessarily equivalent) LTL formula ${A\psi^d}$, where $d$ means syntactically removing all $A,E$ quantifiers ...
0answers
46 views

0answers
37 views

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

Say I have these defined functions: ...
0answers
49 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 ...
0answers
71 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 ...
0answers
86 views

### Calculate expected values of “Craps Game” with the help of Prism Model Checker

I have modelled the craps game (https://en.wikipedia.org/wiki/Craps#Rules_of_play) as a dtmc with the prism model checker: ...
0answers
94 views

0answers
51 views

### How to combine Symbolic Model Checking with Symbolic Execution

I have started reading some textbooks and papers on Model Checking, and have run into the closely related but different Symbolic Execution. I have a few open questions on StackOverflow about the "...
0answers
41 views

### Create a transition system where every sequence has at least twice as many $a$'s than $b$'s

Create a transition system with edges $a$ and $b$ and an initial state, such that for all possible sequences, you have that: The amount of $a$'s in the sequence is at least twice as much as the ...