Informacje ogólne

FIT (Forum Informatyki Teoretycznej) jest doroczną polską konferencją informatyczną odbywającą się nieprzerwanie od 1991 roku. Jej tegoroczna edycja, organizowana przez Instytut Informatyki Analitycznej Wydziału Matematyki i Informatyki Uniwersytetu Jagiellońskiego, odbędzie się wraz z Jubileuszowym Zjazdem Matematyków Polskich organizowanym w stulecie Polskiego Towarzystwa Matematycznego w Krakowie, w dniach 6–7 września 2019.


Note for English-speaking readers

This year's FIT edition is organized as part of the centennial anniversary of the Polish Mathematical Society and will be held in Polish. For more information on the previous FIT edition, please visit this webpage.

Tarski - Logika i Informatyka Teoretyczna

Serdecznie zapraszamy uczestników FIT do wzięcia udziału w sesji zjazdowej "Tarski - Logika i informatyka teoretyczna" odbywającej się w czwartek, 5 września, po południu.


Rejestracja

Rejestracja na FIT odbywa się poprzez formularz na stronie Zjazdu PTM. W formularzu proszę zaznaczyć opcję "Deklaruję udział w Forum Informatyki Teoretycznej". Uczestnicy FIT, którzy nie planują udziału w całym Zjeździe PTM, proszeni są także o wybór opcji "Wyrażam chęć wyłącznej rejestracji na FIT". Uczestnicy FIT, którzy zamierzają wygłosić referat, proszeni są o zaznaczenie tego w formularzu rejestracyjnym oraz o wybór FIT jako sesji tematycznej.

Opłata konferencyjna wynosi 150 PLN i pokrywa uczestnictwo w FIT oraz innych sesjach tematycznych Zjazdu PTM w dniach 6–7 września, obiady i przerwy kawowe. Opłata za uczestnictwo w bankiecie FIT, który odbędzie się 6 września, wynosi dodatkowe 150 PLN.

Dane do przelewu:

IBAN: PL 61 1240 4722 1111 0000 4860 4116
BIC: PKOPPLPW
Właściciel rachunku: Wydział Matematyki i Informatyki UJ, ul. Łojasiewicza 6, 30-348 Kraków
Tytuł przelewu: FIT + nazwiska uczestników

Informacje o możliwościach zakwaterowania dostępne są na stronie Zjazdu PTM po zalogowaniu, w zakładce Zakwaterowanie.

Termin rejestracji

Termin rejestracji i zgłaszania referatów mija 10 sierpnia 2019 o godzinie 23:59.

Informacja dla osób zgłaszających referaty

Formularz rejestracyjny Zjazdu PTM nie umożliwia rejestracji kilku referatów, w tym w ramach różnych sesji. Osoby zainteresowane wygłoszeniem referatu na FIT, które nie mogą go zgłosić poprzez system Zjazdu PTM, proszone są o bezpośredni kontakt z organizatorami FIT.


Zaproszeni goście

  • Tomasz Kociumaka, Bar-Ilan University
  • Krzysztof Onak, IBM Research
  • Jakub Tarnawski, École Polytechnique Fédérale de Lausanne

Sesja specjalna

6 września odbędzie się sesja specjalna pt. Zastosowania teorii gier w informatyce koordynowana przez Krzysztofa Apta. Będzie ona połączona ze Zjazdem Matematyków Polskich. Zaproszeni goście:

  • Marta Kwiatkowska, University of Oxford

      Weryfikacja modelowa dla gier stochastycznych

    Probabilistyczna weryfikacja modelowa jest metodą formalnej weryfikacji poprawności systemów stochastycznych, których własności wyrażane są w probabilistycznej logice temporalnej. Pokrewnym problemem jest synteza strategii, która automatycznie generuje strategię zapewniającą, że dana formuła logiki temporalnej jest spełniona w modelu. Dzięki wsparciu zaawansowanych narzędzi, takich jak na przykład PRISM (www.prismmodelchecker.org), metody te zostały z powodzeniem zastosowane w wielu dziedzinach, w tym w pojazdach autonomicznych, bezpieczeństwie komputerowym i protokołach komunikacyjnych. Wykład ten jest przeglądem najnowszych osiągnięć w zakresie probabilistycznej weryfikacji modelowej współbieżnych gier stochastycznych z uwzględnieniem prawdopodobieństwa, niedeterminizmu oraz wielu graczy konkurujących lub współpracujących, aby osiągnąć swoje cele. W przeciwieństwie do gier turowych, gracze we współbieżnych grach stochastycznych podejmują decyzje jednocześnie. Następnie zostaną przedstawione techniki algorytmiczne, nazywane PRISM-games, opracowane jako rozszerzenie narzędzia PRISM, które przyjmują jako specyfikację formuły podane w probabilistycznej logice temporalnej czasu alternującego i wspierają rozumowanie na temat optymalnych równowag społecznych Nasha dla koalicji graczy. Zastosowanie tych metod zostanie zilustrowane przykładami, takimi jak nawigacja robotów, protokoły komunikacyjne i sterowanie zużyciem energii. Wykład zakończy się podsumowaniem wyzwań istniejących w omawianej dziedzinie.

    Bibliografia

  • Piotr Krysta, University of Liverpool

      Algorytmiczne projektowanie mechanizmów dla aukcji kombinatorycznych

    Mój wykład będzie wstępem do projektowania mechanizmów prawdomównych dla problemów aukcji kombinatorycznych, gwarantujących aproksymacje rozwiązań społecznie optymalnych. Rozważę dwie wersje takich aukcji: pierwszą, która zakłada stałą liczbę sprzedawanych przedmiotów, oraz drugą, która nie ma tego założenia i nie ma dodatkowych założeń o wartościowaniach kupujących.

    Dla pierwszej wersji pokazujemy istnienie deterministycznych prawdomównych mechanizmów aproksymacyjnych, w których sprzedający wystawia stałą liczbę różnych przedmiotów, każdy dostępny w ograniczonej liczbie kopii. Kupujący wyrażają swoje preferencje dla multizbiorów przedmiotów, tj. mogą zażądać jednej lub większej liczby kopii każdego przedmiotu. Celem mechanizmu aukcyjnego jest wyznaczenie alokacji multizbiorów, która jest aproksymacją alokacji społecznie optymalnej. Pomimo istnienia bogatej literatury o prawdomównych mechanizmach dla problemów aukcji kombinatorycznych (zakładających wiele różnych przedmiotów) oraz dla problemów aukcji "multi-unitarnych" (zakładających wielu kopii jednego typu przedmiotu), niewiele wiadomo na temat mechanizmów, które łączą te dwie wersje aukcji. Nasze wyniki dla tego typu aukcji uzyskane są przy założeniu submodularnych i "multi-minded" wartościowań uczestników aukcji.

    Dla drugiej, ogólnej, wersji pokazujemy istnienie prawdomównych mechanizmów aproksymacyjnych dla aukcji kombinatorycznych w modelu online, w którym kupujący pojawiają się sekwencyjnie. Rozważamy dwa warianty takich sekwencji: wariant losowy oraz wariant adwersarialny. Wartościowania uczestników aukcji zadane są przez wyrocznię popytu. Dotychczasowe wyniki dla tego typu aukcji zakładały, że każdy przedmiot dostępny jest w $b > 1$ kopiach, gdzie najczęstsze założenie to $b = \Omega(\log m)$, gdzie $m$ oznacza liczbę typów towarów. Zaproponowane przez nas mechanizmy online dają gwarancje aproksymacyjne bez tego typu założeń. Wprowadzamy nowa technikę nieświadomego zaokrąglania randomizowanego, która umożliwia nam dowodzenie gwarancji aproksymacji w modelu online, które są silniejsze niż najlepsze znane aproksymacje, nawet w modelu 'offline'. Nasze mechanizmy randomizowane są uniwersalnie prawdomówne i znacząco lepsze od dotychczas znanych mechanizmów tego typu.

    Wykład prezentuje wyniki otrzymane wspólnie z Orestisem Telelisem, Carmine Ventre oraz Bertholdem Voeckingiem.

  • Igor Walukiewicz, Université de Bordeaux

      Gry i punkty stałe

    Gra jest interesującą metaforą dla opisania struktury obliczenia. Centralnym problemem jest znalezienie metody na rozwiazanie gier ustalonego typu, to znaczy określenie kto ma strategie wygrywającą w danej grze. W skrócie nazywamy to problemem rozwiązania gry. W tym wystąpieniu skoncentrujemy się na pewnym typie gier, zwanym grami z warunkami parzystości, i na jego związku z problem obliczania punktów stałych. W 2017 roku, Calude, Jain, Khoussainov, Li, and Stephan, znaleźli pierwszy quasi-wielomianowy algorytm na rozwiązywanie gier z warunkami parzystości. Algorytm ten można przedstawić jako metodę na obliczenie wartości termów z punktami stałymi. Gry parzystości, jak też problem obliczania wartości termów z punktami stałymi, maja bezpośrednie związki z otwartymi problemami w weryfikacji systemów informatycznych, programowaniu liniowym, i planowaniu stochastycznym. Wyniki z ostatnich lat pozwalają mieć nadzieje na postęp w rozwiązaniu problemów otwartych od kilku dziesięcioleci.


Kontakt

Komitet organizacyjny: Maciej Bendkowski, Jakub Kozik oraz Bartosz Walczak.

Email: fit@tcs.uj.edu.pl