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

87 questions
Filter by
Sorted by
Tagged with
174 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, ...
179 views

### How to verify a property about a certain order of events in TCTL / UPPAAL?

I'd like to check if a certain order of events happens if another property holds true using UPPAAL and TCTL. ...
175 views

### Find equivalent LTL formula, without Y (Yesterday) operator. How can I handle first state?

The task is to find an equivalent LTL formula for $G(a \Rightarrow Yb)$, which doesn't contain the Y operator. My idea is to search for invalid path patterns with 2 $a$'s in a row, e.g. bbbbaab. ...
136 views

### Model Checking: hardware vs software

In short: What is the basic difference that allows model checking for hardware to be "easily" solvable, but makes it undecidable for software? I guess it has to boil down to the difference between ...
57 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 ...
215 views

### Determining set of states that satisfy a CTL formulae

I'm trying to understand CTL formulae, and until now I've understood everything (or at least I thought I did). I have the following Kripke strucure: Now given the following CTL formulae ...
17 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 ...
57 views

### How are safety/liveness languages defined on the set of finite or infinite words? [closed]

Let $Σ$ be an alphabet (e.g., the powerset of atomic propositions coming from some Kripke structure, though such details are irrelevant here). For infinite words, a language $P\subseteq Σ^ω$ is ...
22 views

92 views

### Can QBF encode #QBF?

In another question Initializing non-deterministic variables in QBF, I was interested about translating assertion-based pseudocode to QBF in order to have an exponentially more compact encoding ...
85 views

### Initializing non-deterministic variables in QBF

I'm trying to translate the following pseudocode to QBF. The integers are encoded as simple fixed-width bitvectors, and the entire procedure runs in polynomial space ensuring QBF has enough ...
932 views

### What does least fix point and greatest fix point mean in Safety games

In safety games there are these mathematical notation about greatest fix points and least fix points but I don't get it. How would we describe them plain English without mathematical symbols.
403 views

### Difference between equivalence and implication

In terms of CTL formulae, what is the difference between equivalence and implication? (prop = some proposition, && = conjunction, AG = CTL syntax for "globally holds") E.g. AG (prop1 &&...
53 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 (...
116 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.
72 views

### Defining a new (informal) operator in CTL

If you were given a "new operator" Wh and a formula a Wh b meaning that a holds for at least as long as b does (in all executions). How would you define this operator in CTL? This is an exercise ...
275 views

### applying CTL/LTL model-checking on some system

I apologies if my title is vague, I'm trying to apply CTL/LTL model-checking on some system written in java, however, I still don't understand how to reach a result using either of the approaches ...
98 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
92 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$ ...
77 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 (...
88 views

### Given two formulae E[G F p] (which is CTL*) and EG EF p ( which is a CTL) with a Model prove that they are not equivalent

I am trying to prove they are not equivalent , a model which satisfies the fist one but not the second since I think EG EF p is stronger than E[GF p],any leads would be helpful. Thanks.
35 views

### Finding Models for a sequent

I am trying to generate models for the following sequent. $$\exists x \exists y \forall z (z = x \lor z = y)$$ What I have come up with is this. $$A= \{0,1\}$$ So in this model, for all the values ...
450 views

### How to prove LTL-formulas true for all paths?

I'm quoting a question from my homework which I don't understand its wording. Also, I'm not looking for an answer for my problem, I just want to be pointed at some articles/tutorials/reading/tips to ...
313 views

### Given a set of LTL formulas, on which states does the Kripke structure hold? [closed]

I'm currently learning about LTL and CTL formulas and to get a better understanding I try to manually interpret the formulas over a given Kripke structure. Since I'm not 100% sure if my results are ...
55 views

### A linear temporal property that represents this (basic) execution?

A question gives me a set of atomic propositions AP = {a, b, c}and asks me to give a linear temporal property that represents all executions over AP such that: (1) ...
121 views

### Defining a new operator in CTL

Lets consider a new operator $B$ where $a B b$ means "in every execution, if $b$ holds some time, then $a$ does so before it" and we're asked to define it in CTL. My working: the system can only ...
84 views

This question is related to formal model checking theory, but I cannot find a tag for it. Let $P_{safe}$ be a safety property. $BadPref(P_{safe})$ is the set of bad prefixes for $P_{safe}$ A Safety ...
165 views

### Determining which states in a transition system satisfy a specific CTL formula [closed]

Trying to answer the following question: However, my answer is that only one of these states satisfy the TS (which is for sure wrong since the next part of this question asks to remove states that ...