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(Editor)

Springer (Publisher)

Published on 12. October 2015

XX, 179 pages

E-Book

PDF with digital watermarking

System requirements

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

€42.79incl. 7% vat

System requirements

for PDF with digital watermarking

E-Book Single Licence

Available for download

Description

More details

Other 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

Save as PDF Copy link into clipboard

Schweitzer Fachinformationen

Reachability Problems

Description

More details

Other editions

Additional editions

Persons

Content

System requirements