Efficient symbolic analysis of bounded Petri nets using interval decision diagrams [Elektronische Ressource] / vorgelegt von Alexey A. Tovchigrechko

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.