Reachability Problems : 13th International Conference, RP 2019, Brussels, Belgium, September 11{u2013}13, 2019, Proceedings

This book constitutes the refereed proceedings of the 13th International Conference on Reachability Problems, RP 2019, held in Brussels, Belgium, in September 2019. The 14 full papers presented were carefully reviewed and selected from 26 submissions. The papers cover topics such as reachability for infinite state systems; rewriting systems; reachability analysis in counter/timed/cellular/communicating automata; Petri nets; computational aspects of semigroups, groups, and rings; reachability in dynamical and hybrid systems; frontiers between decidable and undecidable reachability problems; complexity and decidability aspects; predictability in iterative maps; and new computational paradigms. -- Provided by publisher Preface 6 Organization 9 Abstracts of Invited Talks 10 Bidding Games on Markov Decision Processes 11 The Reachability Problem for Petri Nets is Not Elementary 12 Primitivity and Synchronizing Automata: A Functional Analytic Approach 13 Game Graphs for Reactive Synthesis 14 Reaching Out Towards Fully Verified Autonomous Systems 15 Contents 16 Bidding Games on Markov Decision Processes 18 1 Introduction 18 2 Preliminaries 21 3 Qualitative Bidding Games on MDPs 22 4 Mean-Payoff Bidding Games on Strongly-Connected MDPs 24 5 Discussion 28 References 28 Primitivity and Synchronizing Automata: A Functional Analytic Approach 30 1 Introduction 30 2 Contraction Operators and Reachability Theorems 31 3 Contractive Families and Functional Equations 33 4 m-primitivity and m-syncronising Automata 34 References 37 Reaching Out Towards Fully Verified Autonomous Systems 39 1 Introduction 39 2 Preliminaries: Neural Networks 40 2.1 Neural Networks 40 3 Verification of Neural Networks 42 3.1 Abstract Interpretation for Neural Networks 43 3.2 Training with Robustness 44 3.3 Closed Loop Verification 44 3.4 Falsification and Testing 45 4 Challenges 45 5 Conclusion 47 References 47 On the m-eternal Domination Number of Cactus Graphs 50 1 Introduction 50 2 The m-eternal Domination of Christmas Cactus Graphs 53 3 Upper Bound on the m-eternal Domination Number of Cactus Graphs 57 4 Linear-Time Algorithm 60 5 Future Work 63 References 63 On Relevant Equilibria in Reachability Games 65 1 Introduction 65 2 Preliminaries and Studied Problems 68 3 Existence Problems 71 4 Solving Decision Problems 72 4.1 -Consistent Play 73 4.2 Characterizations 73 4.3 Sufficiency of Lassoes 75 4.4 Algorithms 76 4.5 Results 77 References 78 Partial Solvers for Generalized Parity Games 80 1 Introduction 80 2 Preliminaries 82 3 Zielonka's Algorithm with Partial Solvers 84 4 Algorithms BüchiSolver and GenBüchiSolver 85 5 Algorithms GoodEpSolver and GenGoodEpSolver 87 6 Algorithms LaySolver and GenLaySolver 90 7 Empirical Evaluation 92 References 94 Reachability in Augmented Interval Markov Chains 96 1 Introduction 96 2 Preliminaries 98 3 Qualitative Case 99 4 Quantitative Case: Upper Bound 102 5 Quantitative Case: Lower Bound 104 6 Approximate Case 106 References 108 On Solving Word Equations Using SAT 110 1 Introduction 110 2 Preliminaries 111 3 Word Equation Solving 113 3.1 Solving Bounded Word Equation 113 3.2 Refining Bounds and Guiding the Search 117 4 Experiments 120 5 Conclusion 122 References 122 Parameterised Verification of Publish/Subscribe Networks with Exception Handling 124 1 Introduction 124 2 Formal Model of Pub/Sub Architectures 127 2.1 Pub/Sub Networks 128 3 Example: Specification of an IoT System 129 4 The Coverability Decision Problem 131 4.1 Decision Procedure for Coverability in Pub/Sub Networks 132 5 Notification with Retained Messages 133 6 Handling Exceptions During Notifications 134 7 Conclusions 136 References 137 Cellular Automata for the Self-stabilisation of Colourings and Tilings 138 1 Introduction 138 2 Setting of the Problem 139 3 The Case of 2-Colourings 141 3.1 Directional Self-stabilisation by a Deterministic CA 141 3.2 Isotropic Self-stabilisation by a Probabilistic CA 142 3.3 Extension to Finite SFT 143 4 The Case of k-Colourings, for k5 144 4.1 Directional Self-stabilisation by a Deterministic CA 144 4.2 Isotropic Self-stabilisation by a Probabilistic CA 144 4.3 Extension to Single-Site Fillable Proximity Tilings 145 5 The Case of 4-Colourings 145 5.1 Directional Self-stabilisation by a Deterministic CA that Corrects by Blocks 145 5.2 Isotropic Self-stabilisation by a Probabilistic CA 147 5.3 Extension to -Fillable Proximity Tilings 148 6 The Case of 3-Colourings 149 6.1 Necessity to Correct Arbitrarily Far from the Locations of Errors 149 6.2 Deterministic Self-stabilisation by a CA with Additional States 150 7 Conclusion 152 References 152 On the Termination Problem for Counter Machines with Incrementing Errors 154 1 Introduction 154 2 Preliminaries 155 3 Results 157 4 Discussion 163 References 164 Reachability Problems on Partially Lossy Queue Automata 166 1 Introduction 166 2 Preliminaries 167 2.1 Words and Languages 167 2.2 Automata 168 3 Queues and Queue Automata 169 4 Behavioral Equivalence 171 5 Read-Write Independence 172 6 Partially Lossy Queues 177 7 Conclusion 179 References 180 On the Computation of the Minimal Coverability Set of Petri Nets 181 1 Introduction 181 2 Preliminaries 183 2.1 Markings, -markings and Labelled Trees 184 2.2 Petri Nets 184 2.3 Minimal Coverability Set of Petri Nets 185 3 Presentation of the Monotone-Pruning Algorithm 185 3.1 Acceleration(s) 185 3.2 Definition of the Algorithm 186 4 Structure of the Proof of Correction of MetapostAlgorithm 187 4.1 Widened Petri Nets 188 4.2 Structure of the Proof of Correction Presented in RS13 189 5 Completeness of MetapostAlgorithm for WPN 189 5.1 Coherence of an Acceleration 189 5.2 New Proof 191 6 Coherence of the Acceleration Accone 192 7 Conclusion 193 References 193 Deciding Reachability for Piecewise Constant Derivative Systems on Orientable Manifolds 195 1 Introduction 195 2 Preliminaries 197 2.1 Piecewise Constant Derivative Systems on a Plane 197 2.2 Trajectories 198 2.3 Reachability Problem 199 3 Piecewise Constant Derivative Systems on Manifolds 200 4 Dynamical Systems on the Closed Orientable Surfaces 201 5 Language of PCDr2m 204 6 Decidability of Reachability for PCDr2m 206 6.1 Rauzy Graphs 206 6.2 Deciding Reachability of PCDr2m 207 7 Conclusions 208 References 208 Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with Resets 210 1 Introduction 210 2 Pushdown Vector Addition Systems with Resets 212 3 Reduction from Minsky Machines 212 3.1 Preliminaries 212 3.2 Construction 214 4 Concluding Remarks 215 A Proof of Proposition 2 216 References 217 Synthesis of Structurally Restricted b-bounded Petri Nets: Complexity Results 219 1 Introduction 219 2 Preliminaries 220 3 Our Contribution 223 3.1 The Reduction and the Proof of Condition 1.1 and Condition2.2 225 3.2 The Proof of Condition1.2 and Condition2.2 229 3.3 The Proof of Theorem1.4 232 4 Conclusion 233 References 233 Reachability of Five Gossip Protocols 235 1 Introduction 235 2 Terminology for Gossip Protocols and Reachability 238 3 Reachability 241 4 Subreachability, Unorderded Distributions 245 5 Further Research: Parallel Gossip 247 References 248 Author Index 249 Front Matter ....Pages i-xx Bidding Games on Markov Decision Processes (Guy Avni, Thomas A. Henzinger, Rasmus Ibsen-Jensen, Petr Novotný)....Pages 1-12 Primitivity and Synchronizing Automata: A Functional Analytic Approach (Vladimir Yu. Protasov)....Pages 13-21 Reaching Out Towards Fully Verified Autonomous Systems (Sriram Sankaranarayanan, Souradeep Dutta, Sergio Mover)....Pages 22-32 On the m-eternal Domination Number of Cactus Graphs (Václav Blažej, Jan Matyáš Křišt’an, Tomáš Valla)....Pages 33-47 On Relevant Equilibria in Reachability Games (Thomas Brihaye, Véronique Bruyère, Aline Goeminne, Nathan Thomasset)....Pages 48-62 Partial Solvers for Generalized Parity Games (Véronique Bruyère, Guillermo A. Pérez, Jean-François Raskin, Clément Tamines)....Pages 63-78 Reachability in Augmented Interval Markov Chains (Ventsislav Chonev)....Pages 79-92 On Solving Word Equations Using SAT (Joel D. Day, Thorsten Ehlers, Mitja Kulczynski, Florin Manea, Dirk Nowotka, Danny Bøgsted Poulsen)....Pages 93-106 Parameterised Verification of Publish/Subscribe Networks with Exception Handling (Giorgio Delzanno)....Pages 107-120 Cellular Automata for the Self-stabilisation of Colourings and Tilings (Nazim Fatès, Irène Marcovici, Siamak Taati)....Pages 121-136 On the Termination Problem for Counter Machines with Incrementing Errors (Christopher Hampson)....Pages 137-148 Reachability Problems on Partially Lossy Queue Automata (Chris Köcher)....Pages 149-163 On the Computation of the Minimal Coverability Set of Petri Nets (Pierre-Alain Reynier, Frédéric Servais)....Pages 164-177 Deciding Reachability for Piecewise Constant Derivative Systems on Orientable Manifolds (Andrei Sandler, Olga Tveretina)....Pages 178-192 Coverability Is Undecidable in One-Dimensional Pushdown Vector Addition Systems with Resets (Sylvain Schmitz, Georg Zetzsche)....Pages 193-201 Synthesis of Structurally Restricted b-bounded Petri Nets: Complexity Results (Ronny Tredup)....Pages 202-217 Reachability of Five Gossip Protocols (Hans van Ditmarsch, Malvin Gattinger, Ioannis Kokkinis, Louwe B. Kuijer)....Pages 218-231 Back Matter ....Pages 233-233 This book constitutes the refereed proceedings of the 7th International Workshop on Reachability Problems, RP 2013, held in Uppsala, Sweden, in September 2013. The 19 revised papers (The 14 revised papers were carefully reviewed and selected from 24 submissions in addition to 5 invited talks) were carefully reviewed and selected from 24 submissions. Topics of interest include reachability for finite state systems; rewriting systems, reachability analysis in counter/timed/cellular/communicating automata; Petri-nets; computational aspects of semigroups, groups and rings; reachability in dynamical and hybrid systems; frontiers between decidable and undecidable reachability problems; complexity and decidability aspects, predictability in iterative maps and new computational paradigms.