Strict Divergence for Probabilistic Timed Automata

DOI10.1007/978-3-642-04081-8_41MaRDI QIDQ3184704zbMATH OpenOpenAlexFDO

Authors Jeremy Sproston

Publication date 22 October 2009

Published in CONCUR 2009 - Concurrency Theory (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-04081-8_41

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)

Recommendations

• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Symbolic model checking for probabilistic timed automata
• On probabilistic timed automata.
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• Model Checking Probabilistic Timed Automata with One or Two Clocks

Cites work

• A logic for reasoning about time and reliability
• A theory of timed automata
• Alternating-time temporal logic
• Automatic verification of real-time systems with discrete probability distributions.
• Checking timed Büchi automata emptiness efficiently
• Computer Science Logic
• scientific article; zbMATH DE number 1670788 (Why is no real title available?)
• scientific article; zbMATH DE number 176728 (Why is no real title available?)
• scientific article; zbMATH DE number 3240812 (Why is no real title available?)
• Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
• Model checking of probabilistic and nondeterministic systems
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• Model-checking in dense real-time
• On probabilistic timed automata.
• Performance analysis of probabilistic timed automata using digital clocks
• Real-time system = discrete system + clock variables
• State explosion in almost-sure probabilistic reachability
• Symbolic model checking for probabilistic timed automata
• Symbolic model checking for real-time systems
• The element of surprise in timed games.
• Trading Infinite Memory for Uniform Randomness in Timed Games

Cited in

(5)

• Model checking for probabilistic timed automata
• Combined model checking for temporal, probabilistic, and real-time logics
• A Maximal Entropy Stochastic Process for a Timed Automaton,
• Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
• Tweaking the odds in probabilistic timed automata

This page was built for publication: Strict Divergence for Probabilistic Timed Automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3184704)