A message from our CEO about the future of Stack Overflow and Stack Exchange. Read now.

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

87 questions
Filter by
Sorted by
Tagged with
367 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 ...
520 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 ...
292 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 ...
911 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.
163 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 ...
169 views

### Find equivalent LTL formula, without Y (Yesterday) operator. How can I handle first state?

The task is to find an equivalent LTL formula for $G(a \Rightarrow Yb)$, which doesn't contain the Y operator. My idea is to search for invalid path patterns with 2 $a$'s in a row, e.g. bbbbaab. ...
108 views

### An algorithm to compute a set of states that satisfy a specific CTL formula

Working through a past exam question and I'm unsure where to start or what form they want the answer in: Define an algorithm that receives as input a finite transition system TS defined over the set ...
299 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 ...
180 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: ...
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) ...
2k 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 ...
208 views

275 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 ...
93 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, ...
172 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 ...
139 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 ...
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}$ ...
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 \$...