Contents

I BASIC NOTIONS 1

1 Introduction to Trace Theory 3 (A. Mazurkiewicz) 1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 Preliminary Notions . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.3 Dependency and Traces . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.4 Dependence Graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 1.5 Histories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 1.6 Ordering of Symbol Occurrences . . . . . . . . . . . . . . . . . . . . 21 1.7 Trace Languages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1.8 Elementary Net Systems . . . . . . . . . . . . . . . . . . . . . . . . . 33 1.9 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

2 Dependence Graphs 43 (H. J. Hoogeboom, G. Rozenberg) 2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 2.2 Preliminary Notions . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 2.3 Dependence Graphs via Words . . . . . . . . . . . . . . . . . . . . . 45 2.4 The Structure of Dependence Graphs . . . . . . . . . . . . . . . . . . 52 2.5 Transitive Closures . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 2.6 Graph Grammars . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64

II ALGEBRA AND COMBINATORICS 69

3 Combinatorics in Trace Monoids I 71 (C. Choffrut) 3.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 3.2 Equations in Two Unknowns . . . . . . . . . . . . . . . . . . . . . . 73 3.3 Conjugacy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 3.4 Related Topics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80

4 Combinatorics in Trace Monoids II 83 (G. Duchamp, D. Krob) 4.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 4.2 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 4.3 Elimination for Trace Monoids . . . . . . . . . . . . . . . . . . . . . 89 4.4 Lyndon Traces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 97 4.5 Shuffle Product . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 4.6 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 125 4.7 Some Remarks on Other Related Structures . . . . . . . . . . . . . . 127 4.8 Bibliographical Remarks . . . . . . . . . . . . . . . . . . . . . . . . . 128

5 Counting Techniques for Inclusion, Equivalence and Membership Problems 131 (A. Bertoni, M. Goldwurm, G. Mauri, N. Sabadini) 5.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132 5.2 Rational trace languages . . . . . . . . . . . . . . . . . . . . . . . . . 133 5.3 Formal series and generating functions . . . . . . . . . . . . . . . . . 136 5.4 Equivalence and Inclusion Problems . . . . . . . . . . . . . . . . . . 143 5.5 On counting the prefixes of a trace . . . . . . . . . . . . . . . . . . . 149

III LANGUAGES AND AUTOMATA 165

6 Recognizable Trace Languages 167 (E. Ochmański) 6.1 Monoids and Their Subsets . . . . . . . . . . . . . . . . . . . . . . . 168 6.2 Trace Monoids and Trace Languages . . . . . . . . . . . . . . . . . . 174 6.3 Recognizable Trace Languages . . . . . . . . . . . . . . . . . . . . . 178 6.4 The Star Problem . . . . . . . . . . . . . . . . . . . . . . . . . . . . 183 6.5 Morphisms on Trace Monoids . . . . . . . . . . . . . . . . . . . . . . 190 6.6 Petri Nets and Their Behaviour . . . . . . . . . . . . . . . . . . . . . 192 6.7 Labelled Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . . . . 196 6.8 Bibliographical Remarks . . . . . . . . . . . . . . . . . . . . . . . . . 203

7 Asynchronous Automata 205 (W. Zielonka) 7.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 205 7.2 Asynchronous Transition Systems . . . . . . . . . . . . . . . . . . . . 206 7.3 Non-interleaving Semantics of Asynchronous Transition Systems . . 212 7.4 Asynchronous Cellular Transition Systems . . . . . . . . . . . . . . . 228 7.5 Simulations Between Asynchronous Transition Systems . . . . . . . . 231 7.6 Language Recognizability by Asynchronous Automata . . . . . . . . 238 7.7 Bibliographical Remarks . . . . . . . . . . . . . . . . . . . . . . . . . 246

8 Construction of Asynchronous Automata 249 (V. Diekert, A. Muscholl) 8.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 249 8.2 Métivier’s Construction for Triangulated Dependence Graphs …. 252 8.3 Asynchronous Cellular Automata for Recognizable Trace Languages 257

8.4 Concluding Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . . 267

IV CONCURRENCY AND LOGIC 269

9 Trace Structures and other Models for Concurrency 271 (M. Nielsen, G. Winskel) 9.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 272 9.2 Trace Structures and Hoare Structures . . . . . . . . . . . . . . . . . 273 9.3 Trace Structures and Event Structures . . . . . . . . . . . . . . . . . 280 9.4 Trace Structures and Domains . . . . . . . . . . . . . . . . . . . . . 291 9.5 Trace Structures and Petri Nets . . . . . . . . . . . . . . . . . . . . . 293 9.6 Trace Structures and Asynchronous Transition Systems . . . . . . . 302 9.7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 305

10 Traces and Logic 307 (W. Penczek, R. Kuiper) 10.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 308 10.2 Trace Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 310 10.3 Comparison of Temporal Logics on Trace Systems . . . . . . . . . . 325 10.4 Efficient Model Checking for a Subset of LTL . . . . . . . . . . . . . 336 10.5 Efficient Model Checking for a Subset of CTL . . . . . . . . . . . . . 347 10.6 Model Checking for CTL_{P} . . . . . . . . . . . . . . . . . . . . . . . . 351 10.7 Proving Program Properties using ISTL_{P} . . . . . . . . . . . . . . . 361 10.8 Axiomatization of a Subset of Propositional ISTL_{P} . . . . . . . . . . 373 10.9 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 379 10.10 Appendix: Logical Definability of Trace Languages (W. Ebinger) . . 382

V GENERALIZATIONS 391

11 Infinite Traces 393 (P. Gastin, A. Petit) 11.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 394 11.2 Real and Transfinite Traces . . . . . . . . . . . . . . . . . . . . . . . 397 11.3 Poset Properties of Infinite Traces . . . . . . . . . . . . . . . . . . . 414 11.4 Complex Traces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 422 11.5 Topology on Complex Traces . . . . . . . . . . . . . . . . . . . . . . 434 11.6 Rational Languages of Infinite Traces . . . . . . . . . . . . . . . . . . 441 11.7 Recognizable Real Trace Languages . . . . . . . . . . . . . . . . . . . 455 11.8 Recognizable Complex Trace Languages . . . . . . . . . . . . . . . . 472 12 Semi-Commutations 487

(M. Clerbout, M. Latteux, Y. Roos) 12.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 488 12.2 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 489 12.3 Basic Lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 492 12.4 The Decomposition Theorem . . . . . . . . . . . . . . . . . . . . . . 496 12.5 A Composition Criterion . . . . . . . . . . . . . . . . . . . . . . . . . 500 12.6 Recognizability and Rationality . . . . . . . . . . . . . . . . . . . . . 509 12.7 Algebraic Rational Functions . . . . . . . . . . . . . . . . . . . . . . 528 12.8 Applications of Semi-Commutations . . . . . . . . . . . . . . . . . . 538 12.9 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 549

Bibliography 553