Projects funded by the NCN


Information on the principal investigator and host institution

Information of the project and the call

Keywords

Equipment

Delete all

Symbolic computations on first-order definable objects

2016/21/B/ST6/01505

Keywords:

formal verification symbolic computation sets with atoms orbit-finite sets infinite-state systems register automata Petri nets with data FO definable structures

Descriptors:

  • ST6_4: Formal methods, foundations of computer science, including theoretical computer science, quantum algorithms
  • ST1_15: Mathematical aspects of computer science

Panel:

ST6 - Computer science and informatics: informatics and information systems, computer science, scientific computing, intelligent systems

Host institution :

Uniwersytet Warszawski, Wydział Matematyki, Informatyki i Mechaniki

woj. mazowieckie

Other projects carried out by the institution 

Principal investigator (from the host institution):

prof. Sławomir Lasota 

Number of co-investigators in the project: 6

Call: OPUS 11 - announced on 2016-03-15

Amount awarded: 599 600 PLN

Project start date (Y-m-d): 2017-02-14

Project end date (Y-m-d): 2020-04-13

Project duration:: 38 months (the same as in the proposal)

Project status: Project settled

Project description

Download the project description in a pdf file

Note - project descriptions were prepared by the authors of the applications themselves and placed in the system in an unchanged form.

Equipment purchased [PL]

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

Information in the final report

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