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

85 questions
Filter by
Sorted by
Tagged with
23 views

### Proving that a property is k-inductive with an SMT solver (parametric resettable counter)

I'm following the slides at https://homepage.cs.uiowa.edu/~tinelli/talks/FT-11.pdf where Tinelli explains how k-induction works in the context of SMT based model checking. A parametric and resettable ...
45 views

### Modeling a set of probabilistic concurrent processes

I'm looking into discrete-time Markov chains (DTMCs) for use in analyzing a probabilistic consensus protocol. One basic thing I haven't been able to figure out is how to model a set of independent ...
31 views

46 views

### Is model checking PSpace-hard *in formula size*?

Sistla/Clarke proved [SC82] that the LTL model-checking problem is PSpace-complete. Sometimes people write that this problem is "PSpace-hard in $|\phi|$" (e.g. [LP85]). What does this mean formally? ...
53 views

### Are two CCS processes equivalent with respect to weak bisimilarity if and only if they satisfy exactly the same set of HML formulas?

I was skimming this recent paper and I was struck by the following statement: two processes are equivalent with respect to weak bisimilarity if and only if they satisfy exactly the same set of HML ...
236 views

83 views

### How do you correctly write this sentence as a CTL formula?

Sentence: From every reachable state it is possible to reach a state where $p$ is true. How do you write this sentence as a CTL formula? So far I only dealt with CTL syntax and trees but maybe it ...
86 views

### How to express the existence of winning strategy of the starter of a game in temporal logic?

Consider a two-player game. A winning strategy of a player is a strategy following which the player can always beat his opponent, no matter how his opponent responds. A game can be unfolded to a ...
62 views

### How to collect all states of a behavior in TLA+?

Description of the problem: I am modeling checking a distributed protocol against a global property with TLA+ developed by Leslie Lamport. The global property is defined on all states of a behavior (...
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: ...
165 views

### How to define the Atomic Propositions in Model Checking

The atomic propositions in Symbolic Model Checking form the state in the state-transition graph (the model $\mathcal{M}$ in Model Checking). The other part of Model Checking is the specification, ...
75 views

### What exactly state is in Model Checking

So I finally realized the difference between transition systems and automata, and now am closer to understanding Model Checking. One of the last pieces is understanding what exactly "state" is in ...
193 views

### Least fix point of CTL formula

In the book Logic in Computer Science on page 244, there is a proof that $[[E(\phi U\psi)]]$ is the least fixed point of $G(X)=[[\psi]] \cup ([[\phi]]\cap\mathop{\textrm{pre}}_\exists(X))$. I don't ...
262 views

### How does TLC check liveness properties?

The paper "Model Checking TLA+ Specifications" published in 1999 explained how TLC (Temporal Logic Checker) checks safety properties written in TLA+ developed by Lamport. At that time, TLC did not yet ...
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 ...
164 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 ...
54 views

### How to prove a side effect in a function

I asked a question earlier about Saving to the Database, which was very general and about the requirements for a proof when you go through many layers of non-verified systems such as the network and ...
50 views

### What the State is, and Where it comes from, when Generating Reachability Graphs

For Timed Automata, I found Figure 1 below. For Coloured Petri Nets I found Figure 2. Both are for "Reachability Graph Construction". However, they don't describe where they got the states from (...
62 views

### Acceptance conditions when translating LTL to Büchi automaton?

As an exercise in better understanding, I have been implementing the LTL to Generalized Büchi Automaton translation algorithm of Gerth, et al. (which is also discussed in Clarke, et al., Model ...
84 views

113 views

### LTL to GBA versus LTL to BA

Let's assume that I have an LTL formula and I want to convert it to a Buchi automaton. For which fragment of LTL, GBA is more succinct and for which fragment BA has the same size as GBA.
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 ...
122 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: ...
98 views

### CTL* query evaluation order

I'm currently trying to evaluate a CTL* expression and am not sure how to stepwisely evaluate the queries. For example I have EFG p. This means something like 'there is a path where eventually there ...
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 ...
149 views

### Programming language semantics prototyping tool

Is there any tool for prototyping a programming language semantics and type system and that also allows for some sort of model checking of standard properties, like type soundness? I'm asking this, ...
319 views

### Modeling a sequential circuit as a transition system

I was asked to model the following sequential circuits C1, C2 as transition systems (i.e. identify the output y function and register functions r1, r2, r3) For C2 there appears to be not input x and ...