La lecture en ligne est gratuite
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres
Télécharger Lire

Advanced STG decomposition [Elektronische Ressource] / vorgelegt von Mark Schäfer

230 pages
AdvancedSTGDecompositionDissertation zur Erlangung des Grades einesDoktors der Naturwissenschaften (Dr. rer. nat)der Fakult¨at fu¨r Angewandte Informatikder Universit¨at AugsburgVorgelegt vonMark Sch¨aferGutachterErstgutachter: Prof. Dr. Walter VoglerZweitgutachter: Prof. Dr. Bernhard M¨ollerMu¨ndliche Pru¨fung28. Februar 2008To my wife Maren and my daughter CharlotteI would like to thank everybody who supported and entertained meduring this four years and all the years before.Thank you all!Brina, as ever — Elmar, for explaining objects — Frank, for pizzaGabriele, for all that libraries — Heinz, for bed and breakfast — Hilli, for smokingJan & Thomas, for ma¨a¨a¨a¨a¨a¨h — Jonathan & Victor, for many discussionsJu¨rgen, for da brainz — Minna, for math — Peter, for the gamesStephan, for the ketchup — Ute, for the fun — Walter, for being senseiWerner, for showing the way — Willi, for weldingAdvanced STG DecompositionAdvancedSTGDecompositionMark SchaeferUniversity of AugsburgBibliografische Information der Deutschen NationalbibliothekDie Deutsche Nationalbibliothek verzeichnet diese Publikation in derDeutschenNationalbibliografie; detaillierte bibliografische DatensindimInternet ub¨ er http://dnb.d-nb.de abrufbar.°c 2008 Mark Schaefermark@markschaefer.deHerstellung und VerlagBooks on Demand GmbH, NorderstedtISBN: 978-3-8370-4604-5CONTENTSContents1 Introduction 111.1 Scope . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
Voir plus Voir moins

Advanced
STG
Decomposition
Dissertation zur Erlangung des Grades eines
Doktors der Naturwissenschaften (Dr. rer. nat)
der Fakult¨at fu¨r Angewandte Informatik
der Universit¨at Augsburg
Vorgelegt von
Mark Sch¨aferGutachter
Erstgutachter: Prof. Dr. Walter Vogler
Zweitgutachter: Prof. Dr. Bernhard M¨oller
Mu¨ndliche Pru¨fung
28. Februar 2008To my wife Maren and my daughter Charlotte
I would like to thank everybody who supported and entertained me
during this four years and all the years before.
Thank you all!
Brina, as ever — Elmar, for explaining objects — Frank, for pizza
Gabriele, for all that libraries — Heinz, for bed and breakfast — Hilli, for smoking
Jan & Thomas, for ma¨a¨a¨a¨a¨a¨h — Jonathan & Victor, for many discussions
Ju¨rgen, for da brainz — Minna, for math — Peter, for the games
Stephan, for the ketchup — Ute, for the fun — Walter, for being sensei
Werner, for showing the way — Willi, for weldingAdvanced STG DecompositionAdvanced
STG
Decomposition
Mark Schaefer
University of AugsburgBibliografische Information der Deutschen Nationalbibliothek
Die Deutsche Nationalbibliothek verzeichnet diese Publikation in der
DeutschenNationalbibliografie; detaillierte bibliografische Datensindim
Internet ub¨ er http://dnb.d-nb.de abrufbar.
?c 2008 Mark Schaefer
mark@markschaefer.de
Herstellung und Verlag
Books on Demand GmbH, Norderstedt
ISBN: 978-3-8370-4604-5CONTENTS
Contents
1 Introduction 11
1.1 Scope . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.3 Contribution and Organisation . . . . . . . . . . . . . . . . . . . . . . 13
2 Asynchronous Circuits 15
2.1 Digital Circuits . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.1.1 Sequential Circuits . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.1.2 Synchronous Circuits . . . . . . . . . . . . . . . . . . . . . . . . 18
2.2 Asynchronous Circuits . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.2.1 Timing Assumptions . . . . . . . . . . . . . . . . . . . . . . . . 24
2.2.2 Operating Modes . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.2.3 Handshake Circuits. . . . . . . . . . . . . . . . . . . . . . . . . 27
3 Basic Definitions 31
3.1 Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.1.1 Labelled Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . 35
3.1.2 Implicit and Redundant Places . . . . . . . . . . . . . . . . . . 38
3.1.3 Unfoldings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3.2 Signal Transition Graphs . . . . . . . . . . . . . . . . . . . . . . . . . 40
3.2.1 State Graph and Complete State Coding . . . . . . . . . . . . 43
3.2.2 Parallel Composition, Renaming and Hiding . . . . . . . . . . . 47
3.3 Decomposition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
3.3.1 Purpose . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
3.3.2 Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
3.4 Properties of Transition Contractions . . . . . . . . . . . . . . . . . . . 65
3.5 Some Considerations about Consistency . . . . . . . . . . . . . . . . . 70
74 Determinate Decomposition 75
4.1 Redundant Places in Marked Graphs . . . . . . . . . . . . . . . . . . . 76
4.2 Determinacy of Petri Net Operations . . . . . . . . . . . . . . . . . . . 81
4.2.1 Decomposition as Reduction System . . . . . . . . . . . . . . . 81
4.2.2 Reduction is Locally Confluent . . . . . . . . . . . . . . . . . . 83
5 Internal Signals 95
5.1 Extended Correctness Definition . . . . . . . . . . . . . . . . . . . . . 96
5.2 Hierarchical Decomposition . . . . . . . . . . . . . . . . . . . . . . . . 100
5.3 CSC Solving. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 108
5.4 Comparison with other Approaches . . . . . . . . . . . . . . . . . . . . 114
5.5 Other Implementation Relations . . . . . . . . . . . . . . . . . . . . . 116
5.5.1 Conformance . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117
5.5.2 I/O-Compatibility . . . . . . . . . . . . . . . . . . . . . . . . . 119
5.5.3 Strictness of Inclusions . . . . . . . . . . . . . . . . . . . . . . . 121
6 Advanced Decomposition Strategies 123
6.1 Correctness of New Strategies . . . . . . . . . . . . . . . . . . . . . . . 124
6.2 Reordering Transition Contractions . . . . . . . . . . . . . . . . . . . . 125
6.3 Lazy Backtracking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125
6.4 Tree Decomposition . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130
6.4.1 Component Aggregation . . . . . . . . . . . . . . . . . . . . . . 134
6.5 Undo Stack and Self-Triggering . . . . . . . . . . . . . . . . . . . . . . 135
6.6 CSC-Aware Decomposition . . . . . . . . . . . . . . . . . . . . . . . . 135
6.6.1 CSC-Aware Decomposition . . . . . . . . . . . . . . . . . . . . 137
6.6.2 Safeness-Preserving Contractions . . . . . . . . . . . . . . . . . 141
6.6.3 Implicit Places and Dynamic Auto-Conflicts . . . . . . . . . . . 146
6.7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147
6.7.1 Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 147
6.7.2 Application to other Decomposition Approaches . . . . . . . . 157
6.7.3 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 158
7 Output-Determinacy 161
7.1 Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 163
7.1.1 Output-Determinacy . . . . . . . . . . . . . . . . . . . . . . . . 165
7.2 Decomposition into Output-Determinate Comp. . . . . . . . . . . . . . 169
7.2.1 Valid STG transformations . . . . . . . . . . . . . . . . . . . . 173
7.2.2 New Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . 181
7.3 Output-Determinacy and Internal Signals . . . . . . . . . . . . . . . . 185
7.4 Results. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 188