Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete

Varování

Publikace nespadá pod Fakultu sportovních studií, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky Zevrubné zjemnění na modálních přechodových systémech je EXPTIME-úplný problém
Autoři

BENEŠ Nikola KŘETÍNSKÝ Jan LARSEN Kim G. SRBA Jiří

Rok publikování 2009
Druh Článek ve sborníku
Konference Theoretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-642-03466-4_7
Obor Informatika
Klíčová slova compositional verification; modal transition systems; refinement
Přiložené soubory
Popis Modální přechodové systémy (MTS), specifikační formalismus zavedený před více než 20 lety, jsou nyní ve středu zájmů v řadě různých oblastí. Mnoho základních otázek o MTS již bylo zodpovězeno. Nicméně otázka přesné složitosti zevrubného zjemnění mezi dvěma konečnými MTS zůstala otevřená a byla opakována jako otevřený problém. Tuto otázku zodpovídáme důkazem EXPTIME-úplnosti tohoto problému. Horního odhadu je docíleno exponenciálním algoritmem. Navíc pokud je pravá strana deterministická nebo fixovaná, algoritmus se stává polynomiálním. Dolní odhad je dokázán redukcí z problému akceptace alternujícího lineáně ohraničeného automatu a problém zůstává EXPTIME-těžký, i pokud je levá strana fixována.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info