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

97 questions
Filter by
Sorted by
Tagged with
12 views

### Are automata useful in software verification?

I contrast the paradigm of SMT-based verification of software, such as in LiquidHaskell with the approach based on automata. To me it appears that automata are only used in the paradigm of model ...
47 views

60 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: ...
44 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 ...
37 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 ...
15 views

### Satisfaction of CTL

I'm trying to compute Sat(Φ), but I can't seem to figure out this question, what i understood is that I first need to solve Sat(req U -busy), but it doesn't make sense, how can it be that req is true ...
16 views

### Transition System Problem

I'm very confused about this question, would it be correct to say that (a) is false since executing the state ~req ready being repeated would invalidate that statement ?