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

90 questions
Filter by
Sorted by
Tagged with
29 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, ...
38 views

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 ... 0answers 16 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 ... 2answers 39 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 ... 2answers 105 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 ... 0answers 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 ... 2answers 89 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 ... 1answer 29 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 ... 2answers 48 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 ... 1answer 128 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 1answer 84 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 ... 1answer 165 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 ... 0answers 59 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 ... 0answers 24 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\... 1answer 85 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\ ... 1answer 60 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? ... 1answer 56 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 ... 2answers 56 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 ... 1answer 352 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)... 2answers 142 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 ... 1answer 119 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 ... 1answer 61 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 ... 1answer 95 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 ... 1answer 107 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 ... 2answers 88 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 ... 1answer 100 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 (... 1answer 325 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 ... 0answers 33 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: ... 2answers 748 views ### What exactly is Symbolic Model Checking? I know that Symbolic Model Checking is state space traversal based on representations of states sets and transition relations as formulas like in CTL using models like Kripke Model. I know the theory. ... 1answer 187 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, ... 1answer 227 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 ... 0answers 52 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 ... 0answers 45 views ### How to Construct Kripke Structure States from Nested Functions Say I have these defined functions: ... 0answers 67 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 ... 0answers 195 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 ... 1answer 56 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 (... 2answers 58 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 ... 1answer 73 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 ... 1answer 99 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. 1answer 322 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. ... 1answer 122 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. 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 ... 1answer 2k views ### What is the difference between a Transition System and a Program Graph? (model checking) [closed] As the above question says. I'm wondering if a transition system is the same as a program graph or they are two different things? Thank you. 0answers 77 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 ... 0answers 128 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: ... 1answer 104 views ### CTL* query evaluation order I'm currently trying to evaluate a CTL* expression and am not sure how to stepwisely evaluate the queries. For example I have EFG p. This means something like 'there is a path where eventually there ... 1answer 170 views ### Programming language semantics prototyping tool Is there any tool for prototyping a programming language semantics and type system and that also allows for some sort of model checking of standard properties, like type soundness? I'm asking this, ... 0answers 46 views ### How the$EX(f)\$ is evaluated in symbolic model checking?

I was reading the symbolic model checking, So there it has mentioned that we can represent the set of states and transition relations of any transition system with the help of ROBDDs. I was trying to ...