Parameterized complexity of some problems in concurrency and verification[HBNI Th39]

Abstract

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 infinite state systems. Efficient algorithms for analysis and the power to express interesting properties of concurrent systems are conflicting 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 effect of various restrictions on the complexity of problems related to some models and logics of concurrent systems. Parameterized complexity works by trying to find efficient 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 efficiently. Apart from providing efficient algorithms, parameterized complexity provides a mathematically rigorous way of studying finer structure of the models under analysis. In the first part of this thesis, we look at the effect of well known graph parameters treewidth and pathwidth on the parameterized complexity of satisfiability of some logics used to specify properties of finite 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 finite state systems. In the second part of the thesis, we look at general Petri nets (which are infinite state) and study the parameterized complexity of coverability, boundedness and extensions of these problems with respect to two parameters.