Model checking refers to the following problem: given a model of a system, test automatically whether this model meets a given specification.
2
votes
2answers
70 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 ...
0
votes
1answer
24 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 (...
1
vote
0answers
27 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
vote
1answer
28 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, ...
0
votes
0answers
17 views
How to combine Symbolic Model Checking with Symbolic Execution
I have started reading some textbooks and papers on Model Checking, and have run into the closely related but different Symbolic Execution. I have a few open questions on StackOverflow about the "...
2
votes
1answer
44 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 ...
2
votes
1answer
60 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 ...
4
votes
1answer
81 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 ...
1
vote
0answers
17 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 $ ...
1
vote
0answers
22 views
How to Construct Kripke Structure States from Nested Functions
Say I have these defined functions:
...
1
vote
0answers
30 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 ...
2
votes
0answers
97 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
2answers
41 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 ...
0
votes
1answer
29 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 (...
2
votes
1answer
29 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 ...
2
votes
0answers
35 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 ...
0
votes
0answers
27 views
Create a transition system where every sequence has at least twice as many $a$'s than $b$'s
Create a transition system with edges $a$ and $b$ and an initial
state, such that for all possible sequences, you have that: The amount
of $a$'s in the sequence is at least twice as much as the ...
1
vote
1answer
98 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. ...
0
votes
1answer
35 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
1answer
30 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 ...
0
votes
1answer
53 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.
1
vote
0answers
50 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 ...
1
vote
0answers
41 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:
...
3
votes
1answer
72 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 ...
4
votes
0answers
42 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 ...
11
votes
1answer
138 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, ...
1
vote
1answer
163 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 ...
1
vote
0answers
70 views
generic technique to build LTL/CTL formula that satisfy specific inputs to a model
I have an automaton, for example the below automaton and would like to generate a single formula (LTL or CTL, or some other representation) that satisfy exactly the traces provided. e.g.,
$t_1 = i^*...
1
vote
1answer
117 views
How to verify a property about a certain order of events in TCTL / UPPAAL?
I'd like to check if a certain order of events happens if another property holds true using UPPAAL and TCTL.
...
1
vote
1answer
69 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 ...
1
vote
1answer
76 views
Initializing non-deterministic variables in QBF
I'm trying to translate the following pseudocode to QBF. The integers are encoded as simple fixed-width bitvectors, and the entire procedure runs in polynomial space ensuring QBF has enough ...
2
votes
1answer
78 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:
...
0
votes
1answer
231 views
How to prove LTL-formulas true for all paths?
I'm quoting a question from my homework which I don't understand its wording.
Also, I'm not looking for an answer for my problem, I just want to be pointed at some articles/tutorials/reading/tips to ...
5
votes
1answer
108 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 ...
2
votes
1answer
275 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
...
2
votes
1answer
338 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 ...
2
votes
1answer
120 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 ...
0
votes
2answers
406 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.
0
votes
1answer
119 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 ...
1
vote
1answer
121 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.
...
1
vote
1answer
106 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
206 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 ...
2
votes
1answer
152 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
1answer
45 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) ...
5
votes
1answer
1k 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 ...
3
votes
1answer
118 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, ...
3
votes
1answer
497 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 ...
8
votes
2answers
174 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
117 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
70 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 ...
