Projekty finansowane przez NCN

Dane kierownika projektu i jednostki realizującej

Szczegółowe informacje o projekcie i konkursie

Słowa kluczowe

Aparatura

Wyczyść formularz

Obliczenia symboliczne na obiektach definiowalnych w logice pierwszego rzędu

2016/21/B/ST6/01505

Słowa kluczowe:

weryfikacja formalna obliczenia symboliczne zbiory z atomami zbiory skończenie orbitowe systemy nieskończenie stanowe automaty rejestrowe sieci Petriego z danymi struktury FO definiowalne

Deskryptory:

  • ST6_4: Metody formalne, teoretyczne podstawy informatyki w tym informatyka teoretyczna
  • ST1_15: Matematyczne aspekty informatyki

Panel:

ST6 - Informatyka i technologie informacyjne: technologie i systemy informacyjne, informatyka, obliczenia naukowe, systemy inteligentne

Jednostka realizująca:

Uniwersytet Warszawski, Wydział Matematyki, Informatyki i Mechaniki

woj. mazowieckie

Inne projekty tej jednostki 

Kierownik projektu (z jednostki realizującej):

prof. Sławomir Lasota 

Liczba wykonawców projektu: 6

Konkurs: OPUS 11 - ogłoszony 2016-03-15

Przyznana kwota: 599 600 PLN

Rozpoczęcie projektu: 2017-02-14

Zakończenie projektu: 2020-04-13

Planowany czas trwania projektu: 38 miesięcy (z wniosku)

Status projektu: Projekt rozliczony

Opis Projektu

Pobierz opis projektu w formacie .pdf

Uwaga - opisy projektów zostały sporządzone przez samych autorów wniosków i w niezmienionej formie umieszczone w systemie.

Zakupiona aparatura

  1. Komputery przenośne (3 szt.). Za kwotę 17 074 PLN
  2. Tablet. Za kwotę 4 511 PLN

Dane z raportu końcowego/rocznego

  • Publikacje w czasopismach (4)
  • Teksty w publikacjach pokonferencyjnych (6)
  1. Definable isomorphism problem
    Autorzy:
    Keshvardoost, Khadijeh; Klin, Bartek; Lasota, Sławomir; Ochremiak, Joanna and Toruńczyk, Szymon
    Czasopismo:
    Logical Methods in Computer Science (rok: 2019, tom: 15(4), strony: 14:1--14:19), Wydawca: Free Journal Network
    Status:
    Opublikowana
    Doi:
    10.23638/LMCS-15(4:14)2019 - link do publikacji
  2. Binary reachability of timed-register pushdown automata, and branching vector addition systems
    Autorzy:
    Lorenzo Clemente, Sławomir Lasota, Ranko Lazic, Filip Mazowiecki
    Czasopismo:
    ACM Transactions of Computational Logic (rok: 2019, tom: 20(3), strony: 14:1--14:31), Wydawca: ACM
    Status:
    Przyjęta do publikacji
    Doi:
    10.1145/3326161 - link do publikacji
  3. Scalar and Vectorial mu-calculus with Atoms
    Autorzy:
    Bartek Klin, Mateusz Łełyk
    Czasopismo:
    Logical Methods in Computer Science (rok: 2019, tom: 15(4), strony: 5:1–5:47), Wydawca: Free Journal Network
    Status:
    Złożona
    Doi:
    10.23638/LMCS-15(4:5)2019 - link do publikacji
  4. WQO Dichotomy for 3-graphs
    Autorzy:
    S.Lasota, R.Piórkowski
    Czasopismo:
    Information and Computation (rok: 2020, ), Wydawca: Elsevier
    Status:
    Przyjęta do publikacji
    Doi:
    10.1016/j.ic.2020.104541 - link do publikacji
  1. Regular Separability of Parikh Automata
    Autorzy:
    L.Clemente, W.Czerwinski, S.Lasota, C.Paperman
    Konferencja:
    ICALP'17 (rok: 2017, ), Wydawca: LIPIcs
    Data:
    konferencja 10-14.07.2017
    Status:
    Opublikowana
    Doi:
    link do publikacji
  2. Unboundedness problems for languages of vector addition systems
    Autorzy:
    Wojciech Czerwiński, Piotr Hofman, Georg Zetzsche
    Konferencja:
    ICALP 2018 (rok: 2018, ), Wydawca: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
    Data:
    konferencja 9-13.07.2018
    Status:
    Opublikowana
    Doi:
    link do publikacji
  3. WQO dichotomy for 3-graphs
    Autorzy:
    S.Lasota, R.Piórkowski
    Konferencja:
    FOSSACS'18 (rok: 2018, ), Wydawca: Springer
    Data:
    konferencja 14-20.04.2018
    Status:
    Przyjęta do publikacji
    Doi:
    link do publikacji
  4. Linear Equations with Ordered Data
    Autorzy:
    Piotr Hofman, Sławomir Lasota
    Konferencja:
    CONCUR 2018 (rok: 2018, ), Wydawca: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
    Data:
    konferencja 4-7.09.2018
    Status:
    Opublikowana
    Doi:
    link do publikacji
  5. Timed pushdown automata and branching vector addition systems
    Autorzy:
    L.Clemente, S.Lasota, R.Lazic, F.Mazowiecki
    Konferencja:
    LICS'17 (rok: 2017, ), Wydawca: ACM/IEEE
    Data:
    konferencja 20-23.06.2017
    Status:
    Opublikowana
  6. Binary Reachability of Timed Pushdown Automata via Quantifier Elimination and Cyclic Order Atoms
    Autorzy:
    Lorenzo Clemente, Sławomir Lasota
    Konferencja:
    ICALP 2018 (rok: 2018, ), Wydawca: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik
    Data:
    konferencja 9-13.07.2018
    Status:
    Przyjęta do publikacji
    Doi:
    link do publikacji

O Narodowym Centrum Nauki

Finansowanie nauki

Współpraca zagraniczna

Centrum prasowe

Deklaracja dostępności
Przetwarzanie danych osobowych
Polityka cookies

Partnerzy