Reachability Problems

Name: Reachability Problems | 9th International Workshop, RP 2015, Warsaw, Poland, September 21-23, 2015, Proceedings
Brand: Springer
Price: 42.79 EUR
Availability: OnlineOnly

9th International Workshop, RP 2015, Warsaw, Poland, September 21-23, 2015, Proceedings

Mikolai Bojanczyk Slawomir Lasota Igor Potapov(Herausgeber*in)

Springer (Verlag)

Erschienen am 12. Oktober 2015

XX, 179 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-319-24537-9 (ISBN)

42,79 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken