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

• 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
• 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?)
• 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

(52)

• Probabilistic model checking of deadline properties in the IEEE 1394 fireWire root contention protocol
• Automatic verification of real-time systems with discrete probability distributions.
• Formal verification and quantitative metrics of MPSoC data dynamics
• On probabilistic timed automata.
• 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
• Expected reachability-time games
• Probabilistic NetKAT
• Statistical approximation of optimal schedulers for probabilistic timed automata
• Probabilistic model checking of the CSMA/CD protocol using PRISM and APMC
• Symbolic minimum expected time controller synthesis for probabilistic timed automata
• ExplicitPRISMSymm: symmetry reduction technique for explicit models in PRISM
• Statistical Model Checking for Networks of Priced Timed Automata
• Concavely-Priced Probabilistic Timed Automata
• Strict Divergence for Probabilistic Timed Automata
• Symbolic computing in probabilistic and stochastic analysis
• Symbolic Simulation-Checking of Dense-Time Automata
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• Simulation and Bisimulation for Probabilistic Timed Automata
• Symbolic Analysis for GSMP Models with One Stateful Clock
• Stochastic games for verification of probabilistic timed automata
• 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
• scientific article; zbMATH DE number 1759607 (Why is no real title available?)
• Symbolic model checking for probabilistic processes
• Superposition-based analysis of first-order probabilistic timed automata
• Farkas certificates and minimal witnesses for probabilistic reachability constraints
• Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata
• Stochastic differential dynamic logic for stochastic hybrid programs
• Symbolic verification and strategy synthesis for linearly-priced probabilistic timed automata
• Validation of Stochastic Systems
• Theoretical Aspects of Computing – ICTAC 2005
• Probabilistic and Topological Semantics for Timed Automata
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Constraint Markov chains
• Foundations of Software Science and Computational Structures
• Formal Modeling and Analysis of Timed Systems
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• scientific article; zbMATH DE number 7333236 (Why is no real title available?)
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
• Distributed parametric model checking timed automata under non-zenoness assumption
• Minimal Witnesses for Probabilistic Timed Automata
• Dense integer-complete synthesis for bounded parametric timed automata
• Expressiveness and conciseness of timed automata for the verification of stochastic models
• Tweaking the odds in probabilistic timed automata
• Performance analysis of probabilistic timed automata using digital clocks

Describes a project that uses

Uses Software

• Kronos
• Uppaal2k
• 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)