Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties

DOI10.1007/978-3-319-99154-2_8zbMath1514.68132arXiv1712.00275OpenAlexW2963868694MaRDI QIDQ6104804

No author found.

Publication date: 28 June 2023

Published in: Quantitative Evaluation of Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1712.00275

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Cites Work

• Unnamed Item
• Unnamed Item
• State explosion in almost-sure probabilistic reachability
• Performance analysis of probabilistic timed automata using digital clocks
• A theory of timed automata
• Automatic verification of real-time systems with discrete probability distributions.
• On probabilistic timed automata.
• An extension of the inverse method to probabilistic timed automata
• Model checking for probabilistic timed automata
• Symbolic model checking for probabilistic timed automata
• Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata
• Fluid Model Checking of Timed Properties
• Measuring performance of continuous-time stochastic processes using timed automata
• Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata
• Efficient CTMC Model Checking of Linear Real-Time Objectives
• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• Concavely-Priced Probabilistic Timed Automata
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• Undecidability of Cost-Bounded Reachability in Priced Probabilistic Timed Automata
• Stochastic Games for Verification of Probabilistic Timed Automata
• The benefits of relaxing punctuality