Model checking for probabilistic timed automata

DOI10.1007/s10703-012-0177-xzbMath1291.68265OpenAlexW2086673120MaRDI QIDQ2248072

Yanyan Li

Publication date: 30 June 2014

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2318/143907

zbMATH Keywords

probabilistic timed automataprobabilistic model checkingprobabilistic real-time systems

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)

Related Items (16)

A counter abstraction technique for verifying properties of probabilistic swarm systems ⋮ Expected reachability-time games ⋮ Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities ⋮ Tweaking the odds in probabilistic timed automata ⋮ Model Checking Probabilistic Systems ⋮ Verification and Control of Partially Observable Probabilistic Real-Time Systems ⋮ Probabilistic timed automata with clock-dependent probabilities ⋮ Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties ⋮ Verification and control of partially observable probabilistic systems ⋮ Symbolic checking of fuzzy CTL on fuzzy program graph ⋮ Unnamed Item ⋮ Preface to the special issue on probabilistic model checking ⋮ Probabilistic Time Petri Nets ⋮ Zone-based verification of timed automata: extrapolations, simulations and what next? ⋮ Model checking for entanglement swapping ⋮ Timed games with bounded window parity objectives

Uses Software

• PRISM
• Kronos
• Rabbit
• MoDeST
• MRMC
• UPPAAL TIGA

Cites Work

• Optimal paths in weighted timed automata
• A game-based abstraction-refinement framework for Markov decision processes
• Model-checking in dense real-time
• Interactive Markov chains. And the quest for quantified quality
• Checking timed Büchi automata emptiness efficiently
• Performance analysis of probabilistic timed automata using digital clocks
• Bisimulation through probabilistic testing
• A theory of timed automata
• Symbolic model checking for real-time systems
• A logic for reasoning about time and reliability
• Time-abstracted bisimulation: Implicit specifications and decidability
• Probabilistic model checking of deadline properties in the IEEE 1394 fireWire root contention protocol
• Automatic verification of real-time systems with discrete probability distributions.
• On probabilistic timed automata.
• Updatable timed automata
• An extension of the inverse method to probabilistic timed automata
• Symbolic model checking for probabilistic timed automata
• Optimal infinite scheduling for multi-priced timed automata
• Model checking of probabilistic and nondeterministic systems
• Concavely-Priced Probabilistic Timed Automata
• Strict Divergence for 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
• What good are digital clocks?
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Model checking for probabilistic timed automata