Učitavanje video playera...
01:34:24
Vedran Čačić: Büchijevi automati koji prepoznaju Hintikkina stabla (3)
Sažetak: Ovo je nastavak seminara održanog krajem 2017. godine, u sklopu dokaza da je ispunjivost čvor-formula logike CPDL s dodanim negacijama atomarnih programa EXPTIME-potpuna (netrivijalan dokaz je da je postoji EXPTIME-algoritam). Tada smo izgradili Hintikkina stabla koja predstavljaju modele (za jednu fiksnu formulu) te logike. Sada ćemo konstruirati Büchijeve automate koji ih prepoznaju, što znači da ćemo za fiksnu formulu fi moći izgraditi ne preveliki automat čiji jezik je neprazan ako i samo ako fi ima model. Kako je provjera nepraznosti jezika zadanog Büchijevog automata odlučiva u eksponencijalnom vremenu, time ćemo dokazati traženu tvrdnju.
