Deciding Fast Termination for Probabilistic VASS with Nondeterminism
DOI10.1007/978-3-030-31784-3_27zbMath1437.68127arXiv1907.11010OpenAlexW2981444511MaRDI QIDQ3297606
Krishnendu Chatterjee, Tomáš Brázdil, Petr Novotný, Dominik Velan, Antonín Kučera
Publication date: 20 July 2020
Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1907.11010
Analysis of algorithms and problem complexity (68Q25) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A unified approach for deciding the existence of certain petri net paths
- The covering and boundedness problems for vector addition systems
- On the hardness of analyzing probabilistic programs
- Automated recurrence analysis for almost-linear expected-runtime bounds
- Non-polynomial worst-case analysis of recursive programs
- The complexity of multi-mean-payoff and multi-energy games
- Parallel program schemata
- Probabilistic NetKAT
- Complexity Hierarchies beyond Elementary
- Hyperplane Separation Technique for Multidimensional Mean-Payoff Games
- Generalized Mean-payoff and Energy Games
- An SMT-Based Approach to Coverability Analysis
- Model Checking of Recursive Probabilistic Systems
- Approximating the Termination Value of One-Counter MDPs and Stochastic Games
- ON YEN'S PATH LOGIC FOR PETRI NETS
- Minimizing Expected Termination Time in One-Counter Markov Decision Processes
- Complexity Analysis of the Backward Coverability Algorithm for VASS
- Fixed-Dimensional Energy Games are in Pseudo-Polynomial Time
- Liveness of Parameterized Timed Networks
- An Algorithm for the General Petri Net Reachability Problem
- Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms
- Proving Differential Privacy via Probabilistic Couplings
- Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
- The reachability problem for Petri nets is not elementary
- SPEED
- Model Checking Probabilistic Pushdown Automata
- Markov Decision Processes with Multiple Long-run Average Objectives
- Vector addition system reachability problem
- Multivariate amortized resource analysis
- Efficient Analysis of Probabilistic Programs with an Unbounded Counter
This page was built for publication: Deciding Fast Termination for Probabilistic VASS with Nondeterminism