On probabilistic timed automata.

DOI10.1016/S0304-3975(01)00215-8MaRDI QIDQ1853732zbMATH OpenOpenAlexFDO

Authors Danièle Beauquier

Publication date 22 January 2003

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0304-3975(01)00215-8

zbMATH Keywords

Markov decision processModel-checkingProbabilistic timed automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

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

Cites work

• scientific article; zbMATH DE number 4154239 (Why is no real title available?)
• A logic for reasoning about time and reliability
• A theory of timed automata
• Markov decision processes and regular events
• Model checking of probabilistic and nondeterministic systems
• On the complexity of finite memory policies for Markov decision processes
• Rational \(\omega\)-languages are non-ambiguous
• Testing and generating infinite sequences by a finite automaton
• The Complexity of Markov Decision Processes
• The complexity of probabilistic verification

Cited in

(19)

• A survey of timed automata for the development of real-time systems
• Probabilistic and Topological Semantics for Timed Automata
• Expected reachability-time games
• A maximal entropy stochastic process for a timed automaton
• Stochastic games for verification of probabilistic timed automata
• Stochastic timed automata
• State explosion in almost-sure probabilistic reachability
• Weak bisimulation for probabilistic timed automata
• Automatic verification of real-time systems with discrete probability distributions.
• A comparison of time- and reward-bounded probabilistic model checking techniques
• \(\mathrm{MDP + TA = PTA}\): probabilistic timed automata, formalized (short paper)
• Model checking for probabilistic timed automata
• Symbolic model checking for probabilistic timed automata
• Strict Divergence for Probabilistic Timed Automata
• Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
• Concavely-Priced Probabilistic Timed Automata
• Computing bisimilarity metrics for probabilistic timed automata
• Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata
• Probabilistic timed automata with one clock and initialised clock-dependent probabilities

This page was built for publication: On probabilistic timed automata.

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