Sljedeći termin:

ponedjeljak, 9. lipnja 2008., 15:00, predavaonica 109 — Paola Glavan, FSB

Kada su dva algoritma jednaka?

Algoritmi se obično smatraju apstaktnijima od programa koji ih implemetiraju. Prirodna formalizacija te ideje je: algoritmi su klase ekvivalencije programâ u odnosu na neku relaciju ekvivalencije.
Koja relacija ekvivalencije "hvata" taj pojam i postoji li ona uopće?

Seminari održani ove akademske godine (2007./08.):

ponedjeljak, 12. svibnja 2008., 15:00; predavaonica 109 — Andre Scedrov

Collaborative planning with privacy

Collaboration among organizations or individuals is common. While these participants are often unwilling to share all their information with each other, some information sharing is unavoidable when achieving a common goal. The need to share information and the desire to keep it private/secret are two competing notions which affect the outcome of a collaboration. This joint work with Kanovich and Rowe proposes a formal model of collaboration which addresses privacy/secrecy concerns. We draw on the notion of a plan which originates in the AI literature. We consider transition systems in which actions have pre- and post-conditions of the same size. We show it is PSPACE-complete to decide whether a given such system protects the privacy/secrecy of its participants and whether it contains a plan leading from a given initial state to a desired goal state.


ponedjeljak, 5. svibnja 2008., 15:00; predavaonica 109 — Andre Scedrov

Formal Analysis of the Kerberos 5 Authentication Protocol

The design and security analysis of protocols that use cryptographic primitives is one of the most fundamental and challenging areas of computer security research. Relatively succinct but subtle authentication, key exchange, negotiation, authorization, and related protocols are the building blocks for secure distributed systems. Protocol analysis is a successful scientific area with two important but historically independent foundations, one based on symbolic computation and one based on computational complexity theory.

Here we highlight joint work with Cervesato, Jaggard, Tsay, and Walstad on the formal analysis of the Kerberos 5 authentication protocol suite. This work discovered a serious vulnerability in the Kerberos public-key extension and caused a Microsoft security patch for Windows 2000 and Windows XP operating systems. The work contributed to the reformulation of the IETF standard for Kerberos public-key extension and provided security proofs of the corrected version of the protocol, the latter jointly with Backes. The flaw discovered is not a flaw in implementation or in cryptography, but a protocol-level, structural flaw, which is present even when the underlying cryptographic operations and network infrastructure operate normally. The methodology developed in this work is applicable to a wide range of network security protocols. We also discuss current joint work with Blanchet on mechanized proofs of authentication and key secrecy properties of Kerberos 5, both with and without its public-key extension.

 

ponedjeljak, 10. ožujka 2008., 17:15
ponedjeljak, 17. ožujka 2008., 17:15 — Domagoj Vrgoč

Random reals

Tehnički rezultati teorije iračunljivosti. Hijerarhije reducibilnosti (1, m, tt, wtt, sw, T). Aritmetička hijerarhija i Hijerarhija Ershova. hijerarhija jumpova i Postov teorem. Izračunljivi i rekurzivno prebrojivi realni brojevi.

Tri osnovna pristupa definiciji random broja. Preko teorije mjere(paradigma tipičnosti), nekompresibilnosti (prefix-free complexity) i teorije vjerojatnosti (nemogućnost uspješnog klađenja). Također raspravljamo i o Solovayevoj karakterizaciji, ukoliko postoji.

Definiramo četiri osnovne klase random brojeva: Martin-Löf randoms, computable randoms, Schnorr randoms i Kurtz randoms, te uspostavljamo njihovu hijerarhiju. Poopćenja bazirana na aritmetičkoj hijerarhiji i hijerarhiji Ershova.

ponedjeljak, 11. veljače 2008., 17:15 — Darko Biljaković

Nefaktorizabilnost kvocijentnog prstena generaliziranih redova potencija s nepozitivnim eksponentima po Berarduccijevom idealu

Na prethodnom seminaru ustanovljena je pogreška u dokazu Pitteloudove tvrdnje da se svaka klasa generaliziranih redova iz navedenog prstena može prikazati kao produkt ireducibilnih elemenata tog prstena.
Sada dajemo kontraprimjer za tu tvrdnju.
Osim toga, koliko je nama poznato, po prvi puta su prikazani neki ireducibilni te prosti elementi našeg prstena.

ponedjeljak, 4. veljače 2008., 17:15 — Zvonimir Šikić

Neka poopćenja Schröder, Bernsteinovog teorema

ponedjeljak, 28. siječnja 2008., 17:15 — Zvonimir Šikić

Freilingovo opovrgnuće hipoteze kontinuuma

&

Indukcija bez uređaja

ponedjeljak, 3. prosinca 2007., 15:00
— Ružica Piskač, Swiss Federal Institute of Technology (EPFL)

Decision Procedures for Multisets with Cardinality Constraints

Applications in software verification and interactive theorem proving often involve reasoning about sets of objects. Cardinality constraints on such collections also arise in these applications. Multisets arise in these applications for analogous reasons as sets: abstracting the content of linked data structure with duplicate elements leads to multisets. Interactive theorem provers such as Isabelle specify theories of multisets and prove a number of theorems about them to enable their use in interactive verification. However, the decidability and complexity of constraints on multisets is much less understood than for constraints on sets.

The first contribution of this paper is a polynomial-space algorithm for deciding expressive quantifier-free constraints on multisets with cardinality operators. Our decision procedure reduces in polynomial time constraints on multisets to constraints in an extension of quantifier-free Presburger arithmetic with certain ``unbounded sum'' expressions. We prove bounds on solutions of resulting constraints and describe a polynomial-space decision procedure for these constraints.

The second contribution of this paper is a proof that adding quantifiers to a constraint language containing subset and cardinality operators yields undecidable constraints. The result follows by reduction from Hilbert's 10th problem.

ponedjeljak, 22. listopada 2007., 17:15 (slideovi)
ponedjeljak, 29. listopada 2007., 17:15 (slideovi) — Vedran Čačić

Dekorirani uređaji i teorija konkatenacije

Interpretacija teorije konkatenacije (TC) A. Grzegorczyka u strukturama dekoriranih uređajnih tipova. TC je nepotpuna za tu interpretaciju. Interpretacija aritmetike unutar konkretnih konkatenacijskih strukturâ. Svako proširenje od TC ima model koji nije izomorfan nijednoj strukturi dekoriranih uređajnih tipova.

Seminari održani prethodne akademske godine (2006./07.):

ponedjeljak, 11. lipnja 2007., 17:15 — Marko Doko

Nepotpunost kao posljedica slučajnosti

Definicija kompleksnosti i algoritamske vjerojatnosti, i veza između ta dva pojma. Definicija slučajnosti preko kompleksnosti. Dokaz da iz činjenice da je halting probability slučajan broj slijedi nepotpunost.

ponedjeljak, 4. lipnja 2007., 16:00 — Matko Botinčan

Distribuirani algoritmi — studijski primjer memorijskog modela Jave

(zajednički rad s Paolom Glavan i Davorom Runje)

U ovom seminaru dat ćemo matematički preciznu specifikaciju memorijskog modela Jave (JMM-a), te diskutirati njegovu interpretaciju u kontekstu strojeva s apstraktnim stanjima (ASM-ova). Izvorna specifikacija JMM-a refaktorizirana je na način kako bi bilo jasno vidljivo na koji način JMM uvjetuje ponašanje okoline. Pri tome, svaka nit višenitnog Java programa predstavlja obični interaktivni small-step algoritam, a sam Java program distribuirani obični interaktivni small-step ASM. Obzirom da JMM predstavlja relaksirani memorijski model, ovakvi ASM-ovi manifestiraju ponašanje koje je nemoguće opaziti u sekvencijalno konzistentnom slučaju. Obzirom da svi dosadašnji modeli izvršavanja distribuiranih ASM-ova pretpostavljaju sekvencijalnu konzistentnost, smatramo da naš model koji jasno razdvaja koncept izvršavanja, okolinu izvršavanja, te opravdanje za okolinu izvršavanja daje koristan uvid u dio onoga što bi trebalo uzeti u obzir prilikom daljnjeg razvoja teorije distribuiranih algoritama (unutar ASM konteksta).

ponedjeljak, 28. svibnja 2007., 17:15
ponedjeljak, 21. svibnja 2007., 17:15 — Ljerka Jukić

Teorem o normalnoj formi za zatvoreni fragment logike interpretabilnosti

ponedjeljak, 14. svibnja 2007., 17:15
ponedjeljak, 7. svibnja 2007., 17:15 — Domagoj Vrgoč

Morleyev teorem

ponedjeljak, 26. veljače 2007., 17:15 — Zvonimir Šikić

Što je logicizam i je li propao?

ponedjeljak, 12. veljače 2007., 17:15 — Zvonimir Šikić

Arrowljev teorem

Nemogućnost pravednosti ili upitna pravednost

ponedjeljak, 13. studenog 2006., 17:15 — Marko Doko

Kardinalna aritmetika

Pojam kofinalnosti, regularni i singularni kardinali. Veza potenciranja, kofinalnosti i beskonačnih sumâ i produkata. Ograničenja koja ZFC postavlja na funkciju kontinuuma.

Jaki granični kardinali, Jechov teorem. Bukovsky-Hechlerov teorem. Neki rezultati uz pretpostavku da vrijedi Hipoteza singularnih kardinalâ ili Generalizirana hipoteza kontinuuma.

ponedjeljak, 9. listopada 2006., 17:15 — Darko Biljaković

Primjedbe na rad D. Pittelouda "Algebraic properties of rings of generalized power series", APAL 16, 2002, 39-66

U navedenom radu autor dokazuje da je ideal J prstena generaliziranih redova k((G≤0)), generiran monomima s negativnim eksponentom, prost, služeći se izvjesnom procjenom dobivenom mukotrpnim računom. U drugom rezultatu tvrdi pomoću iste procjene kako svaki element kvocijentnog prstena k((G≤0))/J ima bar jednu faktorizaciju na ireducibilne faktore.

Pokazat ćemo kako se prva tvrdnja može dokazati mnogo jednostavnije, a da druga tvrdnja ne stoji te ćemo negativno odgovoriti na pitanje Berarduccija, S. Kuhlmann i F.-V. Kuhlmann je li k((G≤0)) faktorizacijski prsten.

Održani seminari akademske godine 2005./06.:


ponedjeljak, 25. rujna 2006., 17:15 — Vedran Čačić

Nezavisnost aksioma izbora

Nakon što je razvijena tehnika forcinga, i njome dokazana nezavisnost hipoteze kontinuuma od ZFC, možemo otići i korak dalje, i dokazati nezavisnost aksioma izbora od preostalih aksiomâ, dakle od ZF. U tu svrhu razvit ćemo teoriju simetričnih skupova, i izgraditi međumodel M⊆N⊆M[G], u kojem će vrijediti ZF, ali ne AC.

ponedjeljak, 18, rujna 2006., 17:15
ponedjeljak, 11. rujna 2006., 17:15
ponedjeljak, 29. svibnja 2006., 18:15,
ponedjeljak, 12. lipnja 2006.,
ponedjeljak, 19. lipnja 2006. — Vedran Čačić

Nezavisnost hipoteze kontinuuma

Osnove metode forcinga. Generički skupovi. Osnovni i prošireni model. Aksiomi koji vrijede u proširenom modelu. Prošireni model kao model za ZF. Leme istinitosti i definabilnosti.

ponedjeljak, 5. lipnja 2006. — Tamas Mihalydeak, University of Debrecen

Tarskian and Husserlian models

(otkazan) ponedjeljak, 29. svibnja 2006. — Sanja Balenović

Teorija korespondencije

Osnovne definicije, standardne translacije, modalna saturacija pomoću ultrafilter-proširenja; van Benthemov teorem karakterizacije, iskaz i dokaz.

ponedjeljak, 15. svibnja 2006. — Mirko Mihaljinec

O Hiparh—Plutarhovim brojevima 103049 i 310952

Rekonstrukcija sintakse složenih sudova u logici stoičke škole

ponedjeljak, 8. svibnja 2006. — Darko Biljaković

Generalizirani redni brojevi i primjena na generalizirane redove potencijâ

Pokazuje se kako se generalizirane diferencije višeg reda generaliziranih redova potencijâ s nenegativnim eksponentima ponašaju slično diferencijama višeg reda običnih polinomâ. Pri tome su izvjesne klase generaliziranih rednih brojeva korisna reprezentacija običnih rednih brojeva.

ponedjeljak, 24. travnja 2006.— Vedran Čačić

NuPRL i teorija tipova(2)

Pregled rekurzije, automatskog zaključivanja (inferencije) tipova, paradigme dokazivanja u NuPRLu, te nekih jednostavnih dokazâ. Pogledat ćemo to sve prvo na jednoj podteoriji, a zatim i u punom kontekstu. Vidjet ćemo da su ugrađeni tipovi i osnovni konstrukti NuPRLa pažljivo odabrani kako bi se zadovoljili i matematički i tehnički aspekti automatskog dokazivanja.

ponedjeljak, 10. travnja 2006. — Vedran Čačić

Sustav NuPRL i teorija tipova

Automatsko dokazivanje matematičkih tvrdnji nekada se činilo kao isključivo akademska djelatnost. No, kako se doseg matematičkih modela sve više širi, u computer scienceu ali i drugdje, javlja se potreba za snažnim softverskim alatima (proof assistants), kao i matematičkim teorijama koje su prilagođenije kompjuterskim dokazima nego što je to klasična logika prvog reda. NuPRL je pokušaj izgradnje takvog softverskog alata, dok se intuicionistička teorija tipova može upotrijebiti kao matematička pozadina.

ponedjeljak, 3. travnja 2006. — Matko Botinčan

Entanglement i thief-and-detectives

Entanglement predstavlja recentno predloženu mjeru složenosti konačnih usmjerenih grafova, koja intuitivno kazuje u kojoj mjeri su ciklusi u grafu međusobno isprepleteni. Definirana je pomoću thief-and-detectives igre, konceptualno slične onoj koja se javlja u karakterizaciji tree-widtha. Ipak, njihova svojstva su u mnogočemu različita. Također, entanglement je usko povezan s računskom i deskriptivnom složenosti modalnog μ-računa i pripadajućih igara parnosti. U ovom seminaru pogledat ćemo osnovna svojstva entanglementa i pokazati da su igre parnosti na klasi grafova omeđenog entanglementa rješive u polinomnom vremenu.

ponedjeljak, 27. ožujka 2006. — Matko Botinčan

Tree-width i robber-and-cops

Stablasta dekompozicija, i uz nju vezan pojam stablaste širine (tree-width), od velike je važnosti u teoriji grafova. Jedan od fundamentalnih rezultatâ kaže da MSO-definabilni problemi (u koje spadaju mnogi NP-potpuni problemi na grafovima) postaju rješivi u linearnom vremenu na klasi grafova omeđene stablaste širine. Također, interesantnom se pokazala i karakterizacija stablaste širine pomoću robber-and-cops igre. U ovom seminaru dat ćemo pregled važnijih rezultatâ i primjenâ na neke probleme u verifikaciji.