9
votes
Accepted
How does TLC check liveness properties?
Presumably it can check any "liveness" property that that can be formulated in LTL. A "liveness" property is typically described as a property stating that "something good eventually happens". This is ...
8
votes
Accepted
Programming language semantics prototyping tool
Although there are frameworks created specifically for the purpose of prototyping programming languages (including their semantics, type systems, evaluation, as well as checking properties about them),...
- 540
5
votes
Accepted
What exactly is Symbolic Model Checking?
Symbolic Model Checking is Model Checking that works on symbolic states. That is, they encode the states into symbolic representations, typically Ordered Binary Decision Diagrams (OBDDs).
The ...
- 2,163
5
votes
Accepted
Is model checking PSpace-hard *in formula size*?
You are certainly right that the level of rigor found in old papers making such claims can be a bit low at times when viewed from today's perspective.
The claim is correct anyway, even if it does not ...
- 2,722
4
votes
Accepted
The importance of the language semantics for code generation and frameworks for code generation in model-driven development
In general when we talk about code generation (or model-to-model transformation in general), clearly defined semantics is quite important, since such transformations usually make sense when both the ...
- 540
4
votes
Accepted
How do you correctly write this sentence as a CTL formula?
You can learn a lot about CTL at Wikipedia page.
The sentence you need to write, expressed more closely in the vocabulary of CTL operators, would be
Along all paths starting from current state, it ...
- 1,171
4
votes
Accepted
How to express the existence of winning strategy of the starter of a game in temporal logic?
I don't think it's possible in CTL nor LTL to model two competing players.
You would probably need ATL (Alternating-time Temporal Logic). In ATL, the formula $\langle\langle A \rangle\rangle \phi$ ...
- 15k
4
votes
Accepted
CTL* query evaluation order
Your interpretation of the $G$ modality is incorrect; it does not inherently talk about all paths. In particular, the example you give specifies that there is a path such that from some point on, all ...
- 2,178
4
votes
Accepted
What's the definition of ACTL?
ACTL is the universal fragment of CTL.
Thus, existential path quantification is not allowed.
So a path formula is of the form $AF\psi$, $AG\psi$, or $AX\psi$ (or a conjunction or disjunction of path ...
- 17k
4
votes
Accepted
What exactly state is in Model Checking
My vote is on (4) from an intuition point of view.
I just started learning this recently so take this with a grain of salt but as mentioned by D.W. the set of states can be anything you want. It is ...
- 178
4
votes
What goes into proving two complicated programs are equivalent?
One could write an entire book surveying techniques of proving program equivalence. This answer is just as a very short starting point:
Theoretically, if you think about your programs as Turing ...
- 17k
4
votes
Accepted
First-order model checking is not fixed parameter tractable on general graphs
For a fixed $k$, existence of a $k$-clique can be represented as a first order model formula: $\exists u_1 \dots u_k, (\bigwedge_{i < j} u_i \neq u_j ) \land (\bigwedge_{i < j} (u_i,u_j) \in E)$....
- 2,205
3
votes
Accepted
How to define the Atomic Propositions in Model Checking
Formal verification often involves at least three steps:
Make a formal model of the real-world system. (The formal model might be a state-transition graph or automaton, for example.)
Write down a ...
D.W.♦
- 154k
3
votes
How to prove a side effect in a function
It depends on how you model the system and what proof approach you're using. For early versions of Hoare Logic, there isn't really any notion of "scope", so there's absolutely nothing special you need ...
3
votes
Accepted
How to prove a side effect in a function
If the function has two outputs, a standard way to represent this is as a function $f: A \to (B \times C)$, i.e., $f$ outputs a pair of an AST and a symbol table.
If the function updates an existing ...
D.W.♦
- 154k
3
votes
Accepted
Abstract Interpretation: Connection between soundness relation and a Galois connection
It appears like I have simply misunderstood the expression: $\langle c, d\rangle \in \sigma \stackrel{def}{=} \alpha(c) \sqsubseteq_{\mathcal{D}} d \Leftrightarrow c \subseteq_{\mathcal{C}} \gamma(d)$....
- 161
2
votes
Accepted
What's a side-effect free expression in Timed Automata?
Well, I typed side-effect in Google, then I chose anser number 4: Side effect (computer science)
The first sentence states:
In computer science, a function or expression is said to have a side ...
- 19.4k
2
votes
LTL properties in bounded model checking via assertions
The property "always eventually main terminates" should be expressible and verifiable in a bounded model checker. For such properties, the model checker would either verify the property or find a "...
- 540
2
votes
Modeling a sequential circuit as a transition system
To build a transition system from a sequential circuit, in general, one needs to define three components:
the states of the transition system, which are all possible combinations of
values of your ...
- 540
2
votes
How to verify a property about a certain order of events in TCTL / UPPAAL?
Under the assumption that your property can be interpreted in an intuitive way, as it is written, it seems that you can formulate it both in LTL, as:
...
- 540
2
votes
Accepted
What the State is, and Where it comes from, when Generating Reachability Graphs
Timed automaton case: Here, a state is typically composed of the current location and the values of all clock variables. Thus, timed automata induce transition systems with an infinite number of ...
- 2,722
2
votes
Acceptance conditions when translating LTL to Büchi automaton?
I will start with the last question and then come to the question at the top of your post.
The construction assumes that the LTL formula is given in negation normal form, so that no temporal operator ...
- 2,722
2
votes
Accepted
LTL to GBA versus LTL to BA
There is no precise answer to this.
The smallest GBA for a given language is never larger than the smallest BA for a given language, simply by the fact that BAs are a special case of GBAs.
It is easy ...
- 2,722
2
votes
What exactly state is in Model Checking
A Kripke structure is a mathematical formalism. Formally, a state in a Kripke structure is just a piece of mathematics; it is an element of the set $S$. It's up to us what interpretation we put on ...
D.W.♦
- 154k
2
votes
Accepted
Least fix point of CTL formula
They actually start by proving that $[[E(\varphi U\psi)]]=\bigcup\limits_{k\ge 1}G^k(\emptyset)$.
You can see (or prove by induction for the general case) that repeated applications of $G$ starting ...
- 13.3k
2
votes
(Generally) How to specify asynchronous action with side effects using logic equations
One way to model your example is through program graphs. (See chapter 2 in Principles of Model Checking.) What you can do is model all() as one program, which ...
- 116
2
votes
Accepted
Negation of the semantics of the Until operator in LTL
First, note that you did not really get the "first part the the expression correct". The first formula is, roughly, of the form
$$
\forall i, (p(i) \lor q(i))
$$
while the second one is of the form
$$...
- 14.4k
2
votes
Definition of liveness property in model checking
I'm not sure where the particular liveness definition you wrote comes from, but the definition given in Defining Liveness (Schneider, Alpern, 1985) is as follows.
A property $P$ is a liveness property ...
2
votes
Accepted
What goes into proving two complicated programs are equivalent?
Formal analysis today is usually done on module or unit level. Unfortunately I'm not aware of a common metric which allows to predict if a formal analysis will be possible. Only structurally very ...
- 146
2
votes
Accepted
Given LTL formulas $m$ and $p$, is there a tool that can check whether $m \models p$ does hold?
Yes, you can use an LTL-to-Büchi-automaton translator for this.
Let's assume that you want to check if $\psi \rightarrow \psi'$ is a valid LTL formula, i.e., every word satisfying the LTL property $\...
- 2,722
Only top scored, non community-wiki answers of a minimum length are eligible