Symbolic model checking for probabilistic timed automata

DOI10.1016/J.IC.2007.01.004MaRDI QIDQ2373877zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

discrete probability distributions

Mathematics Subject Classification ID

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

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

Cites work

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

Cited in

(51)

• A survey of timed automata for the development of real-time systems
• Branching-time model-checking of probabilistic pushdown automata
• Minimal counterexamples for linear-time probabilistic verification
• 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
• Tweaking the odds in probabilistic timed automata
• Theoretical Aspects of Computing – ICTAC 2005
• Probabilistic timed graph transformation systems
• Simulation and Bisimulation for Probabilistic Timed Automata
• Abstraction and approximation in fuzzy temporal logics and models
• Constraint Markov chains
• Expected reachability-time games
• Symbolic model checking for probabilistic processes
• Local abstraction refinement for probabilistic timed programs
• Stochastic differential dynamic logic for stochastic hybrid 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
• Automatic verification of real-time systems with discrete probability distributions.
• Formal Modeling and Analysis of Timed Systems
• 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
• Symbolic Analysis for GSMP Models with One Stateful Clock
• scientific article; zbMATH DE number 7333236 (Why is no real title available?)
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata
• 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
• Validation of Stochastic Systems
• scientific article; zbMATH DE number 1759607 (Why is no real title available?)

Describes a project that uses

Uses Software

• Uppaal2k
• Kronos
• PRISM

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)