Checking Thorough Refinement on Modal Transition Systems Is EXPTIME-Complete

• 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
• 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

• 2009-ICTAC.pdf

• 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

• Techniky automatické verifikace a validace softwarových a hardwarových systémů
• Institut Teoretické Informatiky
• Vysoce paralelní a distribuované výpočetní systémy