Symbolic model checking for probabilistic timed automata

DOI10.1016/J.IC.2007.01.004zbMATH Open1122.68075OpenAlexW2095602520MaRDI QIDQ2373877FDOQ2373877

Authors: Marta Kwiatkowska, Gethin Norman, Jeremy Sproston, 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

Recommendations

• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Model checking for probabilistic timed automata
• Validation of Stochastic Systems
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• Model Checking Probabilistic Timed Automata with One or Two Clocks

zbMATH Keywords

discrete probability distributions

Mathematics Subject Classification ID

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

Cites Work

• Title not available (Why is that?)
• Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k
• A theory of timed automata
• Symbolic model checking: \(10^{20}\) states and beyond
• Title not available (Why is that?)
• Model-checking in dense real-time
• A logic for reasoning about time and reliability
• Model checking of probabilistic and nondeterministic systems
• Symbolic model checking for real-time systems
• Automatic verification of real-time systems with discrete probability distributions.
• On probabilistic timed automata.
• Finite state Markovian decision processes
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• A classification of symbolic transition systems
• Title not available (Why is that?)
• Formal Modeling and Analysis of Timed Systems
• Termination of Probabilistic Concurrent Program
• Probabilistic model checking of deadline properties in the IEEE 1394 fireWire root contention protocol
• Title not available (Why is that?)
• TCTL inevitability analysis of dense-time systems

Cited In (51)

• A survey of timed automata for the development of real-time systems
• Branching-time model-checking of probabilistic pushdown automata
• Foundations of Software Science and Computational Structures
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Probabilistic and Topological Semantics for Timed Automata
• Minimal counterexamples for linear-time probabilistic verification
• Theoretical Aspects of Computing – ICTAC 2005
• Tweaking the odds in probabilistic timed automata
• Simulation and Bisimulation for Probabilistic Timed Automata
• Probabilistic timed graph transformation systems
• Abstraction and approximation in fuzzy temporal logics and models
• Constraint Markov chains
• Symbolic model checking for probabilistic processes
• Expected reachability-time games
• Stochastic differential dynamic logic for stochastic hybrid programs
• Local abstraction refinement for probabilistic timed programs
• Stochastic games for verification of probabilistic timed automata
• Statistical approximation of optimal schedulers for probabilistic timed automata
• Symbolic verification and strategy synthesis for linearly-priced probabilistic timed automata
• Superposition-based analysis of first-order probabilistic timed automata
• Farkas certificates and minimal witnesses for probabilistic reachability constraints
• Parameter synthesis for probabilistic timed automata using stochastic game abstractions
• Probabilistic model checking of deadline properties in the IEEE 1394 fireWire root contention protocol
• Probabilistic NetKAT
• Distributed parametric model checking timed automata under non-zenoness assumption
• An extension of the inverse method to probabilistic timed automata
• Symbolic Simulation-Checking of Dense-Time Automata
• Performance analysis of probabilistic timed automata using digital clocks
• Formal Modeling and Analysis of Timed Systems
• Automatic verification of real-time systems with discrete probability distributions.
• Symbolic computing in probabilistic and stochastic analysis
• On probabilistic timed automata.
• Symbolic minimum expected time controller synthesis for probabilistic timed automata
• Statistical Model Checking for Networks of Priced Timed Automata
• Minimal Witnesses for Probabilistic Timed Automata
• Model checking for probabilistic timed automata
• Strict Divergence for Probabilistic Timed Automata
• Expressiveness and conciseness of timed automata for the verification of stochastic models
• Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• Concavely-Priced Probabilistic Timed Automata
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• Title not available (Why is that?)
• Symbolic Analysis for GSMP Models with One Stateful Clock
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• Validation of Stochastic Systems
• Probabilistic model checking of the CSMA/CD protocol using PRISM and APMC
• ExplicitPRISMSymm: symmetry reduction technique for explicit models in PRISM
• Formal verification and quantitative metrics of MPSoC data dynamics
• Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata
• Title not available (Why is that?)

Uses Software

• PRISM
• Kronos
• Uppaal2k

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2373877)