# Tagged Questions

The tag has no usage guidance.

7 views

### How would you construct a proof that the simulation relation is transitive?

I am studying for an exam on model checking and one of the questions that appears in old exams is about Kripke structures, simulations etc.: problem statement (S = set of states; R = transition ...
71 views

### Validity of $F \supset \Box F$

I started to study propositional modal logic and Kripke semantics. I learned that for any Kripke interpration $\mathcal{M}$, we have that, if $\mathcal{M} \models A$ then $\mathcal{M} \models \Box A$. ...
64 views

### Properties of transitive modal frames

I am working through Fitting and Mendelsohn's First Order Modal Logic and have come across the following exercise: Prove that a frame $\langle \mathcal{G}, \mathcal{R} \rangle$ is transitive if ...
33 views

### Persistency on formulas in Kripke models

Let $(W,R,f)$ a Kripke model. I have some trouble proving that the persistency property holds for formulas i.e if $wRw'$ and $w \Vdash \phi$ then $w' \Vdash \phi$ , mainly due to the forcing ...
41 views

### Conditions for total orders in temporal logic

Let $(T,>)$ be a frame of minimal temporal logic, i.e. a frame as defined in Kripke semantics where the relation is a partial order relation $>$ defined on the set $T$ of worlds, called instants....
70 views

### Symmetric relations and $\varphi\rightarrow\square\diamond\varphi$

I read that the schema $$\varphi\rightarrow\square\diamond\varphi$$ corresponds to the symmetric property (D. Palladino, C. Palladino, Logiche non classiche, 'non-classical logics', 2007) of the ...
77 views

### Euclidean relations and $\diamond P\rightarrow\square\diamond P$

I read* that the formula $$\diamond \varphi\rightarrow\square\diamond\varphi$$is valid in a structure $(W,R)$, intended as in Kripke semantics, -i.e. that it is true for any interpretation $I$ and in ...
103 views

### Logical consequence in all structures in Kripke semantics

I read* the following definition of logical consequence in all structures within Kripke semantics:$$X\models A\iff\text{ for every } (W,R),\text{ if }(W,R)\models X,\text{ then }(W,R)\models A$$ \...
64 views

### what does the “fixed point” in fixpoint algorithms refer to?

I was reading the following powerpoint here to remember something I studied a long time ago. http://www.cs.cmu.edu/~emc/15-820A/reading/lecture_1.pdf the 12th slide is labeled fixpoint algorithms, ...
129 views

### Proving the non-derivability of formula using the of the kripke model

I try proving the non-derivability of $(p\to q) \to \lnot p \lor q$, using the of the kripke model. I tried using different combinations of $Wi$, but I get fail.
84 views