
Reachability Problems
Description
Alles über E-Books | Antworten auf Fragen rund um E-Books, Kopierschutz und Dateiformate finden Sie in unserem Info- & Hilfebereich.
More details
Other editions
Additional editions

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
System requirements
File format: PDF
Copy protection: Watermark-DRM (Digital Rights Management)
System requirements:
- Computer (Windows; MacOS X; Linux): Use the free software Adobe Reader, Adobe Digital Editions, or any other PDF viewer of your choice (see eBook Help).
- Tablet/Smartphone (Android; iOS): Install the free app Adobe Digital Editions or another reading app for eBooks, e.g., PocketBook (see eBook Help).
- E-reader: Bookeen, Kobo, Pocketbook, Sony, Tolino and many more (only limited: Kindle).
The file format PDF always displays a book page identically on any hardware. This makes PDF suitable for complex layouts such as those used in textbooks and reference books (images, tables, columns, footnotes). Unfortunately, on the small screens of e-readers or smartphones, PDFs are rather annoying, requiring too much scrolling.
This eBook uses Watermark-DRM, a „soft” copy protection. This means that there are no technical restrictions to prevent illegal distribution. However, there is a personalised watermark embedded in the eBook that can be used to identify the purchaser of the eBook in the event of misuse and to provide evidence for legal purposes.
For more information, see our eBook Help page.