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 | |
| 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 | |
| Citace | |
| Doi | https://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: |