Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities

DOI10.1007/978-3-030-50086-3_9OpenAlexW3037699571MaRDI QIDQ5041280

Jeremy Sproston

Publication date: 13 October 2022

Published in: Formal Techniques for Distributed Objects, Components, and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-030-50086-3_9

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Markov and semi-Markov decision processes (90C40) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (1)

Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• What's decidable about hybrid automata?
• A theory of timed automata
• Bounded-parameter Markov decision processes
• Interval-valued finite Markov chains
• Automatic verification of real-time systems with discrete probability distributions.
• Model checking of open interval Markov chains
• Probabilistic timed automata with clock-dependent probabilities
• Qualitative reachability for open interval Markov chains
• On the complexity of model checking interval-valued discrete time Markov chains
• Model checking for probabilistic timed automata
• Reachability analysis of uncertain systems using bounded-parameter Markov decision processes
• Interval iteration algorithm for MDPs and IMDPs
• The complexity of reachability in parametric Markov decision processes
• Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties
• Stochastic Timed Automata
• Quantitative Multi-objective Verification for Probabilistic Systems
• Model Checking Real-Time Systems
• Model Checking One-clock Priced Timed Automata
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• The Complexity of Markov Decision Processes
• Stochastic Timed Games Revisited
• CONCUR 2004 - Concurrency Theory
• Robust Control of Markov Decision Processes with Uncertain Transition Matrices
• Model-Checking ω-Regular Properties of Interval Markov Chains
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities