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

111 questions
Filter by
Sorted by
Tagged with
8 views

### Counterexample Construction and Translation in CEGAR

As in this slide, M2 is an abstraction of M1 using the abstraction function f1 which essentially groups based on labels. Then we see that the property is not satisfied by the abstraction so we find ...
• 80
17 views

### When does Simulation Equivalent imply Bisimulation

Here, Given 2 Kripke structures M1 and M2, if there exists a simulation from M1 to M2 and a simulation from M2 to M1, is there a bisimulation from M1 to M2?, it is shown that for two LTSs M1 and M2 ...
• 80
14 views

### ROBDDs heuristics for optimal variable ordering

I have this slide about how a BDD can vary in size depending on the order of the boolean variables fixed for it, and how it is NP-Complete to find the optimal ordering. It says there are heuristics ...
• 80
16 views

### LTL Model Checking Worst Case size for NBA

I have a slide that gives the worst case time complexity of LTL model checking which uses a product construction of an LTS along with the NBA for the negation of the LTL formula. My question is, when ...
• 80
16 views

### Irregular Safety Properties

A regular safety property is a safety property whose bad prefixes form a regular language, https://moves.rwth-aachen.de/wp-content/uploads/WS1920/MC/mc2019_handout_lec4.pdf. My questions is, are there ...
• 80
123 views

### Can CTL* express every model's behaviour

CTL* as in https://en.wikipedia.org/wiki/CTL*, is a logic that combines CTL and LTL. I know that CTL* can express everything expressible in these two languages and more. My question is whether we can ...
• 80
33 views

### Given 2 Kripke structures M1 and M2, if there exists a simulation from M1 to M2 and a simulation from M2 to M1, is there a bisimulation from M1 to M2?

Given two kripke structures $M_1$ and $M_2$, if $M_1\leq_{sim}M_2$ and $M_2\leq_{sim}M_1$, then does $M_1\leq_{b-sim}M_2$ holds? intuitively, I think that it's not true, since two simulations are ...
• 241
60 views

### Is there a model for the given logical formula, and if not, why?

I'm trying to determine whether there exists a model for the following logical formula: $(p_1 \to (p_2 \lor p_3)) \land(p_2 \to \neg p_3) \land ((p_1 \lor p_3) \to \neg p_2)$. Here's my understanding ...
192 views

### Does this paper by Patrick Cousot describe an undecidable method for model checking?

All of the discussion is in the context of this paper. I think that the whole procedure that the paper describes is not decidable, because if we can have an algorithm for it, then we can solve halting ...
• 31
329 views

### Real-life applications of pure Mealy machines

I'm currently studying formal methods in software engineering related to state machines, specifically Mealy machines. This made me wonder how relevant Mealy machines really are for practical ...
• 161
68 views

### Safety VS. Liveliness Property

I have to prove whether a certain property is safety or liveliness. The property represents the absence of deadlock so I expected it to be a safety property from what I read online. The issue is that ...
• 121
121 views

### Transition System vs State Machines

Why there is no final state for a transition system? And why do NFA and DFA have final states? The transition system may or may not have any terminal states, but NFA/DFA has at least one final state (...
350 views

### How can I prove that LTL formula is valid?

I do not know with which technique i can prove if a LTL forumula is valid. Let's say we have for example this one: ¬q U(¬p ∧ ¬q) → ¬Gp. How can prove if this valid or not? (should be true in any state ...
• 3
40 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
38 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
184 views

### Understanding a proof from a paper (model checking game)

I'm reading the paper: "Model Checking Games for Branching Time Logics" by Martin Lange and Colin Stirling - https://carrick.fmv.informatik.uni-kassel.de/~mlange/papers/jlc2000.pdf. The ...
• 41
92 views

### Abstract Interpretation: Connection between soundness relation and a Galois connection

I am currently studying the paper "Abstract Interpretation Frameworks" by Cousot and Cousot from 1992 (https://doi.org/10.1093/logcom/2.4.511) to gain an understanding of the theory behind ...
• 161
252 views

### Getting rid of "FG" in a LTL equation

i am currently struggling with a Linear temporal logic equation: $$\phi=FG( \lnot a\lor X \lnot a )$$ For my understanding, it means that starting at a certain point in the future, proposition a can ...
34 views

• 41
458 views

### Calculating probability of reaching state in DTMC

Consider a highly-connected graph of states & transitions where each transition is marked with a weight (representing probability of occurring) and the graph satisfies the Discrete Time Markov ...
• 209
384 views

### Safety property vs Liveness property

If i take a safety property $SP$ and a liveness property $LP$, is it true that the result of their intersection is a safety property (and not a liveness property) ? Why ? Thanks
490 views

• 23
66 views

### (Generally) How to specify asynchronous action with side effects using logic equations

Say you have this function call sequence: function all() { fn1() fn2() fn3() } And say that fn2 was asynchronous and ...
• 2,243
1 vote
322 views

### Buchi automata in formal software verification

As I am studying the application of Buchi automata in formal software verification, I am interested in the computational complexity (or links to papers) for the algorithms used to solve the problem in ...
• 237
222 views

### Model Checking CTL* algorithm

Currently I'm trying to understand the CTL* model checking algorithm from this book. The basic idea is clear to that we can use the LTL algorithm to whenever we have a subformular $E\phi$ or $A\phi$ ...
• 415
1 vote
221 views

### Validity of CTL formula $s_0 \models EG\ AF\ p$ in given model

I have been learning Verification by model checking recently and I get the following question: Is the CTL formula $s_{0} \models EG\ AF\ p$ valid in the following model? I think it is ...
• 135