Last call to make your voice heard! Our 2022 Developer Survey closes in less than a week. Take survey.

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

100 questions
Filter by
Sorted by
Tagged with
21 views

### First-order model checking is not fixed parameter tractable on general graphs

I read that the problem of first-order model checking is believed to be not fixed parameter tractable on general graphs. Why is this the case? Would be happy about some reference Thanks in advance!
1 vote
30 views

### First-order model checking on general graphs is intractable

I read that the first-order model checking problem is intractable on general graphs. How is this shown? Would be happy about some reference! Thanks in advance
12 views

73 views

### Is there a tool that can check whether m |= p holds, where m and p are both ltl formula

To the best of my understanding, m |= p asks whether the ltl formula p satisfies the ltl formula m. In other words, m -> p is a tautology. Here are some example of where m |= p hold: ...
50 views

### Does Rice's theorem apply to sequential logic circuits?

I am wondering if Rice's theorem (or something similar to that) applies also to sequential circuits. I.e. given any finite sequential circuit, can there be an algorithm that can formally verify any ...
42 views

### Check if given safety properties are regular, and if so construct NFAs

Let $\mathit{AP} = \{a, b, c\}$. Consider the following LT properties: Between two neighboring occurrences of $a$, $b$ always holds. Between two neighboring occurrences of $a$, $b$ occurs more often ...
42 views

### Automaton-based model checking on finite traces

I want to check whether a formula in finite LTL is valid on a finite, linear trace. For infite traces I would create a Kripke structure of the trace and a Büchi automaton for the negated formula, ...
21 views

### Fault localisation using model checking

In many papers like Empirical Evaluation of the Tarantula Automatic Fault-Localization Technique there is a good explanation about how tarantula algorithm can be used with test suits. Is there any ...
1 vote
106 views

### What are the limitations of symbolic model checking?

What are the limitations of the Symbolic Model Checking? As far as I know, "state-space explosion" can still happen by this technique but it can explore much larger state space. So, is the Symbolic ...
1 vote
25 views

### Review of Formal Verification and How to Apply it to Greenfield Project [duplicate]

Last year I looked heavily into Formal Verification, such as automated theorem proving, model checking, type systems, symbolic evaluation, and many others. I probably spent a few weeks or maybe months ...
500 views

### What goes into proving two complicated programs are equivalent?

Say I wanted to prove that two programs were equivalent (either rigorously if possible, or informally if not). More specifically, say I have something relatively complex such as an HTTP server ...
37 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 ...
60 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 ...
57 views

111 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? ...
105 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 ...
801 views

232 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 ...
105 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 ...
188 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 (...
1 vote
37 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: ...
340 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, ...
123 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 ...
297 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 ...
503 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 ...
1 vote
62 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$ ...
1 vote
51 views

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

Say I have these defined functions: ...
1 vote
72 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 ...
263 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 ...
1 vote
84 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 ...
97 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 (...
118 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 ...