
Reachability Problems
Description
Alles über E-Books | Antworten auf Fragen rund um E-Books, Kopierschutz und Dateiformate finden Sie in unserem Info- & Hilfebereich.
This
book constitutes the refereed proceedings of the 9th International
Workshop on Reachability Problems, RP 2015, held in Warsaw, Poland, in
September 2015. The 14 papers presented together with 6 extended
abstracts in this volume were carefully reviewed and selected from 23
submissions. The papers cover a range of topics in
the field of 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.
More details
Other editions
Additional editions

Persons
Content
- Intro
- Preface
- Organization
- Abstracts of Invited Talks
- Modeling and Co-design of Control Tasks OverWireless Networking Protocols: Stateof the Art and Challenges
- Vector Addition Systems Howto
- Recent Results on ConcurrentReachability Games
- Horn Constraints with Quantifiersand Cardinalities
- Reachability Problems for Continuous LinearDynamical Systems
- Reasoning About Cost-Utility Constraintsin Probabilistic Models
- Contents
- Reasoning About Cost-Utility Constraints in Probabilistic Models
- References
- Integer-Complete Synthesis for Bounded Parametric Timed Automata
- 1 Introduction
- 2 Preliminaries
- 2.1 Clocks, Parameters and Constraints
- 2.2 Parametric Timed Automata
- 3 Parametric Extrapolation
- 4 Integer-Complete Dense Parametric Algorithms
- 4.1 Parametric Reachability: RIEF
- 4.2 Parametric Unavoidability: RIAF
- 4.3 Implementation in Romo
- 5 Conclusion
- References
- Polynomial Interrupt Timed Automata
- 1 Introduction
- 2 Polynomial ITA
- 3 Cylindrical Decomposition and Reachability
- 3.1 Definition
- 3.2 Reachability for PolITA
- 4 Effective Construction and on-the-fly Algorithm
- 4.1 Construction of a Cylindrical Decomposition
- 4.2 On-the-fly Algorithm
- 5 Conclusion and Discussion
- References
- Irregular Behaviours for Probabilistic Automata
- 1 Introduction
- 2 Preliminaries
- 3 A Universally Non-regular Probabilistic Automaton
- 4 Main Result
- References
- Reachability in Succinct One-Counter Games
- 1 Introduction
- 2 Preliminaries
- 2.1 Arenas, Plays, and Strategies
- 2.2 One-Counter Systems
- 2.3 Winning Conditions
- 3 Equivalence of Models and Problems
- 3.1 Removing the Guards
- 3.2 Removing Negative Counter Values
- 3.3 From Reachability to Counter Reachability
- 4 EXPSPACE-completeness of Succinct One-Counter Games
- 4.1 Upper Bound
- 4.2 Lower Bounds
- 5 Conclusion and Further Work
- References
- On Reachability-Related Games on Vector Addition Systems with States
- 1 Introduction
- 1.1 Strategies, Winning Strategies, Winning Regions Win, Win
- 2 Reducing GIC-parity-eVASS to GIC-eVASS
- 3 A Direct Proof of Theorem 1
- 3.1 Mixing -Strategies, and Pruning -Transitions
- 3.2 Detecting Nonnegative Cycles, and Their (Exponential) Lengths
- 3.3 Attractor-Based Algorithm for the GIC-parity-eVASS Problem
- References
- A Topological Method for Finding Invariant Sets of Continuous Systems
- 1 Introduction
- 2 Some Basics of Dynamical Systems Theory
- 3 Isolating Blocks: Algebraic Conditions
- 4 A Simple Combinatorial Condition for Proving the Existence of (Non-empty) Invariant Sets
- 5 Experiments
- 6 Conclusion and Future Work
- References
- The Ideal View on Rackoff's Coverability Technique
- 1 Introduction
- 2 Preliminaries
- 2.1 Well-Structured Transition Systems
- 2.2 Ideal Decompositions
- 3 Backward Coverability
- 3.1 Generic Algorithm
- 3.2 Coverability for VAS and Reset VAS
- 3.3 Ackermann Upper Bounds
- 4 Complexity for VAS
- 4.1 Transitions Between Proper Ideals
- 4.2 omega-Monotonicity
- 4.3 Upper Bound
- 5 Concluding Remarks
- References
- Synthesis Problems for One-Counter Automata
- 1 Introduction
- 2 Complexity of RPAD
- 3 Decidable Properties of One-Counter Automata
- 3.1 Weighted Graphs and Flow Networks
- 3.2 One-Counter Automata
- 3.3 Reachability for Parametric 1-CA
- 3.4 Translating Büchi and LTL Synthesis to RPAD
- 3.5 Complexity
- 4 A Lower Bound for Büchi Synthesis
- 5 Conclusion
- References
- On Boundedness Problems for Pushdown Vector Addition Systems
- 1 Introduction
- 2 Preliminaries
- 3 Grammar-Controlled Vector Addition Systems
- 4 Certificates of Unboundedness
- 5 Growing Patterns
- 6 Small Certificates
- 7 Conclusion
- References
- Multithreaded-Cartesian Abstract Interpretation of Multithreaded Recursive Programs Is Polynomial
- 1 Introduction
- 2 Related Work
- 3 Programs
- 4 Multithreaded-Cartesian Abstract Interpretation
- 5 Model-Checking Recursive Multithreaded Programs
- 5.1 Inference System TMR
- 5.2 Interpretation of the Output of TMR
- 5.3 Computing Multithreaded-Cartesian Semantics
- 6 Model-Checking General Multithreaded Programs
- 7 Proof of Theorem 1
- 7.1 Soundness: Left Componentwise Inclusion in (2)
- 7.2 Completeness: Right Componentswise Inclusion in (2)
- 7.3 Combining the Left and Right Inclusions
- 8 Conclusion
- References
- Over-Approximating Terms Reachable by Context-Sensitive Rewriting
- 1 Introduction
- 2 Preliminaries
- 3 Computing Context-Sensitive Descendants
- 3.1 Closure Under Context-Sensitive Rewriting
- 3.2 Normalization
- 3.3 Initialization
- 3.4 Simplification
- 3.5 Reduction
- 3.6 Completion
- 4 Examples
- 5 Related Work
- 6 Further Work
- References
- Reducing Bounded Realizability Analysis to Reachability Checking
- 1 Introduction
- 2 Realizability and Bounded Realizability
- 2.1 Reactive Systems and Environments
- 2.2 Reactive System Specifications
- 2.3 Realizability
- 2.4 Bounded Realizability
- 2.5 Procedure for Bounded Realizability Checking
- 3 Reachability-Based Bounded Nonemptiness Checking for UCT
- 3.1 Universal co-Büchi Tree Automata(UCT)
- 3.2 Characterization for Transition Machines of Size k Accepted by UCT
- 3.3 SAT Encoding
- 3.4 Incremental Checking
- 4 Complexity of Bounded Realizability Problem
- 4.1 Upper Bound
- 4.2 Lower Bound
- 4.3 Discussion
- 5 Experiments
- 6 Related Works
- 7 Conclusion
- References
- Rearranging Two Dimensional Arrays by Prefix Reversals
- 1 Introduction
- 2 Rearrangement of Two Dimensional Arrays
- 2.1 Prefix Reversals
- 2.2 Reachability Problem
- 2.3 Elementary Operations
- 3 Reachable Arrays
- 3.1 n = 2
- 3.2 n = 1,3 (mod 4)
- Horizontal Transposition of (k+1, 1) and (k+1, 2) Entries.
- Transposition of Entries on Arbitrary Positions.
- 3.3 n = 2 (mod 4)
- Vertical Transposition of (2k+1, 1) and (2k+2, 1) Entries.
- Transposition of Entries of Arbitrary Positions.
- 4 Unreachable Arrays
- 4.1 Unreachability of (E4h4k) for Any Odd Permutation
- 4.2 Reachability of (E4h4k) for Any Even Permutation
- 5 Upper Bound of Prefix Reversals
- References
- The Emptiness Problem for Valence Automata Or: Another Decidable Extension of Petri Nets
- 1 Introduction
- 2 Preliminaries
- 3 Results
- 4 Proof of the Characterization
- 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.