Symbolic model checking for probabilistic timed automata

DOI10.1016/j.ic.2007.01.004zbMath1122.68075OpenAlexW2095602520MaRDI QIDQ2373877

Gethin Norman, Jeremy Sproston, Marta Kwiatkowska, Fuzhi Wang

Publication date: 16 July 2007

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2007.01.004

zbMATH Keywords

discrete probability distributions

Mathematics Subject Classification ID

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

Related Items (25)

Expected reachability-time games ⋮ Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints ⋮ Tweaking the odds in probabilistic timed automata ⋮ Parameter synthesis for probabilistic timed automata using stochastic game abstractions ⋮ Concavely-Priced Probabilistic Timed Automata ⋮ Strict Divergence for Probabilistic Timed Automata ⋮ Symbolic computing in probabilistic and stochastic analysis ⋮ Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata ⋮ ExplicitPRISMSymm: Symmetry Reduction Technique for Explicit Models in PRISM ⋮ A survey of timed automata for the development of real-time systems ⋮ Minimal counterexamples for linear-time probabilistic verification ⋮ Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties ⋮ Distributed parametric model checking timed automata under non-zenoness assumption ⋮ Formal verification and quantitative metrics of MPSoC data dynamics ⋮ Local abstraction refinement for probabilistic timed programs ⋮ 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 ⋮ Probabilistic timed graph transformation systems ⋮ Constraint Markov chains ⋮ Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs ⋮ Probabilistic NetKAT ⋮ Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata ⋮ Stochastic Games for Verification of Probabilistic Timed Automata ⋮ Abstraction and approximation in fuzzy temporal logics and models

Uses Software

• PRISM
• Kronos
• Uppaal2k

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model-checking in dense real-time
• Symbolic model checking: \(10^{20}\) states and beyond
• A theory of timed automata
• Symbolic model checking for real-time systems
• A logic for reasoning about time and reliability
• 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.
• Finite state Markovian decision processes
• Model checking of probabilistic and nondeterministic systems
• TCTL Inevitability Analysis of Dense-Time Systems
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Termination of Probabilistic Concurrent Program
• A classification of symbolic transition systems
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Formal Modeling and Analysis of Timed Systems
• Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k

This page was built for publication: Symbolic model checking for probabilistic timed automata