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.
100
questions
2
votes
1
answer
21
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!
- 35
1
vote
1
answer
30
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
- 35
0
votes
0
answers
12
views
Is the closure of a Linear Time Property closed under union and intersection?
Defining the closure of a linear time property $P$ to be the set of all infinite traces $x$ such that the set of prefixes of $x$ is a subset of the set of prefixes of $P$, is $closure(P \cup P') = ...
4
votes
0
answers
174
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
2
votes
1
answer
38
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 ...
- 141
0
votes
1
answer
50
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 ...
3
votes
0
answers
34
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 ...
- 2,220
0
votes
1
answer
31
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 $...
- 149
2
votes
1
answer
73
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:
...
- 23
2
votes
0
answers
50
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 ...
- 121
0
votes
0
answers
42
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 ...
- 1
0
votes
1
answer
42
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, ...
- 3
0
votes
0
answers
21
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 ...
- 101
1
vote
2
answers
106
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 ...
- 111
1
vote
0
answers
25
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 ...
- 1,873
2
votes
2
answers
500
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 ...
- 1,873
2
votes
1
answer
37
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 ...
- 168
2
votes
2
answers
60
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 ...
- 145
3
votes
1
answer
57
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 ...
- 31
2
votes
1
answer
317
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 ...
- 145
0
votes
1
answer
205
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
- 21
2
votes
1
answer
163
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\...
- 21
4
votes
1
answer
111
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?
...
- 1,016
5
votes
1
answer
105
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 ...
- 228
2
votes
2
answers
801
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)...
- 23
2
votes
2
answers
62
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 ...
- 1,873
1
vote
2
answers
218
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 ...
- 227
0
votes
1
answer
189
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$ ...
- 365
1
vote
1
answer
148
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
2
votes
1
answer
164
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\ ...
- 135
2
votes
1
answer
232
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 ...
- 133
2
votes
2
answers
105
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 ...
- 9,179
0
votes
1
answer
188
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 (...
- 9,179
1
vote
0
answers
37
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,873
2
votes
1
answer
340
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, ...
- 1,873
2
votes
2
answers
123
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 ...
- 1,873
3
votes
1
answer
297
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 ...
- 198
7
votes
1
answer
503
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 ...
- 9,179
1
vote
0
answers
62
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 $ ...
- 268
1
vote
0
answers
51
views
How to Construct Kripke Structure States from Nested Functions
Say I have these defined functions:
...
- 1,873
1
vote
0
answers
72
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,873
2
votes
0
answers
263
views
Equivalence preserving operator from CTL* to LTL
The question is about an operator that transforms any CTL* formula ${\psi}$ into a (not necessarily equivalent) LTL formula ${A\psi^d}$, where $d$ means syntactically removing all $A,E$ quantifiers ...
1
vote
2
answers
84
views
How to prove a side effect in a function
I asked a question earlier about Saving to the Database, which was very general and about the requirements for a proof when you go through many layers of non-verified systems such as the network and ...
- 1,873
0
votes
1
answer
97
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 (...
- 1,873
2
votes
1
answer
118
views
Acceptance conditions when translating LTL to Büchi automaton?
As an exercise in better understanding, I have been implementing the LTL to Generalized Büchi Automaton translation algorithm of Gerth, et al. (which is also discussed in Clarke, et al., Model ...
3
votes
1
answer
96
views
Why do we have free variables in mu-calculus?
I'm reading the Model Chekcing book of E. M. Clarke and in the chapter about µ-calculus there is an example formula
$$
f = \mu Z. ((q \mathrel{\mathrm{AND}} Y) \mathrel{\mathrm{OR}} \langle a \rangle ...
- 33
2
votes
1
answer
499
views
Explanation of the Gelfond Lifschitz reduct
Can someone explain with a hands on example how the Gelfond Lifschitz reduct works in order to check stable model semantics?
edit
a simple example here - at least as far as I understand the thing. ...
- 131
0
votes
1
answer
149
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
1
answer
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 ...
- 163
0
votes
1
answer
179
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.
- 165