Efficient Symbolic Analysis ofBounded Petri Nets UsingInterval Decision DiagramsVon der Fakultät fürMathematik, Naturwissenschaften und Informatikder Brandenburgischen Technischen Universität Cottbuszur Erlangung des akademischen GradesDoktor der Naturwissenschaften(Dr.rer.nat.)genehmigte Dissertationvorgelegt vonDipl.-Math. Alexey A. Tovchigrechkogeboren am 15.3.1978in Krasnoarmeisk, Moskau Gebiet, RußlandGutachter: Prof. Dr.-Ing. Monika HeinerGutachter: Prof. Dr. habil. François FagesGutachter: Prof. Dr. rer. nat. Kurt LautenbachTag der mündlichen Prüfung: 16.10.2008Contents1 Introduction 51.1 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51.2 Motivation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71.3 Organization of Thesis and Contributions . . . . . . . . . . . . . . . . . 72 Petri Nets 112.1 Definition of P/T Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122.2 Dynamic Behavior of P/T Nets . . . . . . . . . . . . . . . . . . . . . . . 142.3 Reachability Graph . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162.4 Basic Petri Nets Properties . . . . . . . . . . . . . . . . . . . . . . . . . 182.4.1 Boundedness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 182.4.2 Reachability Problem . . . . . . . . . . . . . . . . . . . . . . . . 202.4.3 Liveness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 202.4.