9

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 \times Q$) of the product but make mistakes about its transition relation. Below I focus on the transition relation. Definition 4.16 Product of Transition System $...


8

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. That is, the least $X$ such that $X = A\cup(B\cap\circ X)$, and the greatest $X$ such that $X = A\cap(B\cup\circ X)$, respectively. More generally, we are talking ...


8

John Harrison's book is an exception in going all the way from theory to practice and making all the source code available. I think you will find it difficult to find an equivalent book for model checking, but there are a few that achieve a close approximation. Principles of Model Checking by Baier and Katoen contains a lot of examples and pretty detailed ...


8

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), the best choice depends on your particular case and specific needs. Having that said, there are multiple (perhaps not so distinct) alternatives you might ...


5

Technically, LTL and CTL are incomparable in their differentiating power over Kripke structures. So intuitively, it shouldn't be easier to design one or the other. However, most people tend to find it easier to think in linear time. Making sure a certain property holds for all paths is easier than studying a branching-time property. In particular, this is ...


5

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 unintended consequences where an adversary obtains secret authentication tokens or related circumstantial data that could help them contravene the process. A ...


5

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 usually contrasted to a "safety" property which states that "nothing bad ever happens". See e.g. Slide 20 of this SPIN tutorial. Basically, a basic safety ...


5

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 follow from Sistla/Clarke's proof. The reason is that LTL satisfiability checking is also PSPACE-complete. You can see satisfiability checking as a special ...


4

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 $x$ and register $r$ (no output variable $y$) in $\texttt{SC}$. The label of each state in $\texttt{TS}$ consists of all the variables (including the register) ...


4

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 question is what do they do and how do they work. You first have your source code for some application. You then transform your source code into some state-transition ...


4

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,S_1)^\omega$, and it induces a single word: $(\{a\},\{a,b\})^\omega$. Now, this word satisfies $aUb$, since $a$ holds until the secod letter, in which $b$ holds....


4

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 source and the target model semantically match according to some criteria. For example, programmers might describe the behaviour of a program with a formal ...


4

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 formulas). Moreover, you are not allowed a general NOT operator, but rather negations have to be on the atomic propositions (otherwise this fragment would be ...


4

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 states on that path satisfy $p$. As you suspect, for CTL* it is in general not possible to use a simple bottom-up evaluation, as you would for CTL, the reason ...


4

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$ says that agent (or coalition) $A$ can enforce $\phi$ to come about. In your case, $\langle\langle P_1 \rangle\rangle \text{Win}_1$. In modal µ-calculus, it ...


4

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 always has to hold that there exists at least one path where $p$ eventually is true. I think you can take it from there, but comment if you have troubles. hint: ...


3

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 that we specify the "smallest" such set because otherwise you could pick the set of all states, or include arbitrary cycles of $a$-states, etc. Do you see how ...


3

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., $f(x)=x$ where $x$ comes from some infinite set). If $x$ comes from a set with an ordering relation, such as $\leq$ on some kind of numbers, or $\subseteq$ on ...


3

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, g_0)$ where: $Loc$ is a set of locations $Effect: Act \times Eval(Var) \to Eval(Var)$ is the effect function $\rightarrow \subseteq Loc \times Cond(...


3

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 Katoen (The MIT Press). For completeness, I first present the definitions of both transition system and program graph in this book. (Keep the numbering of the ...


3

CTL formulas are always evaluated from the starting state of the Kripke structure. Indeed, CTL stands for computation Tree logic, and the tree in question is the unwinding of the Kripke structure, starting from the initial state. If you want to specify that $EF q$ should hold from every (reachable) state, that can be specified as $AGEFq$, which is still a ...


3

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 propositional logic, that is, $A \leftrightarrow B$ is the same $(A \to B) \land (B \to A)$. But your real question is whether $\mathrm{AG}\,(A \land B)$ is equivalent ...


3

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 symbol table, you could represent this as a function $f : (A \times C) \to (B \times C)$. It takes as an input a pair of a string and a symbol table, and ...


3

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 to do. You simply have a pre-conditions and post-conditions on the global state. For Hoare Logic, types have nothing to do with it. In a bit more detail, in a ...


3

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 an abstract concept. However, it is natural to think of states as being valuations of the variables in the system. For example, we may think of the current state ...


3

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 specification that hopefully captures the real-world requirements. Verify that the formal model of the system meets the specification. Formal methods provides ...


2

The two definitions are equivalent: As you point out, the second one implies the first, as if $\phi$ holds, then clearly $\phi\vee \psi$ holds. Conversely, consider a computation that satisfies the first definition, and assume by way of contradiction that it does not satisfy the second definition. Thus, there exists some time in which $\psi$ holds, and in ...


2

Here are two techniques I've been able to identify: Identify an explicit Skolem function. Suppose Priscilla can identify an explicit function $f$ such that $$\forall x . P(x) \Leftrightarrow Q(x,f(x))$$ holds. Then it follows that Priscilla's claim is correct. This means that Priscilla can help us verify her claim by providing a function $f$ so that the ...


2

I'm pretty sure that you need your system to be designed in Promela, rather than Java. You then input the system in Promela, and the specification in LTL (or CTL) to SPIN, which outputs a C code for a model checker for the specific instance.


2

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 formula does not hold is correct. The formula $A [a U b]$ does not hold on such a path; Wikipedia gives the following definition: $\bigg( (\mathcal{M}, s) \models A[...


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