Model checking refers to the following problem: given a model of a system, test automatically whether this model meets a given specification.

learn more… | top users | synonyms

1
vote
1answer
12 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. ...
0
votes
0answers
11 views

Formalize the following expressions to LTL formula

I'm trying to solve a question that asks me Formalize a sentence from English to LTL formula as follows; ...
0
votes
1answer
41 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 ...
0
votes
1answer
44 views

Given a set of LTL formulas, on which states does the Kripke structure hold?

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 ...
2
votes
1answer
30 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: ...
0
votes
0answers
11 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) ...
3
votes
1answer
55 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 Can't seem to find a good example on how to do this so I sort of just freestyled ...
3
votes
1answer
49 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, ...
2
votes
1answer
25 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 ...
3
votes
1answer
59 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. ...
0
votes
1answer
51 views

Defining a new operator in CTL

Lets consider a new operator $B$ where $a B b$ means "in every execution, if $b$ holds some time, then $a$ does so before it" and we're asked to define it in CTL. My working: the system can only ...
0
votes
1answer
53 views

Defining a new (informal) operator in CTL

If you were given a "new operator" Wh and a formula a Wh b meaning that a holds for at least as long as b does (in all executions). How would you define this operator in CTL? This is an exercise ...
0
votes
1answer
80 views

Applying DFS algorithm to a transition system to find reachable states

Currently working on a past exam question which tells me to compute the product of two transition systems and then use DFS to find the reachable states of the product. I learnt how to compute the ...
0
votes
1answer
46 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.
1
vote
2answers
99 views

Some slight confusion with the UNTIL operator in CTL (e.g. a U b)

I've sketched a very small transition system in paint that I'll use as an example. I want to see if $A(aUb)$ holds for this transition system. From my understanding, this CTL formula is asking if ...
0
votes
1answer
52 views

Given this transition system, for which states are these (very basic) LTL formulas fulfilled?

I missed a lot of lectures for this module due to surgery so I'm trying to teach it to myself now. This is the question I've been working on: First of all, would I be correct in saying that the LTL ...
1
vote
1answer
28 views

Model Checking: hardware vs software

In short: What is the basic difference that allows model checking for hardware to be "easily" solvable, but makes it undecidable for software? I guess it has to boil down to the difference between ...
0
votes
1answer
49 views

Difference between equivalence and implication

In terms of CTL formulae, what is the difference between equivalence and implication? (prop = some proposition, && = conjunction, AG = CTL syntax for "globally holds") E.g. AG (prop1 ...
0
votes
1answer
61 views

Set containment of MinimumBadPrefix and BadPrefix of a Safety Property

This question is related to formal model checking theory, but I cannot find a tag for it. Let $P_{safe}$ be a safety property. $BadPref(P_{safe})$ is the set of bad prefixes for $P_{safe}$ A Safety ...
1
vote
1answer
45 views

Determining set of states that satisfy a CTL formulae

I'm trying to understand CTL formulae, and until now I've understood everything (or at least I thought I did). I have the following Kripke strucure: Now given the following CTL formulae ...
5
votes
0answers
56 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 ...
1
vote
1answer
115 views

Computation tree logic and Kripke structures

Specifications in Kripke structures are verified by Computation tree logic (CTL). However, refering to this Wikipedia article the CTL-operators are relative to a current state. So, when we want to ...
1
vote
1answer
92 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, ...
2
votes
0answers
49 views

Is there any open-source tools for verifying TCTL formulae over timed automata can be imported into my project?

In my project, there is one important step to automatically verify a timed automata with TCTL formulae. I briefly surveyed the tool UPPAAL that provides a GUI to construct a timed automata and to ...
3
votes
1answer
52 views

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

Background: In the book of Principle of Model Checking (Section 9.2, Page 701), the semantics of the until modality is defined over some time-divergent path $\pi ...
2
votes
0answers
120 views

Example of execution fragment of multi-process transition system

Here is a simple transition system of beverage vending machine: The exemplary execution fragments can look like this: Now, imagine we have multi-process TS where processes are identical and ...
8
votes
1answer
129 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 ...
0
votes
1answer
110 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 ...
3
votes
0answers
76 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, ...
3
votes
1answer
91 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 ...
3
votes
1answer
111 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 ...
3
votes
1answer
91 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}$ ...
7
votes
4answers
395 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 ...