"V\u00FDpo\u010Detn\u00ED slo\u017Eitost vybran\u00FDch verifika\u010Dn\u00EDch probl\u00E9m\u016F" . . "Verification of hardware and software systems is increasingly recognized as a non-dispensable part of their development. Exploring the bounds of automated verification has exposed several interesting problems whose computational complexity remains elusive despite a considerable effort of the research community. One such problem is the equivalence of first-order schemes, which can be phrased as language equivalence of deterministic pushdown automata. Its decidability is the celebrated result by G. S\u00E9nizergues, but the known complexity lies somewhere between polynomial time and the tower of exponentials. The main aim of the project is to explore this and related problems in more detail, continuing the previous research of the project team that clarified the complexity of some subcases. An important part of the project is the development of a software tool that will allow to experiment with problem instances, which should bring a new research insight into the equivalence problems."@en . " first-order scheme" . . . . . . . . . "0"^^ . "verification; behavioural equivalence; pushdown system; first-order scheme; computational complexity"@en . "2015-01-01+01:00"^^ . . . " pushdown system" . "2015-04-23+02:00"^^ . "1"^^ . "0"^^ . "0"^^ . . "Computational complexity of selected verification problems"@en . "verification" . "0"^^ . "http://www.isvav.cz/projectDetail.do?rowId=GA15-13784S"^^ . "Verifikace hardwarov\u00FDch a softwarov\u00FDch syst\u00E9m\u016F se st\u00E1v\u00E1 neodd\u011Blitelnou sou\u010D\u00E1st\u00ED jejich v\u00FDvoje. Zkoum\u00E1n\u00ED mez\u00ED automatizovan\u00E9 verifikace odhalilo n\u011Bkolik zaj\u00EDmav\u00FDch probl\u00E9m\u016F, jejich\u017E v\u00FDpo\u010Detn\u00ED slo\u017Eitost je nejasn\u00E1 i p\u0159es nemal\u00E9 \u00FAsil\u00ED v\u00FDzkumn\u00E9 komunity. Takov\u00FDm probl\u00E9mem je i ekvivalence funk\u010Dn\u00EDch sch\u00E9mat prvn\u00EDho \u0159\u00E1du, kter\u00FD lze vyj\u00E1d\u0159it jako ekvivalenci deterministick\u00FDch z\u00E1sobn\u00EDkov\u00FDch automat\u016F. Rozhodnutelnost probl\u00E9mu je proslul\u00FD v\u00FDsledek, kter\u00FD doc\u00EDlil G. S\u00E9nizergues, ale zn\u00E1m\u00E1 slo\u017Eitost le\u017E\u00ED n\u011Bkde mezi polynomi\u00E1ln\u00EDm \u010Dasem a opakovan\u00FDm umoc\u0148ov\u00E1n\u00EDm. Hlavn\u00EDm c\u00EDlem projektu je prozkoum\u00E1n\u00ED tohoto a p\u0159\u00EDbuzn\u00FDch probl\u00E9m\u016F podrobn\u011Bji, v n\u00E1vaznosti na p\u0159edchoz\u00ED v\u00FDzkum \u010Dlen\u016F t\u00FDmu, kter\u00FD vyjasnil slo\u017Eitost n\u011Bkter\u00FDch podp\u0159\u00EDpad\u016F. D\u016Fle\u017Eitou sou\u010D\u00E1st\u00ED projektu je vytvo\u0159en\u00ED softwarov\u00E9ho n\u00E1stroje, kter\u00FD umo\u017En\u00ED experimentov\u00E1n\u00ED s instancemi probl\u00E9m\u016F, co\u017E by m\u011Blo umo\u017Enit z\u00EDsk\u00E1n\u00ED v\u011Bt\u0161\u00EDho vhledu do probl\u00E9m\u016F ekvivalence." . . " behavioural equivalence" . . "GA15-13784S" . . "2017-12-31+01:00"^^ . . .