On Determinism in Modal Transition Systems
| Název česky | O determinismu v modálních přechodových systémech |
|---|---|
| Autoři | |
| Rok publikování | 2009 |
| Druh | Článek v odborném periodiku |
| Časopis / Zdroj | Theoretical Computer Science |
| Fakulta / Pracoviště MU | |
| Citace | |
| Obor | Informatika |
| Klíčová slova | compositional verification; modal transition systems; determinism; refinement; consistency |
| Přiložené soubory | |
| Popis | Modální přechodové systémy (MTS) jsou formalismus rozšiřující klasické označkované přechodové systémy zavedením přechodů dvou typů: must přechody, které musí být přítomny v každé implementaci a may přechody, které jsou povolené, ale nikoli vyžadované. Rámec MTS se prokázal být užitečným formalismem pro specifikaci komponentových systémů, protože podporuje kompozicionální verifikaci a postupné zjemňování. Nicméně tato teorie má i své limity: přirozeně definované pojmy modálního zjemnění a modální kompozice jsou neúplné vzhledem k sémantice založené na množinách implementací dané MTS specifikace. Nedávné výsledky však naznačují, že tyto potíže mohou být překonány uvážením deterministických systémů, které se zdají více zvladatelné, ale stále zajímavé pro řadu praktických oblastí. V tomto článku podáváme ucelenou studii MTS v deterministickém rámci. Studujeme řadu problémů dříve uvažovaných na MTS a ukazujeme, do jaké míry můžeme očekávat lepší výsledky při restrikci na determinismus. |
| Související projekty: |