This HTML5 document contains 36 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
n13http://linked.opendata.cz/ontology/domain/vavai/cep/zivotniCyklusProjektu/
n21http://linked.opendata.cz/ontology/domain/vavai/cep/druhSouteze/
n6http://linked.opendata.cz/ontology/domain/vavai/cep/typPojektu/
dctermshttp://purl.org/dc/terms/
n2http://linked.opendata.cz/resource/domain/vavai/projekt/
n16http://linked.opendata.cz/resource/domain/vavai/subjekt/
n12http://linked.opendata.cz/resource/domain/vavai/cep/prideleniPodpory/
n20http://linked.opendata.cz/ontology/domain/vavai/cep/kategorie/
n14http://linked.opendata.cz/ontology/domain/vavai/
n17http://linked.opendata.cz/ontology/domain/vavai/cep/duvernostUdaju/
skoshttp://www.w3.org/2004/02/skos/core#
rdfshttp://www.w3.org/2000/01/rdf-schema#
n19http://linked.opendata.cz/ontology/domain/vavai/cep/obor/
n5http://linked.opendata.cz/ontology/domain/vavai/cep/fazeProjektu/
n9http://linked.opendata.cz/resource/domain/vavai/soutez/
n11http://linked.opendata.cz/ontology/domain/vavai/cep/statusZobrazovaneFaze/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
xsdhhttp://www.w3.org/2001/XMLSchema#
n4http://linked.opendata.cz/ontology/domain/vavai/cep/
n10http://linked.opendata.cz/resource/domain/vavai/projekt/GA15-13784S/
n8http://linked.opendata.cz/resource/domain/vavai/aktivita/
n7http://reference.data.gov.uk/id/gregorian-year/

Statements

Subject Item
n2:GA15-13784S
rdf:type
n14:Projekt
rdfs:seeAlso
http://www.isvav.cz/projectDetail.do?rowId=GA15-13784S
dcterms:description
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. Verifikace hardwarových a softwarových systémů se stává neoddělitelnou součástí jejich vývoje. Zkoumání mezí automatizované verifikace odhalilo několik zajímavých problémů, jejichž výpočetní složitost je nejasná i přes nemalé úsilí výzkumné komunity. Takovým problémem je i ekvivalence funkčních schémat prvního řádu, který lze vyjádřit jako ekvivalenci deterministických zásobníkových automatů. Rozhodnutelnost problému je proslulý výsledek, který docílil G. Sénizergues, ale známá složitost leží někde mezi polynomiálním časem a opakovaným umocňováním. Hlavním cílem projektu je prozkoumání tohoto a příbuzných problémů podrobněji, v návaznosti na předchozí výzkum členů týmu, který vyjasnil složitost některých podpřípadů. Důležitou součástí projektu je vytvoření softwarového nástroje, který umožní experimentování s instancemi problémů, což by mělo umožnit získání většího vhledu do problémů ekvivalence.
dcterms:title
Výpočetní složitost vybraných verifikačních problémů Computational complexity of selected verification problems
skos:notation
GA15-13784S
n4:aktivita
n8:GA
n4:celkovaStatniPodpora
n10:celkovaStatniPodpora
n4:celkoveNaklady
n10:celkoveNaklady
n4:datumDodatniDoRIV
2015-04-23+02:00
n4:druhSouteze
n21:VS
n4:duvernostUdaju
n17:S
n4:fazeProjektu
n5:100813348
n4:hlavniObor
n19:IN
n4:kategorie
n20:ZV
n4:klicovaSlova
verification; behavioural equivalence; pushdown system; first-order scheme; computational complexity
n4:partnetrHlavni
n16:orjk%3A27240
n4:pocetKoordinujicichPrijemcu
0
n4:pocetPrijemcu
1
n4:pocetSpoluPrijemcu
0
n4:pocetVysledkuRIV
0
n4:pocetZverejnenychVysledkuVRIV
0
n4:prideleniPodpory
n12:15-13784S
n4:sberDatUcastniciPoslednihoRoku
n7:2015
n4:sberDatUdajeProjZameru
n7:2015
n4:soutez
n9:SGA0201500001
n4:statusZobrazovaneFaze
n11:DRRVZ
n4:typPojektu
n6:P
n4:ukonceniReseni
2017-12-31+01:00
n4:zahajeniReseni
2015-01-01+01:00
n4:zivotniCyklusProjektu
n13:Z
n4:klicoveSlovo
first-order scheme pushdown system verification behavioural equivalence