Posts by ink


    Did I understand this correctly: When having a LTL formula, all possible traces have to satisfy the formula?


    Yes, as far as I have understood it correctly, LTL assumes implicit universal (A) quantification over all paths whereas in CTL we have explicit existential (E) and universal (A) quantification.



    Then, in 152 I have {s0,s 1 ,s 2 ,s3 } for F(a) since there is a trace for s4, where a is never satisfied (never leave s4).


    Yes, you are right! I've corrected the error in my result set.


    Also, in 145 I do not get the meaning if G(b -> (Xa -> Xb)). Does this mean that it is globally valid, that when b is satisfied and the next state also satisfies a, this next state also has to satisfy b?


    You can transform

    to

    .

    Can somebody verify the following solutions?:)


    Exam from 27.03.2015 (fmi152.pdf), 4a:


    Exam from 27.03.2015 (fmi152.pdf), 4b:
    [TABLE='class: grid, width: 500']

    [tr]


    [td]

    EG(a)

    [/td]


    [td]

    CTL, CTL*

    [/td]


    [td][/td]


    [/tr]


    [tr]


    [td]

    EX(b)

    [/td]


    [td]

    CTL, CTL*

    [/td]


    [td][/td]


    [/tr]


    [tr]


    [td]

    X(c)

    [/td]


    [td]

    LTL, CTL*

    [/td]


    [td][/td]


    [/tr]


    [tr]


    [td]

    F(a)

    [/td]


    [td]

    LTL, CTL*

    [/td]


    [td]

    all states (EDIT: except s4)

    [/td]


    [/tr]


    [/TABLE]


    Exam from 08.05.2015 (fmi153.pdf), 4b:
    [TABLE='class: grid, width: 500']

    [tr]


    [td]

    G(a)

    [/td]


    [td]

    LTL, CTL*

    [/td]


    [td][/td]


    [/tr]


    [tr]


    [td]

    X(b ^ c)

    [/td]


    [td]

    LTL, CTL*

    [/td]


    [td][/td]


    [/tr]


    [tr]


    [td]

    AG(c)

    [/td]


    [td]

    LTL, CTL, CTL*

    [/td]


    [td][/td]


    [/tr]


    [tr]


    [td]

    EF(c)

    [/td]


    [td]

    CTL, CTL*

    [/td]


    [td]

    all states except s2

    [/td]


    [/tr]


    [/TABLE]


    Exam from 03.07.2015 (fmi154.pdf), 4a:


    Exam from 03.07.2015 (fmi154.pdf), 4b:
    [TABLE='class: grid, width: 500']

    [tr]


    [td]

    EG(a)

    [/td]


    [td]

    CTL, CTL*

    [/td]


    [td][/td]


    [/tr]


    [tr]


    [td]

    EX(a ^ b)

    [/td]


    [td]

    CTL, CTL*

    [/td]


    [td][/td]


    [/tr]


    [tr]


    [td]

    EF(a ^ b)

    [/td]


    [td]

    CTL, CTL*

    [/td]


    [td][/td]


    [/tr]


    [tr]


    [td]

    X(b ^ c)

    [/td]


    [td]

    LTL, CTL*

    [/td]


    [td][/td]


    [/tr]


    [tr]


    [td]

    F(a ^ b)

    [/td]


    [td]

    LTL, CTL*

    [/td]


    [td][/td]


    [/tr]


    [/TABLE]


    Exam from 16.10.2015 (fmi155.pdf), 4b:
    [TABLE='class: grid, width: 500']

    [tr]


    [td]

    G(c)

    [/td]


    [td]

    LTL, CTL*

    [/td]


    [td][/td]


    [/tr]


    [tr]


    [td]

    X(a ^ c)

    [/td]


    [td]

    LTL, CTL*

    [/td]


    [td][/td]


    [/tr]


    [tr]


    [td]

    AG(a)

    [/td]


    [td]

    LTL, CTL, CTL*

    [/td]


    [td]

    no state

    [/td]


    [/tr]


    [tr]


    [td]

    EF(a)

    [/td]


    [td]

    CTL, CTL*

    [/td]


    [td]

    all states

    [/td]


    [/tr]


    [/TABLE]


    Exam from 17.10.2014 (fmi145.pdf), 4a:


    Exam from 17.10.2014 (fmi145.pdf), 4b:
    [TABLE='class: grid, width: 500']

    [tr]


    [td]

    F(c)

    [/td]


    [td]

    LTL, CTL*

    [/td]


    [td]

    all states

    [/td]


    [/tr]


    [tr]


    [td]

    G(b v c)

    [/td]


    [td]

    LTL, CTL*

    [/td]


    [td]

    no state

    [/td]


    [/tr]


    [tr]


    [td]

    G(Fb)

    [/td]


    [td]

    LTL, CTL*

    [/td]


    [td]

    all states

    [/td]


    [/tr]


    [tr]


    [td]

    G(b -> (Xa -> Xb))

    [/td]


    [td]

    LTL, CTL*

    [/td]


    [td]

    all states

    [/td]


    [/tr]


    [tr]


    [td]

    aU(bUc)

    [/td]


    [td]

    LTL, CTL*

    [/td]


    [td][/td]


    [/tr]


    [/TABLE]

    Hello, can sb verify if the following would be a solution?


    We have to provide a reduction from HALTING to SOME-HALTS. The reduction is defined as follows. Let

    be an arbitrary instance of HALTING. We build an instance

    of SH as follows. We define


    [TABLE='class: outer_border, width: 500, align: left']

    [tr]


    [td]

    Boolean

    (String

    , String

    , String

    ) {[INDENT]return

    ;
    [/INDENT]
    }

    [/td]


    [/tr]


    [/TABLE]
    where

    is an interpreter for HALTING which takes two programs and a string as input and alternately executes one line of the first program and then one line of the second program while providing both programs the given string as input. The interpreter returns true if either the first or the second program terminates.



    To prove the correctness of the reduction, we have to show that:

    is a positive instance of [B]HALTING [/B]

    is a positive instance of [B]SOME-HALTS


    [/B]Since we let

    and

    we have to show that:

    is a positive instance of [B]HALTING [/B]

    is a positive instance of [B]SOME-HALTS


    [/B]
    Note that

    is invoked which internally invokes

    .



    "

    ": Suppose that

    is a positive instance of HALTING, i.e.

    terminates when run on input

    . Since the call of our interpreter simulates the run of

    on input

    (twice) it terminates as well. This means that

    provided with

    as

    ,

    as

    and

    as

    terminates as well because one of the provided programs

    or

    terminated given the input

    . Therefore,

    is a positive instance of SOME-HALTS.



    "

    ": Suppose that

    is a positive instance of SOME-HALTS, i.e.

    terminates and either the first or the second program halts when run on input

    . Since both programs are equal to

    , it means that

    halts when run on input

    . Therefore,

    is a positive instance of HALTING.

    Gesucht: Persönliche Assistenz am Arbeitsplatz


    Hallo liebe Leute, wir möchten unser Team erweitern,


    und suchen zur Unterstützung eines sehr sympathischen, körper- und sprechbehinderten Studenten der Medizinischen Informatik eine/n persönliche/n Assistentin/en am Arbeitsplatz. Der Student arbeitet mit "Autonom", eine an der TU Wien entwickelten Software zur externen Steuerung von Tastatur und Maus eines PCs.


    Konkret möchte der Student im kommenden Wintersemester die LVA Algorithmen und Datenstrukturen 2 absolvieren.


    Voraussetzungen
    * Algorithmen und Datenstrukturen 2 bereits abgeschlossen
    * Gute Deutschkenntnisse


    Tätigkeiten
    * Die Autonom-Software muss immer wieder mit neuen Befehlen ausgestattet und angepasst werden
    * Gemeinsames Bearbeiten der Übungsbeispiele
    * Unterstützung des Studenten beim Erlernen des Stoffes für die Endprüfung
    * Kreativ Bilder für die Masken erstellen
    * Autonom laufend konfigurieren
    * Prüfungsvorbereitung
    * Besprechungen mit dem jeweiligen Professoren über den Prüfungsmodus und den Prüfungsablauf
    * Anwesenheit bei Prüfungen
    * Kommunikation zwischen Professoren und Studenten
    * Eine Einschulung erfolgt vor Ort


    Arbeitszeit
    Mindestens einmal wöchentlich 3 Stunden wobei der Tag mit dem Studenten vereinbart wird/ Verhandlungen mit den Prof. und Anwesenheit bei Prüfungen etc werden. sep. bezahlt.


    Arbeitsort
    Beim Studenten zuhause im 22. Bezirk, Donaustadt


    Anstellungsdauer
    Mindestens 2 Semester, Verlängerung ist möglich


    Arbeitsverhältnis und Bezahlung
    Freier Dienstvertrag, Bezahlung nach Vereinbarung

    Kontakt
    Christian Detamble
    christian.detamble@hotmail.com
    0677 61266904

    Die Tutorenstelle ist bereits vergeben, allerdings bieten wir eine Stelle als persönliche/n Assistentin/en am Arbeitsplatz an. Der Stundenlohn beträgt dabei 11€ brutto mit einem freien Dienstvertrag, wobei die Stundenanzahl variabel ist.

    Nein, die Liste ist vollständig. Gesucht war ursprünglich nur ein Tutor - jetzt werden insgesamt 3 Tutoren gesucht, wobei einer schon bei der Einschulung war und sich ein weiterer heute gemeldet hat. Das einzige was mir noch einfällt, und nicht oben steht, ist die Koordination unter den Tutoren bzgl. was vom Stoff schon durchgenommen wurde. Bis jetzt war's üblich, nach jedem Tutorium in einem Textdokument in der Dropbox einzutragen, wie weit man im Stoff gekommen ist. Falls du Interesse hast, können wir gerne bei einer unverbindlichen Einschulung vor Ort alle Unklarheiten beseitigen. :-)