About: Výpočetní složitost vybraných verifikačních problémů

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Výpočetní složitost vybraných verifikačních problémů Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Projekt, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	http://linked.opendata.cz/ontology/domain/vavai/Projekt
rdfs:seeAlso	http://www.isvav.cz/projectDetail.do?rowId=GA15-13784S
Description	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. 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. (en)
Title	Výpočetní složitost vybraných verifikačních problémů Computational complexity of selected verification problems (en)
skos:notation	GA15-13784S
http://linked.open...avai/cep/aktivita	Standard projects
http://linked.open...kovaStatniPodpora	http://linked.opendata.cz/resource/domain/vavai/projekt/GA15-13784S/celkovaStatniPodpora
http://linked.open...ep/celkoveNaklady	http://linked.opendata.cz/resource/domain/vavai/projekt/GA15-13784S/celkoveNaklady
http://linked.open...datumDodatniDoRIV	2015-04-23 (xsd:date)
http://linked.open...i/cep/druhSouteze	VS - Veřejná soutěž ve výzkumu a vývoji
http://linked.open...ep/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open.../cep/fazeProjektu	100813348
http://linked.open...ai/cep/hlavniObor	IN - Informatika
http://linked.open...vai/cep/kategorie	ZV - Základní výzkum
http://linked.open.../cep/klicovaSlova	verification; behavioural equivalence; pushdown system; first-order scheme; computational complexity (en)
http://linked.open...ep/partnetrHlavni	Fakulta elektrotechniky a informatiky
http://linked.open...inujicichPrijemcu	0 (xsd:int)
http://linked.open...cep/pocetPrijemcu	1 (xsd:int)
http://linked.open...ocetSpoluPrijemcu	0 (xsd:int)
http://linked.open.../pocetVysledkuRIV	0 (xsd:int)
http://linked.open...enychVysledkuVRIV	0 (xsd:int)
http://linked.open.../prideleniPodpory	http://linked.opendata.cz/resource/domain/vavai/cep/prideleniPodpory/15-13784S
http://linked.open...iciPoslednihoRoku	2015
http://linked.open...atUdajeProjZameru	2015
http://linked.open.../vavai/cep/soutez	SGA0201500001
http://linked.open...usZobrazovaneFaze	DRRVZ
http://linked.open...ai/cep/typPojektu	P - Projekt výzkumu a vývoje financovaný ze státního rozpočtu
http://linked.open...ep/ukonceniReseni	2017-12-31 (xsd:date)
http://linked.open...ep/zahajeniReseni	2015-01-01 (xsd:date)
http://linked.open...tniCyklusProjektu	Z
http://linked.open.../cep/klicoveSlovo	verification behavioural equivalence first-order scheme pushdown system
is http://linked.open...vavai/cep/projekt of	http://linked.opendata.cz/resource/domain/vavai/cep/ucast/GA15-13784S/2015/orjk%3A27240 http://linked.opendata.cz/resource/domain/vavai/cep/ucast/GA15-13784S/2016/orjk%3A27240 http://linked.opendata.cz/resource/domain/vavai/cep/ucast/GA15-13784S/2017/orjk%3A27240

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 112 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software