Automatic verification of real-time systems with discrete probability distributions.
From MaRDI portal
Publication:1603709
DOI10.1016/S0304-3975(01)00046-9zbMath1050.68094MaRDI QIDQ1603709
Gethin Norman, Roberto Segala, Jeremy Sproston, Marta Kwiatkowska
Publication date: 15 July 2002
Published in: Theoretical Computer Science (Search for Journal in Brave)
Related Items (55)
Expected reachability-time games ⋮ Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities ⋮ Tweaking the odds in probabilistic timed automata ⋮ Parameter Synthesis for Probabilistic Timed Automata Using Stochastic Game Abstractions ⋮ Symbolic model checking for probabilistic timed automata ⋮ Probabilistic Real-Time Rewrite Theories and Their Expressive Power ⋮ Model Checking Probabilistic Systems ⋮ State explosion in almost-sure probabilistic reachability ⋮ Parameter synthesis for probabilistic timed automata using stochastic game abstractions ⋮ Concavely-Priced Probabilistic Timed Automata ⋮ Strict Divergence for Probabilistic Timed Automata ⋮ Performance analysis of probabilistic timed automata using digital clocks ⋮ Better abstractions for timed automata ⋮ Model Checking Linear-Time Properties of Probabilistic Systems ⋮ Weak bisimulation for probabilistic timed automata ⋮ A uniform framework for modeling nondeterministic, probabilistic, stochastic, or mixed processes and their behavioral equivalences ⋮ Verification and Control of Probabilistic Rectangular Hybrid Automata ⋮ Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata ⋮ Safety verification for probabilistic hybrid systems ⋮ A survey of timed automata for the development of real-time systems ⋮ \textsc{ULTraS} at work: compositionality metaresults for bisimulation and trace semantics ⋮ Probabilistic timed automata with clock-dependent probabilities ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ Combined model checking for temporal, probabilistic, and real-time logics ⋮ Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties ⋮ Bounded model checking for interval probabilistic timed graph transformation systems against properties of probabilistic metric temporal graph logic ⋮ Model checking HPnGs in multiple dimensions: representing state sets as convex polytopes ⋮ Formal verification and quantitative metrics of MPSoC data dynamics ⋮ Unnamed Item ⋮ Local abstraction refinement for probabilistic timed programs ⋮ Verification and control for probabilistic hybrid automata with finite bisimulations ⋮ Towards general axiomatizations for bisimilarity and trace semantics ⋮ Emptiness and Universality Problems in Timed Automata with Positive Frequency ⋮ Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata ⋮ An extension of the inverse method to probabilistic timed automata ⋮ Model checking for probabilistic timed automata ⋮ A compositional modelling and analysis framework for stochastic hybrid systems ⋮ Probabilistic timed graph transformation systems ⋮ Unnamed Item ⋮ Identity-Based Cryptosystems and Quadratic Residuosity ⋮ Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata ⋮ Consistency in parametric interval probabilistic timed automata ⋮ Unnamed Item ⋮ Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata ⋮ Probabilistic Time Petri Nets ⋮ Stochastic Games for Verification of Probabilistic Timed Automata ⋮ Performance analysis and functional verification of the stop-and-wait protocol in HOL ⋮ A note on the attractor-property of infinite-state Markov chains ⋮ Unnamed Item ⋮ Towards light-weight probabilistic model checking ⋮ A theory of stochastic systems. I: Stochastic automata ⋮ Calculating Probabilities of Real-Time Test Cases ⋮ On Verification of Linear Occurrence Properties of Real-Time Systems ⋮ Model checking for entanglement swapping ⋮ Interval probabilistic timed graph transformation systems
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Model-checking in dense real-time
- Bisimulation through probabilistic testing
- A theory of timed automata
- Symbolic model checking for real-time systems
- A logic for reasoning about time and reliability
- Uppaal in a nutshell
- Computer aided verification. 8th international conference, CAV '96, New Brunswick, NJ, USA, July 31 -- August 3, 1996. Proceedings
- Deciding bisimilarity and similarity for probabilistic processes.
- Model checking of probabilistic and nondeterministic systems
- Markov decision processes and regular events
This page was built for publication: Automatic verification of real-time systems with discrete probability distributions.
