Verification of Automata with Storage Mechanisms / Köcher, Chris

Ilmenau : Universitätsverlag Ilmenau, 2023. - xii, 248 Seiten.

ISBN 978-3-86360-265-9
DOI 10.22032/dbt.53804
URN urn:nbn:de:gbv:ilm1-2022000388
Preis (Druckausgabe): 18,00 €

Zugl.: Dissertation, Technische Universität Ilmenau, 2022


An important question in computer science is to ask, whether a given system conforms to a specification. Often this question is equivalent to ask whether a finite automaton with certain memory like a stack or queue can reach some given state. In this thesis we focus this reachability problem of automata having one or more lossy or reliable stacks or queues as their memory. Unfortunately, the reachability problem is undecidable or of high complexity in most of these cases. We circumvent this by several approximation methods. So we extend the exploration algorithm by Boigelot and Godefroid under-approximating the reachability problem of queue automata. We also study some automata having multiple stacks with a restricted behavior. These “asynchronous pushdown systems” have an efficiently decidable reachability problem. To show our results we first have to gain knowledge of several algebraic properties of the so-called transformation monoid of the studied storage mechanisms.

Zugriff auf den Volltext über die dbt:

Druckfassung im Buchhandel lieferbar und z.B. über den folgenden Webshop direkt bestellbar!