Reachability Problems: 5th International Workshop, RP 2011, Genoa, Italy, September 28-30, 2011, Proceedings

Front Cover
Giorgio Delzanno, Igor Potapov
Springer Science & Business Media, Sep 19, 2011 - Computers - 245 pages
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
Author Index
245
Copyright

Other editions - View all

Common terms and phrases