Symbolic model checking for probabilistic timed automata

DOI10.1016/j.ic.2007.01.004zbMath1122.68075MaRDI 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

68Q45: Formal languages and automata

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

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

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