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.

Filter by
Sorted by
Tagged with
1
vote
1answer
193 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 ...
1
vote
0answers
12 views

Definition of liveness property in model checking

A property $P$ is simply a set of sequences of states and a certain program is characterized by its set of sequences of states, let's call it $T$. A program is compliant to a specific property P if $T\...
1
vote
0answers
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: ...
1
vote
0answers
41 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
0answers
39 views

How to Construct Kripke Structure States from Nested Functions

Say I have these defined functions: ...
1
vote
0answers
53 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 ...
1
vote
0answers
73 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 ...
1
vote
0answers
90 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: ...
1
vote
0answers
103 views

generic technique to build LTL/CTL formula that satisfy specific inputs to a model

I have an automaton, for example the below automaton and would like to generate a single formula (LTL or CTL, or some other representation) that satisfy exactly the traces provided. e.g., $t_1 = i^*...
1
vote
1answer
85 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 ...
1
vote
1answer
82 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 ...
0
votes
2answers
724 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.
0
votes
1answer
333 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 &&...
0
votes
1answer
43 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 (...
0
votes
1answer
98 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.
0
votes
1answer
71 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 ...
0
votes
1answer
267 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 ...
0
votes
1answer
45 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$ ...
0
votes
1answer
44 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 (...
0
votes
1answer
65 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.
0
votes
1answer
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 ...
0
votes
1answer
394 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 ...
0
votes
1answer
275 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 ...
0
votes
1answer
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) ...
0
votes
1answer
119 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 ...
0
votes
1answer
83 views

Set containment of MinimumBadPrefix and BadPrefix of a Safety Property

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 ...
0
votes
0answers
20 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
0
votes
0answers
13 views

Timed Kripke structures with inequality constraints

I am having problems creating a timed Kripke structure $\mathcal{TK} = \langle S, \mathcal{T}, \rightarrow, L \rangle$ for a system that I have. My system, a timed automaton system (time base $\...
0
votes
1answer
157 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 ...
0
votes
1answer
167 views

Applying DFS algorithm to a transition system to find reachable states

Currently working on a past exam question which tells me to compute the product of two transition systems and then use DFS to find the reachable states of the product. I learnt how to compute the ...
0
votes
1answer
428 views

Given this transition system, for which states are these (very basic) LTL formulas fulfilled?

I missed a lot of lectures for this module due to surgery so I'm trying to teach it to myself now. This is the question I've been working on: First of all, would I be correct in saying that the LTL ...