Fragestunde - Latest question feedhttp://fragestunde.fachschaft.cs.uni-kl.de/Fragen/Fragestunde der Fachschaft Informatik, Universität KaiserslauterndeSun, 05 Nov 2017 10:14:34 +0100VRS Exam WS17/18http://fragestunde.fachschaft.cs.uni-kl.de/Frage/342/vrs-exam-ws1718/I'm not sure if this is an appropriate place to ask, please correct me if I'm wrong.
I would like to know whether the exam is offered in this semester (WS17/18). And if so, what is the date (at least approximately).etherealynSun, 05 Nov 2017 10:14:34 +0100http://fragestunde.fachschaft.cs.uni-kl.de/Frage/342/Simplex Algorithmhttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/336/simplex-algorithm/There's one thing that I could not understand in Simplex is that which element pivots with which element.
I tried all the variables that I could pivot, and I got different answers (yeah, this could be obvious). However, the number of iterations to do the problem increases.
How do I know if have chosen the correct variable to pivot?
y0 := -1 x0 + 2 x1
y1 := -2 x0 + 1 x1
y2 := 1 x0 + 2 x1
-------------------------------------------------------
-oo <= x0 := 0 <= +oo
-oo <= x1 := 0 <= +oo
-oo <= y0 := 0 <= -3
-oo <= y1 := 0 <= 1
4 <= y2 := 0 <= +oo
=======================================================
pivoting x0 with y0 to set y0 := -3
=======================================================
x0 := -1 y0 + 2 x1
y1 := 2 y0 + -3 x1
y2 := -1 y0 + 4 x1
-------------------------------------------------------
-oo <= x0 := 3 <= +oo
-oo <= x1 := 0 <= +oo
-oo <= y0 := -3 <= -3
-oo <= y1 := -6 <= 1
4 <= y2 := 3 <= +oo
In this problem, when I tried to pivot y0 with y1, I got the answer in that iteration. But when I chose to pivot x1 with y1, I had to do one extra step.
blackmambaSat, 26 Aug 2017 01:29:37 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/336/Correct Counterexamples for formulahttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/333/correct-counterexamples-for-formula/ Hey there,
Like in Problem 7 of the last exam (2.2017) I can follow the given solution, but I am not sure if mine is also correct.
Can someone just check them and give maybe short comments? Would the explanation below be sufficient to get the points in the exam?
![image](https://preview.ibb.co/jsNLj5/IMG_20170825_184121.jpg)
**a)**
s1 is satisfied, because on all paths Ga or F!a holds
s2 is not satisfied, because the path 0(2)^w does not hold, since Ga is false and !a is also false in the initial state.
**b)**
[$\phi$ SU $\psi$] is only true, if we have $\phi$*$\psi$, which means, that somewhere $\psi$ must hold.
[$\phi$ WU $\psi$] on the other side is also true, if we have only $\phi$.
Therefore s1 is not satisfied, because b never holds.The same is true for s2 except we have GFa here and in state 1 a holds indeed infinity often. So s2 is satisfied
**c)**
S1 is satisfied, because IF at some time t a holds, in t+1 b must hold.
S2 is not satisfied, because in the next Step (which is one after the initial state) a has to hold if and only if b holds finally. But we are in an endless loop of b, so a cannot hold. The right example doesn't show this, since in the next step a holds and then we reach the b-loop.
**d)**
S2 is satisfied, because on all paths (we obviously have only one path) infinity often !b holds.
S1 is not satisfied, because there is no path, where after one step and some time finally !b holds always.
**e)**
b never holds, so according to my understanding above [c SU b] never becomes true. This leads to A[ false SU a] which should be false as well. Therefore S2 is not satisfied. (Would it be satisfied, if the initial state is empty, which means false? Then [false SU c] would hold).
S1 is satisfied, because we have a sub-path (initial state) with only one c, which satisfies [c WU b] and then reach a.
In e) I am not 100% sure..
Thanks in advance for help.tdFri, 25 Aug 2017 19:35:08 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/333/2012.03.19 Task 6 c solutionshttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/327/20120319-task-6-c-solutions/ Hi there,
if these two automatons are different, how can i transofrm the acceptance condition of A 1 to Fa ∨ Fq ?
–
A
1
=A
∃
(V,
φ
I
,
φ
R
,Fa
∨
Gb)
–
A
2
= A
∃
(V,
φ
I
∧
q,
φ
R
∧
b
∧
q
∧
q
ʹ
, Fa
∨
Fq) JonasFri, 25 Aug 2017 15:28:54 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/327/Propositional formula to RMNF conversionhttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/328/propositional-formula-to-rmnf-conversion/The method described in the lecture for conversion of a propositional formula to RMNF sometimes requires a lot of transformations (or I'm being unfortunate enough to apply rules in a wrong order). For example, in the latest exercise sheet for exam preparation I found myself to be able to transform 1.c to RMNF quite fast while 2.c took a lot of time to complete.
Is there a quicker way to convert a propositional formula to RMNF? etherealynFri, 25 Aug 2017 15:31:18 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/328/Linear clause formhttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/324/linear-clause-form/as an answer can I just write {!a, !c}, {!d, b} as is written in the solution of
question 1_a of exam of 2015.10.15?
![Bildbeschreibung](/upfiles/1503655947778695.png)arsinuxFri, 25 Aug 2017 12:14:14 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/324/CTL*/CTL/LTL questionhttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/320/ctlctlltl-question/It seems to me that the solution provided here is wrong, because I think the solution satisfies both formulas. Would you please prove me wrong if I am mistaken? This does not mean that I am claiming that the formulas are equivalent. So please provide another counter example if the one here is wrong, and if it is correct please explain why.
![Bildbeschreibung](/upfiles/1503503218988509.png)arsinuxWed, 23 Aug 2017 17:51:28 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/320/cheat sheet -Parallel Computinghttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/316/cheat-sheet-parallel-computing/ > are we allowed to take cheat sheet for
> Parallel Computing exam?
if anybody
> has cheat share for the same please
> share,
ppWed, 23 Aug 2017 13:51:38 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/316/Omega Automata language translationhttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/307/omega-automata-language-translation/ I am having trouble doing translations for finite many subwords:
α contains only finitely many subwords aa
α contains only finitely many subwords a!a and !aa
blackmambaTue, 22 Aug 2017 21:26:56 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/307/Does the represented Kripke distinguish the difference between the formulas?http://fragestunde.fachschaft.cs.uni-kl.de/Frage/288/does-the-represented-kripke-distinguish-the-difference-between-the-formulas/![Bildbeschreibung](/upfiles/15034116346358254.bmp) arsinuxTue, 22 Aug 2017 16:22:06 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/288/# 2013.10.07 : Question 6_ehttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/298/20131007-question-6_e/ Is this answer really sufficient?
![Bildbeschreibung](/upfiles/15034201224507346.png)arsinuxTue, 22 Aug 2017 18:42:24 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/298/Exists Algorithmhttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/305/exists-algorithm/ So, I need to clear some basics for Exists Algorithm.
This is what I know so far.
∀x1 ∀x2. ϕ
e becomes x1 & x2.
Then I will negate the ϕ (!(ϕ)) as the algorithm is for Exists.
Do we also have to change the Apply parameter from OR to AND?blackmambaTue, 22 Aug 2017 21:11:09 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/305/# 2016.09.06 : Question6_bhttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/296/20160906-question6_b/How the red signed part (in the picture) has been inferred?
In the alt solution part : if 'a' hold in initial states, how can we solve it?
![Bildbeschreibung](/upfiles/15034186766007246.png) arsinuxTue, 22 Aug 2017 18:19:12 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/296/# 2013.10.07 : Question 6_ahttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/297/20131007-question-6_a/ What is this Q2:{} ? Should we draw it?
There is no transition like that in the related automaton.SiavashTue, 22 Aug 2017 18:32:22 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/297/# 2016.09.06 : Question4_ahttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/294/20160906-question4_a/As I checked with global model checking it holds for all initial states (so it holds for s2), but in the solution (for local model checking) it doesn't hold.
I have two other question in local/ global model checking :
1. should we eliminate the states without successor or the ones which do not have an infinite path?
2. By the way here in this question we can reach to state s8 in one step or to state s1
in two steps which in both states "c | a" holds. As "si |= <>x" results in all OR of successor states of si, then by local model checking (K, s2) |= S1![Bildbeschreibung](/upfiles/1503418004618853.png)arsinuxTue, 22 Aug 2017 18:07:02 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/294/# 2016.02.17 prob8 . part d :http://fragestunde.fachschaft.cs.uni-kl.de/Frage/285/20160217-prob8-part-d/AX(a -> Fb) _ AX(a -> AFb)
isn't it != ? (look at the kripke in attached pic)
I think the attached kripke satisfies the first formula but not the second one.
![Bildbeschreibung](/upfiles/1503410611227154.bmp)arsinuxTue, 22 Aug 2017 16:07:00 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/285/Temporal Logichttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/290/temporal-logic/Does FGXa =? FGa ?
Does GFXa =? GFa ?
arsinuxTue, 22 Aug 2017 16:36:29 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/290/Temporal Logichttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/287/temporal-logic/ Can we say XGF p = GFX p ?arsinuxTue, 22 Aug 2017 16:16:03 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/287/Cheat Sheet Preparationhttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/270/cheat-sheet-preparation/Can someone please give an idea how to prepare the cheat sheet effectively. Online Tools / Softwares.
Can I get the digital version of the lecture slides so that I can copy paste?
Can you please share the LaTex edition of the cheat sheet, so that I can edit upon that.SRFri, 18 Aug 2017 15:21:21 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/270/Compute the set of states from which the states satisfy b<->(c->b) can be reached symbolicallyhttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/276/compute-the-set-of-states-from-which-the-states-satisfy-b-c-b-can-be-reached-symbolically/ What is the meaning of this statement. what I have to find for this kind of questions in KRIPKE structure where Initital state φI= !(a->c), φR=!((next(c)<->c)|!a|next(b)).herleSat, 19 Aug 2017 19:54:26 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/276/LTL / CTL querieshttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/275/ltl-ctl-queries/How are these derived?
([!a W b] & Fb) -> [!a SW b]
G(a&b) -> FGb
GFa -> Fa
blackmambaSat, 19 Aug 2017 18:54:12 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/275/Basic difference between CTL/LTL/CTL*http://fragestunde.fachschaft.cs.uni-kl.de/Frage/264/basic-difference-between-ctlltlctl/As far as I understand LTL has path quantifiers only - A,E, [a U b], [a W b], [a B b]
CTL has path quantifiers followed by state quantifiers - AFa
And CTL* has no restriction.
How would I know if the formula is both CTL and LTL? How do I distinguish? What is the basic difference that I need to remember to distinguish between LTL, CTL?
Also, why is this `E[(¬a) W b]` a CTL and not LTL?
Can you please explain all the three types with suitable example?blackmambaThu, 17 Aug 2017 12:36:43 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/264/CTL*/CTL/LTL/Automatahttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/262/ctlctlltlautomata/ First when we translate from LTL formula to Automata most of the examples in the exams first simplify the LTL formula than apply the formulas given from the lecture. Is this necessary or can we apply directly the given LTL to Automata formulas. If not, can you please describe which approach I should follow for the simplification.
For the translation of CTL* to CTL also in most of the cases there is a translation using some formula that is equivalent to the given formula but I think that this is derived based on logic and not by using the formulas given in the lecture. In this kind of approach how should we try to look for the equivalent formulas if we cannot derive them using the formulas given in the lecture. vrs123Wed, 16 Aug 2017 11:30:34 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/262/Davis-Putnam Procedurehttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/229/davis-putnam-procedure/ I do not understand the Davis-Putnam Procedure.
Here is the question:
{{a}, {b, !d, !a}, {c, !d, !b}, {d, c, a, !b}, {d, c, b}, {c, !d, !b}, {d, c, !b, !a}, {c, a, !b}}. Name the literals that need to be satisfied according to Unit-Propagation
{{a}, {b, !d, !a}, {c, !d, !b}, {d, c, a, !b}, {d, c, b}, {c, !d, !b}, {d, c, !b, !a}, {c, a, !b}}.Name the literals that need to be satisfied according to Pure-Literal-Rule
Can anyone explain this in detail?blackmambaSun, 06 Aug 2017 12:33:35 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/229/Simulation and Bisimulationhttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/257/simulation-and-bisimulation/If K1 is over (a,b,c) and K2 is over (a,b).
Suppose there is a state in K1 which has label c (S1), and there is a state in K2 which has label {} (Q2).
We take the intersection of all the state labels from K1 and (a,b){which is K2}.
Suppose we get the result as {} (empty) for this intersection: `S1 ∩ {a,b} ({c} ∩ {a,b})`.
Now, when we have to do SIM1 for this state, do we consider (S1,Q1) in SIM1?blackmambaMon, 14 Aug 2017 18:42:16 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/257/CTL to mu-calulus conversionhttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/252/ctl-to-mu-calulus-conversion/ How to know when to use mu.x and when to use nu.x while converting CTL to mu-calculus. I know that for mu.x we start with empty set and for nu.x we start with all the sets but still things are not that clear for me. srishMon, 14 Aug 2017 09:57:06 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/252/How to convert from RMNF to DNF/CNF?http://fragestunde.fachschaft.cs.uni-kl.de/Frage/248/how-to-convert-from-rmnf-to-dnfcnf/ I have an RMNF, for example - `(a ⊕ b ⊕ a & b)`
How can I convert it to CNF/DNF?blackmambaWed, 09 Aug 2017 17:39:56 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/248/Conflict in Global Model Checking on Persistence and the definitionhttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/237/conflict-in-global-model-checking-on-persistence-and-the-definition/ I gave this as an entry to Global Model Checking tool
vars a,b;
init 0,5,7;
labels 0:b; 1:; 2:a,b; 3:a; 4:b; 5:; 6:a,b; 7:a,b;
transitions 0->1; 1->3; 2->0; 2->1; 2->5; 3->4; 3->6; 4->6; 5->2; 5->6; 6->3; 6->7; 7->4;
and I wanted to check Persistence property(`mu y.(nu x. (a & <>x) | <>y) ;`) on it. The result says `Property mu y:bool. (nu x:bool. (a & <> x) | <> y) holds in states {s0;s1;s2;s3;s4;s5;s6;s7} ⊇ {s0;s5;s7} = k.init. Hence, the structure satisfies the property.`, but it seems to me that the result is in a conflict with the definition of Persistence I know, which is "It is true in a state if, there is an infinite path from that state that *phi* sometimes holds and sometimes doesn't, but eventually it always holds". The conflict that I see is that it can go to a state like s4 which is outside of s3-s6 loop. So it doesn't seem to be "eventually it **always** holds".arsinuxTue, 08 Aug 2017 17:40:34 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/237/Propositional Logic CNFhttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/230/propositional-logic-cnf/ How can I compute this in a faster way?
d<->a<->b
I want to know if I can directly apply any formulas here to reduce it to CNF. Right now it takes me much time to compute it.
blackmambaSun, 06 Aug 2017 13:25:56 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/230/BDDs: Restrict Algorithmushttp://fragestunde.fachschaft.cs.uni-kl.de/Frage/126/bdds-restrict-algorithmus/Hallo,
Ich verstehe den Restrict-Algorithmus für BDDs nicht. Der Apply Algorithmus ist kein Problem, aber der Restrict Algorithmus wurde irgendwie nur sehr knapp behandelt. Hätte jemand eine Erklärung und ein paar Beispiele?
LG und dankeKejMon, 25 Aug 2014 17:20:18 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/126/