Skip to main content

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
0 votes
0 answers
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 ...
revision's user avatar
0 votes
0 answers
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 ...
revision's user avatar
0 votes
0 answers
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 ...
revision's user avatar
0 votes
0 answers
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 ...
revision's user avatar
0 votes
0 answers
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 ...
revision's user avatar
2 votes
1 answer
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 ...
revision's user avatar
0 votes
1 answer
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 ...
sadcat_1's user avatar
  • 241
0 votes
2 answers
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 ...
cozen's user avatar
  • 3
3 votes
0 answers
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 ...
Senmorta's user avatar
0 votes
0 answers
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 ...
programonkey's user avatar
2 votes
1 answer
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 ...
davinci_07's user avatar
0 votes
1 answer
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 (...
Jahid Chowdhury Choton's user avatar
0 votes
1 answer
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 ...
40er's user avatar
  • 3
2 votes
1 answer
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!
amhineoni's user avatar
1 vote
1 answer
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
amhineoni's user avatar
4 votes
0 answers
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 ...
Mcgfbtl's user avatar
  • 41
3 votes
1 answer
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 ...
cherrywoods's user avatar
0 votes
1 answer
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 ...
TheDudeWithTheBeard's user avatar
0 votes
1 answer
34 views

$Sat(EG^2\alpha)$ as a fixpoint of an operator

Currently I am studying CTL model checking. I found this exercise: Consider the CTL formula $EG^2(\alpha)$ which means that there exists a path that satisfies $\alpha$ at every even position. Define $...
user avatar
2 votes
1 answer
127 views

Given LTL formulas $m$ and $p$, is there a tool that can check whether $m \models p$ does hold?

To the best of my understanding, $m \models p$ asks whether the LTL formula $p$ satisfies the LTL formula $m$. In other words, $m \to p$ is a tautology. Here are some examples of where $m \models p$ ...
Meowth8743's user avatar
2 votes
0 answers
54 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 ...
Grisu47's user avatar
  • 121
0 votes
0 answers
53 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 ...
Aman Jha's user avatar
1 vote
1 answer
77 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, ...
twinrix's user avatar
  • 13
0 votes
0 answers
22 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 ...
Alex's user avatar
  • 101
1 vote
2 answers
183 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 ...
Elahe's user avatar
  • 111
1 vote
0 answers
31 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 ...
Lance's user avatar
  • 2,243
3 votes
2 answers
1k 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 ...
Lance's user avatar
  • 2,243
2 votes
1 answer
63 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 ...
MuchToLearn's user avatar
2 votes
2 answers
69 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 ...
ahelwer's user avatar
  • 209
4 votes
1 answer
66 views

Algorithm for computing $Pr[s \vDash C \bigcup^{\geq n} B]$ for probabilistic verification

I'm having some difficulty trying to come up with an algorithm for computing $Pr[s \vDash C ~\bigcup^{\geq n} B]$ given a finite Markov chain where $S$ is the set of states, $s \in S$, $B,C \subseteq ...
enigma's user avatar
  • 41
2 votes
1 answer
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 ...
ahelwer's user avatar
  • 209
0 votes
1 answer
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
AleWereWolf's user avatar
2 votes
1 answer
490 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\...
AleWereWolf's user avatar
4 votes
1 answer
153 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? ...
Ayrat's user avatar
  • 1,075
5 votes
1 answer
153 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 ...
Tobia Tesan's user avatar
2 votes
2 answers
1k views

Negation of the semantics of the Until operator in LTL

I have been looking at the Until operator and the release operator and when introduced to the release operator it was suggested that it is equivalent to: $\phi R \psi \equiv \neg(\neg\phi U \neg \psi)...
Jack's user avatar
  • 23
2 votes
2 answers
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 ...
Lance's user avatar
  • 2,243
1 vote
2 answers
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 ...
asdf's user avatar
  • 237
0 votes
1 answer
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$ ...
Cilenco's user avatar
  • 415
1 vote
1 answer
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 ...
Bowen Peng's user avatar
2 votes
1 answer
202 views

How to prove a LTL formula correct in a specific model?

I have been learning Verification by model checking recently and I get the following question: $Whether\ the\ LTL\ formula\ M, q_3\ \models (X\ \lnot a) \rightarrow (F\ G\ \lnot a)\ is\ established\ ...
Bowen Peng's user avatar
2 votes
1 answer
340 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 ...
tenepolis's user avatar
  • 133
2 votes
2 answers
125 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 ...
hengxin's user avatar
  • 9,561
0 votes
1 answer
281 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 (...
hengxin's user avatar
  • 9,561
1 vote
0 answers
40 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: ...
Lance's user avatar
  • 2,243
2 votes
1 answer
492 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, ...
Lance's user avatar
  • 2,243
3 votes
2 answers
164 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 ...
Lance's user avatar
  • 2,243
3 votes
1 answer
386 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 ...
nrofis's user avatar
  • 198
8 votes
1 answer
718 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 ...
hengxin's user avatar
  • 9,561
1 vote
0 answers
111 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 $ ...
Amir-Mousavi's user avatar