Title
Výpočetní složitost vybraných verifikačních problémů
Code
GA15-13784S
Summary
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énizergues, 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.
Start year
2015
End year
2017
Provider
Grantová agentura ČR
Category
Obecná forma
Type
Standardní projekty
Solver
Information system of research, development and innovation (in Czech)