Reachability Problems: 6th International Workshop, RP 2012, Bordeaux, France, September 17-19, 2012. Proceedings (Lecture Notes in Computer Science (7550))

This book constitutes the refereed proceedings of the 6th International Workshop on Reachability Problems, RP 2012, held in Bordeaux, France, in September, 2012. The 8 revised full papers presented together with 4 invited talks were carefully reviewed and selected from 15 submissions. The papers present current research and original contributions related to reachability problems in different computational models and systems such as algebraic structures, computational models, hybrid systems, logic and verification. Reachability is a fundamental problem that appears in several different contexts: finite- and infinite-state concurrent systems, computational models like cellular automata and Petri nets, decision procedures for classical, modal and temporal logic, program analysis, discrete and continuous systems, time critical systems, and open systems modeled as games. Reachability Problems Title 1 Preface 4 Organization 7 Table of Contents 8 Fraenkel-Mostowski Sets with Non-homogeneous Atoms 10 Non-homogeneous Atoms 11 Integers with Order and Successor 12 Real Numbers with Order and Successor 13 References 14 Recursive Schemes, Krivine Machines, and Collapsible Pushdown Automata 15 Introduction 15 Basic Notions 17 Simply Typed Lambda Calculus and Recursive Schemes 17 Krivine Machines 20 Collapsible Pushdown Automata 21 From Y-Calculus to CPDA 22 Stackless Krivine Machines 23 Simulation 24 Lowering the Order 26 Conclusions 27 References 28 Decision Problems for Linear Recurrence Sequences 30 Introduction 30 Preliminaries 31 Linear Recurrence Sequences 31 Algebraic Numbers 32 The Skolem Problem 32 Decidability 32 Complexity 34 Variants and Reductions 34 Positivity and Ultimate Positivity 35 References 36 Playing Games with Counter Automata 38 Introduction 38 Preliminaries 39 Existing Results about Multi-counter Games 42 eVASS Games 42 Consumption Games 43 Multiweighted Energy Games 44 One-Counter Games and MDPs 45 Energy Markov Decision Processes 47 Solvency Games 48 Conclusions 48 References 49 LTL-Model-Checking via Model Composition 51 Introduction 51 Technical Preliminaries 53 Structures 53 Logics 54 Interface Information 55 Composition Theorem for LTL 55 Summary and Outlook 61 References 61 On the Relationship between Reachability Problems in Timed and Counter Automata 63 Introduction 63 Preliminaries 64 The General Case 66 The Case of Two Clocks and One Bounded Counter 69 Discussion 74 References 74 Smooth Sand Piles 75 Introduction 75 Preliminaries 76 The Model 79 Properties 80 The Complete Model 85 Conclusions 86 References 87 Ariadne: Dominance Checking of Nonlinear Hybrid Automata Using Reachability Analysis 88 Introduction 88 Automata and Evolution 89 Approximations to the Reachable Set 90 Outer Approximation 91 -Lower Approximation 92 Parametric Dominance Checking 93 The Water Tank Case Study 94 Conclusions 99 References 100 Robustness of Time Petri Nets under Guard Enlargement 101 Introduction 101 Preliminaries 103 Perturbations in TPN 105 Problems Considered 105 Examples of Non-robust TPNs 105 Sequential TPNs 107 Undecidability Results 108 A Robust Translation from TPN to TA 109 Robustly Bounded TPNs 111 Untimed Language Robustness in TPNs 113 Conclusion 114 References 115 Efficient Probabilistic Model Checking of Systems with Ranged Probabilities 116 Introduction 116 Preliminaries 117 Model Checking a DTMC 118 Model Checking of Bounded Properties 120 Approximate Model Checking 120 Bounding the First-Order Error Terms 124 Model Checking of Unbounded Properties 127 Case Study 128 Conclusion 128 References 129 On the Length of Knot Transformations via Reidemeister Moves I and II 130 Introduction 130 Discrete Representations of Knots and Formal Notations 131 Reidemeister Moves as Rewriting Rules 134 Reachability Properties of Reidemeister Moves I and II 136 Reachability by Type I 137 Reachability by Type II 140 Reachability by Combination of Types I and II 143 References 144 Invariants for LTI Systems with Uncertain Input 146 Introduction 146 Preliminaries 147 Real Canonical Form 147 System Decomposition 148 One-Dimensional Subsystems 148 Two-Dimensional Subsystems 149 Invariant Ellipsoids 149 Optimal Control 150 Combining the Results 151 Decomposition Method 152 Comparison 152 Linear Matrix Inequalities 153 Examples 154 Related Work 157 Conclusion and Outlook 157 References 157 Author Index 158 Front Matter....Pages - Fraenkel-Mostowski Sets with Non-homogeneous Atoms....Pages 1-5 Recursive Schemes, Krivine Machines, and Collapsible Pushdown Automata....Pages 6-20 Decision Problems for Linear Recurrence Sequences....Pages 21-28 Playing Games with Counter Automata....Pages 29-41 LTL-Model-Checking via Model Composition....Pages 42-53 On the Relationship between Reachability Problems in Timed and Counter Automata....Pages 54-65 Smooth Sand Piles....Pages 66-78 Ariadne: Dominance Checking of Nonlinear Hybrid Automata Using Reachability Analysis....Pages 79-91 Robustness of Time Petri Nets under Guard Enlargement....Pages 92-106 Efficient Probabilistic Model Checking of Systems with Ranged Probabilities....Pages 107-120 On the Length of Knot Transformations via Reidemeister Moves I and II....Pages 121-136 Invariants for LTI Systems with Uncertain Input....Pages 137-148 Back Matter....Pages - This book constitutes the proceedings of the 8th International Workshop on Reachability Problems, RP 2014, held in Oxford, UK, in September 2014. The papers offer new approaches for the modelling and analysis of computational processes by combining mathematical, algorithmic, and computational techniques. This book constitutes the refereed proceedings of the International Workshop on Augemented Environments for Computer-Assited Interventions, held in conjunction with MICCAI 2011, in Toronto, Canada, in September 2011.