## Reachability Problems: 5th International Workshop, RP 2011, Genoa, Italy, September 28-30, 2011, ProceedingsGiorgio Delzanno, Igor Potapov This book constitutes the refereed proceedings of the 5th International Workshop on Reachability Problems, RP 2011, held in Genoa, Italy, in September 2011. The 16 papers presented together with 4 invited talks were carefully reviewed and selected from 24 submissions. The workshop deals with reachability problems that appear in 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 modelled as games. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

Graph Games with Reachability Objectives | 1 |

Observing ContinuousTime MDPs by 1Clock Timed Automata | 2 |

Automata for Monadic SecondOrder ModelChecking | 26 |

Reachability Problems for Hybrid Automata | 28 |

Synthesis of Timing Parameters Satisfying Safety Properties | 31 |

Formal Language Constrained Reachability and Model Checking Propositional Dynamic Logics | 45 |

Completeness of the Bounded Satisfiability Problem for Constraint LTL | 58 |

Characterizing Conclusive Approximations by Logical Formulae | 72 |

Monotonic Abstraction for Programs with MultiplyLinked Structures | 125 |

Efficient Bounded Reachability Computation for Rectangular Automata | 139 |

Reachability and Deadlocking Problems in Multistage Scheduling | 153 |

Improving Reachability Analysis of Infinite State Systems by Specialization | 165 |

Lower Bounds for the Length of Reset Words in Eulerian Automata | 180 |

Parametric Verification and Test Coverage for Hybrid Automata Using the Inverse Method | 191 |

A New Weakly Universal Cellular Automaton in the 3D Hyperbolic Space with Two States | 205 |

A Fully Symbolic Bisimulation Algorithm | 218 |

Decidability of LTL for Vector Addition Systems with One ZeroTest | 85 |

Complexity Analysis of the Backward Coverability Algorithm for VASS | 96 |

Automated Termination in Model Checking Modulo Theories | 110 |

Reachability for FiniteState Process Algebras Using Static Analysis | 231 |

245 | |

### Other editions - View all

### Common terms and phrases

abstraction algorithm automaton backward reachability Bellman equation bisimulation bounded cell 13 cellular automaton clock CLTLB(D complexity Computer Science constraint constraint logic programs context-sensitive languages CTMDP data structures decidable deﬁned Deﬁnition Delzanno denote doubly-linked lists edge equivalent example exists ﬁnite formal formal languages formula function gchains given graph heap Heidelberg hybrid automata hybrid systems implemented infinite initial instantiation integer inverse method languages Lemma linear LNCS logic machine model checking node NP-hard operator parameter valuation partition path Petri net Potapov Eds predicate processing plans Proof reachability analysis reachability problem regular languages reset word safety properties satisfiability problem schedulers Section semantics sequence sig1 signature Springer symbolic valuations techniques termination Theorem tiles trace sets track transition relation transition system tree automata tree automaton tuple unsafe upward-closed variables VASS0 vector verification vertex zero-test