Parameterized complexity of some problems in concurrency and verification
M. Praveen · INFLIBNET · 2011
Formal methods for the analysis of concurrent systems is an active area of research. Many mathematical models like Petri nets, communicating automata, automata with auxiliary storage like counters and stacks, rewrite systems and process algebras have been proposed for modelling concurrent in nite state systems. E cient algorithms for analysis and the power to express interesting properties of concurrent systems are con icting goals in these models. Having too much expressiveness results in undecidability, so it is important to get an insight into what kind of restrictions will lead to good analysis algorithms while retaining some expressive power. Restrictions like reversal boundedness in counter automata, disallowing cycles in network of push-down systems etc. lead to decidability in the respective models. In this thesis, we propose to use the framework of parameterized complexity to study the e ect of various restrictions on the complexity of problems related to some models and logics of concurrent systems. Parameterized complexity works by trying to nd e cient algorithms for instances of hard problems where one can identify structure that helps in analysis. A numerical parameter is associated with problem instances and algorithms are designed whose time and/or memory requirement is a fast growing function of the parameter, but growing slowly in terms of the size of the instance. On instances where the parameter is small, such algorithms run e ciently. Apart from providing e cient algorithms, parameterized complexity provides a mathematically rigorous way of studying ner structure of the models under analysis. In the rst part of this thesis, we look at the e ect of well known graph parameters treewidth and pathwidth on the parameterized complexity of satis ability of some logics used to specify properties of nite state concurrent systems. This is followed by parameterized complexity of some problems associated with synchronized transition systems and 1-safe Petri nets, which are compactly represented nite state systems. In the second part of the thesis, we look at general Petri nets (which are in nite state) and study the parameterized complexity of coverability, boundedness and extensions of these problems with respect to two parameters.