Reachability Problems
5th International Workshop, RP 2011, Genoa, Italy, September 28-30, 2011, Proceedings
Published on 25. September 2011
XII, 245 pages
978-3-642-24288-5 (ISBN)
Description
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.
More details
Other editions
Additional editions
Giorgio Delzanno | Igor Potapov
Reachability Problems
5th International Workshop, RP 2011, Genoa, Italy, September 28-30, 2011, Proceedings
Book
09/2011
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- Title
- Preface
- Organization
- Table of Contents
- Graph Games with Reachability Objectives
- Observing Continuous-Time MDPs by 1-Clock Timed Automata
- Introduction
- Preliminaries
- CTMDP
- Single-Clock DTA
- Problem Statement
- Timed Reachability in CTMDP
- Product Construction
- Reduction to a Linear Programming Problem
- Conclusion
- References
- Automata for Monadic Second-Order Model-Checking
- References
- Reachability Problems for Hybrid Automata
- References
- Synthesis of Timing Parameters Satisfying Safety Properties
- Introduction
- The Inverse Method
- Optimized Algorithms Based on the Inverse Method
- Algorithm with State Inclusion in the Fixpoint
- Algorithm with Union of the Constraints
- Algorithm with Direct Return
- Combination: Inclusion in Fixpoint and Union
- Combination: Inclusion in Fixpoint and Direct Return
- Summary of the Algorithms
- Behavioral Cartography
- Implementation and Experiments
- Conclusion
- References
- Formal Language Constrained Reachability and Model Checking Propositional Dynamic Logics
- Introduction
- Preliminaries
- Applications
- The Connection between the Three Problems
- Forth and Back between Graphs and Formulas
- Forth and Back between Graphs and Formal Languages
- New Decidability and Complexity Results on Model Checking and Formal Language Constrained Reachability
- Summary
- References
- Completeness of the Bounded Satisfiability Problem for Constraint LTL
- Introduction
- Languages
- Symbolic Valuations
- Automaton Construction
- Extensions
- Bounded Satisfiability Problem
- Completeness Bound for CLTLB(D)
- Conclusions
- References
- Characterizing Conclusive Approximations by Logical Formulae
- Introduction
- Background and Notations
- Symbolic Tree Automata
- Solutions for Patterns in STA
- Finding a Conclusive Fix-Point Automaton
- Reachability Analysis via Logical Formula Solving
- Conclusion
- References
- Decidability of LTL for Vector Addition Systems with One Zero-Test
- Introduction
- Preliminaries
- Generalities
- Transition Systems
- Vector Addition Systems
- The LTL Logic
- Buchi Automata and LTL
- Model Checking
- Decidability of Repeated Control State Reachability
- Conclusion
- References
- Complexity Analysis of the Backward Coverability Algorithm for VASS
- Introduction
- Preliminaries
- Notations and Definitions
- Well-Quasi Orderings
- Vector Addition Systems with States (VASS)
- Coverability Problem and Rackoff's Upper Bound
- Complexity of the Backward Algorithm for Coverability
- Lower Bound
- Net Programs
- Proof of Theorem 3
- References
- Automated Termination in Model Checking Modulo Theories
- Introduction
- Preliminaries
- Array-Based Systems and Backward Reachability
- Closure under Pre-image Computation
- Wqo-Theories, QE-Degrees, and Termination
- Automated Termination
- An Application of Theorem 4.5: The Fischer Protocol
- Conclusions
- References
- Monotonic Abstraction for Programs with Multiply-Linked Structures
- Introduction
- Heaps
- Programming Language
- Signatures
- Bad Configurations
- Reachability Analysis
- Implementation and Experimental Results
- Conclusions and Future Work
- References
- Efficient Bounded Reachability Computation for Rectangular Automata
- Introduction
- Preliminaries
- Polyhedra and Their Computation
- Rectangular Automata
- A New Approach for Reachability Computation
- Facets of the Reachable Set Under Flow Transitions
- Compute the Reachable Set under Flow Transitions
- Compute the Reachable Set After a Jump
- Complexity of the Reachability Computation
- Experimental Results
- Conclusion
- References
- Reachability and Deadlocking Problems in Multi-stage Scheduling
- Introduction
- A Taxonomy of Job Processing Plans
- System States: Safe, Unsafe, and Deadlocks
- Deciding Safety: Easy Cases
- Deciding Safety: Hard Cases
- Reachability
- Reachable Deadlock
- References
- Improving Reachability Analysis of Infinite State Systems by Specialization
- Introduction
- Specifying Reactive Systems
- Constraint-Based Specialization of Reactive Systems
- Experimental Evaluation
- Related Work and Conclusions
- References
- Lower Bounds for the Length of Reset Words in Eulerian Automata
- Background and Overview
- Preliminaries
- Main Results
- References
- Parametric Verification and Test Coverage for Hybrid Automata Using the Inverse Method
- Introduction
- Related Work
- Hybrid Automata with Parameters
- Basic Definitions
- Symbolic Semantics
- Algorithm
- Inverse Method
- Behavioral Cartography
- Enhancement of the Method for Affine Dynamics
- Final Remarks
- References
- A New Weakly Universal Cellular Automaton in the 3D Hyperbolic Space with Two States
- Introduction
- The Railway Circuit
- A New Implementation in the Dodecagrid
- Representation of the Dodecagrid
- The New Tracks
- The New Switches
- The Scenario of the Simulation
- The Motion of the Particle
- Fixed Switches
- Flip-Flop Switches
- Memory Switches
- A Word about the Computer Program
- Conclusion
- References
- A Fully Symbolic Bisimulation Algorithm
- Introduction
- Background
- Deterministic Colored Labeled Transition Systems (DCLTSs)
- Bisimulation
- Quasi-Reduced Ordered Multi-way Decision Diagrams
- Saturation
- Symbolic Bisimulation
- Main Results
- Bisimulation Partition Refinement Relations
- Reduction of Deterministic Bisimulation to Set Closure
- Experimental Results
- Related Work
- Conclusions
- References
- Reachability for Finite-State Process Algebras Using Static Analysis
- Introduction
- The Process Algebra
- Data Flow Analysis
- Reachability Algorithm
- Determining Possible States
- Computing Reachable Labels
- Main Algorithm
- Algorithmic Complexity
- Conclusions
- References
- Author Index
