Propositional Logic CNFhttp://fragestunde.fachschaft.cs.uni-kl.de/Fragen/Fragestunde der Fachschaft Informatik, Universität KaiserslauterndeThu, 17 Aug 2017 10:03:39 +0200CTL*/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. Wed, 16 Aug 2017 11:30:34 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/262/ctlctlltlautomata/Answer by PS for CTL*/CTL/LTL/Automata http://fragestunde.fachschaft.cs.uni-kl.de/Frage/262/ctlctlltlautomata/?answer=263#post-id-263For the translation from LTL to ω-automata, no preprocessing is required for the procedures discussed in the lecuture. Since these procedures also run in linear time w.r.t. the length of the LTL formula, it is best to not simply the formula given, since you won't save much time and have the risk to do it in a wrong way. So, I would recommend to simply apply the translation procedure as it is.
The (optional) simplification done by the teaching tool on http://es.cs.uni-kl.de/tools/teaching/TemporalLogicProver.html removes some redundant operators. For example, G[a WU b] becomes simple G(a/b), so that just one state variable is required for the remaining temporal logic operator. Other reductions done there are based on suffix-closures that are difficult to explain. You are not expected to do that. Since the complexity of model checking depends on the size of the automata there is a general interest to keep the automata small, or better in whatever way doable for model checking (which may also address the size of the BDDs instead of the number of states), so these simplifications are of interest in practice.
But to keep it short: For the exam, I would not recommend simplifications for the translation from LTL to ω-automata. However, you may have to think about such simplifications when the question should be in which class of ω-automata a formula can be translated.
For the translation from CTL* to CTL (you rather mean LeftCTL* to CTL I guess, since a translation from CTL* to CTL is not always possible), the rules given in the course are indeed sufficient (but maybe not the simplest way). So, to keep things as simple as possible, you could proceed as follows here:
* first reduce all temporal operators to WU and SU only and all boolean operators to negation, conjunction and disjunction
* drive in all negation symbols
* drive in all E and A operators by the laws given
* replace A$\varphi$ by $\neg E\neg\varphi$ and again drive in the new negation after the E
* now you only have E's that can be applied to temporal operators (where nothing has to be done) and disjunctions or conjunctions
* $E(\varphi\vee\psi)$ becomes $(E\varphi)\vee(E\psi)$, and for $E(\varphi\wedge\psi)$, you have to consider the three rules where $\varphi$ and $\psi$ are one of the WU or SU formulas
* in case X-operators should occur, you may have to unwind a temporal operator, e.g. $[a SU b]$ should become $b \vee a \wedge [a SU b]$ and to combine the X-operators (but that does usually not occur)
The steps may have to be repeated a couple of times, and you cannot translate to CTL if driving in the E quantifiers will not be possible, i.e., if you don't find a rule for that on the corresponding slide. Thu, 17 Aug 2017 10:03:39 +0200http://fragestunde.fachschaft.cs.uni-kl.de/Frage/262/ctlctlltlautomata/?answer=263#post-id-263