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
11 votes
1 answer
215 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, ...
Rodrigo Ribeiro's user avatar
9 votes
2 answers
2k 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. ...
Xpleria's user avatar
  • 193
9 votes
1 answer
237 views

Verify correctness of quantifier elimination, using SAT

Let $x=(x_1,\dots,x_n)$ and $y=(y_1,\dots,y_n)$ be $n$-vectors of boolean variables. I have a boolean predicate $Q(x,y)$ on $x,y$. I give my friend Priscilla $Q(x,y)$. In response, she gives me $P(...
D.W.'s user avatar
  • 159k
8 votes
1 answer
691 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,551
8 votes
4 answers
1k views

How can I decide manually whether two CTL formulae are equivalent?

Assume I have two formulae $\Phi$ and $\Psi$ (over the same set of atomic propositions $AP$) in CTL. We have that $\Phi \equiv \Psi$ iff $Sat_{TS}(\Phi) = Sat_{TS}(\Psi)$ for all transition systems $...
bitmask's user avatar
  • 1,755
6 votes
1 answer
3k views

Product of a Transition System and a Finite Automaton

Dealing with a question that asks me to compute the product of the following transition system and finite automaton. Compute the product between the transition system TS and the finite-word automaton ...
eyes enberg's user avatar
6 votes
1 answer
255 views

Looking for a book that derives and constructs a model checking application

I am teaching myself program verification and am currently learning proof assistants. I have the book Handbook of Practical Logic and Automated Reasoning which gives the proofs necessary for the ...
Guy Coder's user avatar
  • 5,101
6 votes
1 answer
142 views

Why are there two different `until` ($\cup$) semantics in Timed Computation Tree Logic?

Background: In the book of Principles of Model Checking (Christel Baier and Joost-Peter Katoen, MIT Press, 2007), Section 9.2, page 701, the semantics of the until modality is defined over some time-...
hengxin's user avatar
  • 9,551
5 votes
1 answer
389 views

The importance of the language semantics for code generation and frameworks for code generation in model-driven development

I am implementing worflow where the code in industrial programming languages (JavaScript and Java) should be generated from the formal (formally verified) expressions (from ontologies as objects and ...
TomR's user avatar
  • 1,401
5 votes
1 answer
142 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
5 votes
0 answers
189 views

Introduction to bounded model checking that describes model generation

Most of the tutorials I have found on model checking and bounded model checking start with, the model is given as a Kripke Structure M = (S,I,T,L) where S is a set of states, I is a set of initial ...
Jonathan Gallagher's user avatar
4 votes
1 answer
152 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,065
4 votes
1 answer
145 views

Witness for the $EU(\phi_1,\phi_2)$ using BDDs

I wanted ask if you know an algorithm to find the witness for $EU(\phi_1,\phi_2)$ (CTL formula "Exist Until") using BDDs (Binary Decision Diagram). In pratice you should use the fixed point for ...
kafka's user avatar
  • 401
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
4 votes
0 answers
183 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
4 votes
0 answers
51 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 ...
Sujit Kumar Muduli's user avatar
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,223
3 votes
2 answers
159 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,223
3 votes
2 answers
1k views

Modelling a basic sequential circuit as a transition system?

I'm going through Dr Joost-Pieter Katoen's slides and stumbled upon this: For some reason I can't quite make out how the transition system relates to the sequential circuit. If I had a question for ...
eyes enberg's user avatar
3 votes
1 answer
3k 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.
Deyaa's user avatar
  • 33
3 votes
1 answer
150 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 ...
hubsi's user avatar
  • 33
3 votes
1 answer
618 views

What's the definition of ACTL?

I have been looking for the definition of ACTL, but Google has given me very little to go with. So far, I know ACTL is another form of CTL model checking, and CTL includes the following operators: ...
Thang Do's user avatar
  • 209
3 votes
1 answer
85 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
3 votes
1 answer
398 views

Description and semantics of program graphs

I'm working on a question which gives me a program graph and tells me to give a mathematical description of it. I'm aware that a program graph PG is a tuple $(Loc, Act, Effect, \rightarrow, Loc_0, ...
eyes enberg's user avatar
3 votes
1 answer
499 views

Time to construct a GNBA for LTL formula

I have a problem with the proof for constructing a GNBA (generalized nondeterministic Büchi automaton) for a LTL formula: Theorem: For any LTL formula $\varphi$ there exists a GNBA $G_{\varphi}$ ...
kafka's user avatar
  • 401
3 votes
1 answer
385 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
3 votes
1 answer
105 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 ...
Y. Tang's user avatar
  • 33
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
3 votes
0 answers
96 views

Spot the formalism (some kind of process logic)

Consider the following specification technique. A specification consists of a finite set of triples $\langle C, A, C' \rangle$, where $A$ is the name of an action and $C, C'$ are conditions, that is, ...
reinierpost's user avatar
  • 5,519
2 votes
1 answer
612 views

Transition systems that satisfy LTL but not CTL, and vice versa

I am learning about temporal logic and model checking systems. One conceptual exercise that I am struggling with is how to create a transition system which satisfies only one of two given properties, ...
KJ50's user avatar
  • 131
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
2 votes
1 answer
318 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
122 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,551
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,223
2 votes
1 answer
480 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,223
2 votes
1 answer
123 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
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
2 votes
1 answer
429 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
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
1 answer
209 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 ...
Robert P. Goldman's user avatar
2 votes
1 answer
656 views

Modeling a sequential circuit as a transition system

I was asked to model the following sequential circuits C1, C2 as transition systems (i.e. identify the output y function and register functions r1, r2, r3) For C2 there appears to be not input x and ...
jn025's user avatar
  • 123
2 votes
1 answer
462 views

LTL properties in bounded model checking via assertions

Is there a way to check LTL properties in a bounded model checker? As an example, consider a liveness property ($G F p$ - always eventually $p$)? Suppose we have the following trivial program ...
Markus Müller's user avatar
2 votes
1 answer
781 views

What's a side-effect free expression in Timed Automata?

I'm trying to get myself more familiar with Timed Automata theory. At some point I came across the expression "side-effect free" like in the following: A guard is a side-effect free expression that ...
Jim McAdams's user avatar
2 votes
1 answer
246 views

SPIN / Promela Verification [closed]

I have this code here which performs the 'leader election' among a specified number of processes. In Promela, it is written as: ...
Boris Jakovljevic's user avatar
2 votes
1 answer
62 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
1 answer
441 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
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
703 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. ...
Georg Heiler's user avatar
2 votes
1 answer
174 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 ...
user avatar
2 votes
1 answer
978 views

The Interleaved Transition System for 2 Independent and Concurrent Transition Systems

This question is about Model Checking for Software Formal Verification How do you model the joint behavior of 2 independent and concurrent transition systems? Specifically, given the two independent ...
eyeezzi's user avatar
  • 123