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 ...
Derek Elkins left SE's user avatar
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),...
ivcha's user avatar
  • 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 ...
Lance's user avatar
  • 2,223
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 ...
DCTLib's user avatar
  • 2,742
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 ...
ivcha's user avatar
  • 540
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 ...
Shaull's user avatar
  • 17.2k
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 ...
Klaus Draeger's user avatar
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 ...
MuchToLearn's user avatar
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 ...
Sandro Lovnički's user avatar
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$ ...
Pål GD's user avatar
  • 16.1k
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 ...
Shaull's user avatar
  • 17.2k
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)$....
pcpthm's user avatar
  • 2,348
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.'s user avatar
  • 159k
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 ...
Derek Elkins left SE's user avatar
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.'s user avatar
  • 159k
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)$....
cherrywoods's user avatar
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 ...
ivcha's user avatar
  • 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: ...
ivcha's user avatar
  • 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 ...
DCTLib's user avatar
  • 2,742
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 ...
DCTLib's user avatar
  • 2,742
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.'s user avatar
  • 159k
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 ...
Ariel's user avatar
  • 13.4k
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 ...
DCTLib's user avatar
  • 2,742
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 ...
J.Svejda's user avatar
  • 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 $$...
chi's user avatar
  • 14.6k
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 ...
William Schultz's user avatar
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 ...
goofy's user avatar
  • 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 $\...
DCTLib's user avatar
  • 2,742
1 vote

Buchi automata in formal software verification

The fastest theoretical algorithm to solve Büchi Games in game graphs is presented in [1] and runs in $O(n^2)$: The algorithm uses a hierarchical decomposition approach. An easier folklore algorithm ...
Alexander Svozil's user avatar
1 vote
Accepted

Model Checking CTL* algorithm

The algorithm is full and correct. If you look back to definition 6.80 in the same book, you will see that the until operator is part of path formulae, which in the CTL* MC algorithm are checked via a ...
J.Svejda's user avatar
  • 116

Only top scored, non community-wiki answers of a minimum length are eligible