Model checking for probabilistic timed automata
From MaRDI portal
Publication:2248072
DOI10.1007/s10703-012-0177-xzbMath1291.68265OpenAlexW2086673120MaRDI QIDQ2248072
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
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
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