Termination Time of Vector Addition Systems with States /
Vector Addition Systems with States (VASS) jsou důležitým modelem pro souběžné procesy, paralelní programy a parametrizované systémy. Mohou být také použity jako model programů za účelem získání odhadů na času a/nebo prostor, které tyto programy mohou vyžadovat. V této dizertační práci se zaměřujeme...
Uloženo v:
| Hlavní autor: | |
|---|---|
| Další autoři: | |
| Typ dokumentu: | VŠ práce nebo rukopis |
| Jazyk: | Angličtina |
| Vydáno: |
2022
|
| Témata: | |
| On-line přístup: | https://is.muni.cz/th/d9zyd/ |
| Shrnutí: | Vector Addition Systems with States (VASS) jsou důležitým modelem pro souběžné procesy, paralelní programy a parametrizované systémy. Mohou být také použity jako model programů za účelem získání odhadů na času a/nebo prostor, které tyto programy mohou vyžadovat. V této dizertační práci se zaměřujeme na získání odhadů na dobu terminace VASS a jejich rozšíření, zejména stochastické rozšíření a hry na VASS, přičemž klademe důraz na lineární dobu terminace. Uvažujeme obě krajní varianty nedeterminismu, andělskou a démonickou. Andělský (démonický) nedeterminismus je vyřešen co největším snížením (zvýšením) doby terminace. Výsledky naší práce jsou následující. Pro démonické VASS představíme polynomiální algoritmus, který rozhoduje, zda je terminace lineární. Ukážeme, že pokud doba terminace není lineární, je alespoň kvadratická. Také ukážeme, že každý VASS, který má lineárně ohraničené čítače buď neterminuje, nebo má polynomiální dobu terminace, kde nejnižší stupeň polynomu ohraničující dob Vector Addition Systems with States (VASS) are a fundamental model for concurrent processes, parallel programs, and parametrised systems. They can be also used as models of programs for obtaining bounds on the time and/or space needed by the program. In this thesis, we focus on determining the bounds on the termination time of VASS and their extensions, namely VASS MDPs and VASS games, with an emphasis on the linear termination. We consider both angelic and demonic nondeterminism. Here, the angelic (demonic) nondeterminism is resolved by lowering (increasing) the termination time as much as possible. Our contributions are as follows. For demonic VASS, we give a polynomial time algorithm for deciding whether it has linear termination complexity. We show that if the termination complexity is not linear then it is at least quadratic. We show that every VASS with linearly bounded counters is either non-terminating or it has a polynomial termination time where the degree of the polynomial |
|---|---|
| Popis jednotky: | Vedoucí práce: Tomáš Brázdil |
| Fyzický popis: | vii, 160 stran : ilustrace |