9 votes
Accepted

Product of a Transition System and a Finite Automaton

In Section 4.2.2 of the book "Principles of Model Checking", there is a definition (Definition 4.16; Page 165) of "Product of Transition System and NFA". You are right about the states (i.e., $S \...
user avatar
  • 9,219
9 votes
Accepted

What does least fix point and greatest fix point mean in Safety games

Probably the most common fixpoint expressions in model checking are things like $\mu X.A\cup(B\cap\circ X)$ and $\nu X.A\cap(B\cup\circ X)$, where $\circ$ is some flavour of "next state" operator. ...
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),...
user avatar
  • 540
7 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 ...
user avatar
6 votes

What exactly is Symbolic Model Checking?

Symbolic model checking can be very useful for verifying the correctness of communications and security protocols. For example: A symbolic model of an OAUTH2 implementation could help check for ...
user avatar
  • 161
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 ...
user avatar
  • 1,911
5 votes
Accepted

What is the difference between a Transition System and a Program Graph? (model checking)

You did not provide any particular resources for neither transition system nor program graph. My answer below is based on the book "Principles of Model Checking" by Christel Baier and Joost-Pieter ...
user avatar
  • 9,219
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 ...
user avatar
  • 2,682
4 votes
Accepted

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

You have some misconception regarding transition systems: The alphabet of the system is $2^P$ for some set $P$, and paths induce words over $2^P$. In the first system, there is a single path: $(S_0,...
user avatar
  • 16.2k
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 ...
user avatar
  • 16.2k
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 ...
user avatar
  • 540
4 votes
Accepted

Modelling a basic sequential circuit as a transition system?

How does the transition system (denoted by $\texttt{TS}$) relate to the sequential circuit (denoted by $\texttt{SC}$)? The states of $\texttt{TS}$ are all possible combinations of values of variable $...
user avatar
  • 9,219
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 ...
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 ...
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$ ...
user avatar
  • 13.3k
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 ...
user avatar
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)$....
user avatar
  • 1,396
3 votes

What does least fix point and greatest fix point mean in Safety games

A fixed point of a function $f$ is a value $x$ such that $f(x)=x$. A function might have no fixed points (e.g., $f(x)=x+1$), a finite number of them (e.g., $f(x)=x^2+x-1$) or infinitely many (e.g., $...
user avatar
3 votes

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

The set of states satisfying $\exists a U b$ is the smallest set $S$ such that $S$ contains all states satisfying $b$, and $S$ contains all states satisfying $a$ which have a successor in $S$ Note ...
user avatar
3 votes
Accepted

Description and semantics of program graphs

Definitions From "Principle of Model Checking" By Joost-Pieter Katoen and Christel baier: A program graph over a set Var of typed variables is a tuple $(Loc, Act, >Effect, \rightarrow, Loc_0, ...
user avatar
  • 530
3 votes
Accepted

Difference between equivalence and implication

First, to answer the question in your question title: the difference between equivalence and implication in CTL formulae is the same as the difference between equivalence and implication in ...
user avatar
  • 1,090
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 ...
user avatar
  • 143k
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 ...
user avatar
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 ...
user avatar
  • 143k
3 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 ...
user avatar
  • 16.2k
2 votes
Accepted

Model Checking: hardware vs software

The statespace explosion problem. More specifically, software often uses unbounded loops, pointers into complex data structures on the heap, and dynamic allocation. Each of these can cause rapid ...
user avatar
  • 143k
2 votes

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

A small addendum to @Shaull's anwswer, which is completely correct: for the output (1), $aaaaaaaaa\ldots$, you suggested (if it were possible in your transition system), your assumption that the ...
user avatar
  • 133
2 votes
Accepted

Defining a new (informal) operator in CTL

You seem to be stuck, so here is the answer: You want $a$ to hold for at least as long as $b$ does. The alphabet consists of $2^{\{a,b\}}=\{\emptyset, \{a\},\{b\},\{a,b\}\}$. Rephrasing the ...
user avatar
  • 16.2k
2 votes
Accepted

SPIN / Promela Verification

For the "all the processes agree about the one elected leader" part: It is a combination (conjunction) of No more than one process can ever be declared to be the leader: $\Box (\textrm{nr} \_ \...
user avatar
  • 9,219
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 ...
user avatar
  • 19.1k

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