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

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 ...


6

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 ...


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

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

It seems to me that "$\Phi≡\Psi$" is equivalent to "Neither $(\Phi ∧ ¬\Psi)$ nor $(\Psi ∧ ¬\Phi)$ is satisfiable". Therefore deciding equivalence is as difficult as deciding satisfiability, since "$\Phi$ satisfiable" is equivalent to "not ($¬\Phi≡\top$)". In this article there is a mention of a an exponential procedure to decide satisfiability in ...


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

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

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

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

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 ...


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

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

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

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

What you describe is symbolic model checking, and it is treated in this set of slides, using reduced ordered BDDs. In a nutshell, you still do the fixpoint iteration, the main issue being how to do the transformation $Q\mapsto \phi_2\vee(\phi_1\wedge EXQ)$ on BDDs. The elementary operations you need are renaming (to replace unprimed by primed variables in $...


3

In general, logical formulae can be thought of as trees; inner nodes are operators and leaves are atomic propositions. Therefore, every formula consists of as many direct subformulae (that is on the first level) as its top-most operator's arity. For example, $\qquad \varphi \land \psi$ has two direct subformulae $\varphi$ and $\psi$. This can be continued ...


3

If you want to prove the identities by hand, I do not know if there are absolutely general techniques. You can start with the axioms and well known identities for CTL and work from there. If you want the answer and worry about having a human readable proof separately, you can use a CTL satisfiability checker like MLSolver.


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 ...


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.


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