Partially-commutative context-free graphs
Wojciech Krzysztof Czerwinski · 2013
The theme of this dissertation is the class of partially-commutative contextfree graphs. It is a computation model, which reflects both recursive and concurrent behaviour of programs. In the field of automatic verification and analysis of programs there is a strong need for systems, which have capability to model various aspects of programs and additionally have good algorithmic properties. It seems, that we are still on the beginning of the way to obtain efficient automatic verification. However, some techniques are already used in the industry. Results shown in this thesis are divided into two main parts. The first one focuses on expressivity of investigated model, while the second one presents methods of its analysis. The algorithmic part considers the reachability problem and the bisimulation problem.