Performance analysis of probabilistic timed automata using digital clocks

DOI10.1007/s10703-006-0005-2zbMath1105.68063OpenAlexW2028827800MaRDI QIDQ853731

N. E. Zubov

Publication date: 17 November 2006

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: http://eprints.gla.ac.uk/43789/1/43789.pdf

zbMATH Keywords

Timed automataDigital clocksProbabilistic model checking

Mathematics Subject Classification ID

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

Related Items (31)

Tweaking the odds in probabilistic timed automata ⋮ Parameter Synthesis for Probabilistic Timed Automata Using Stochastic Game Abstractions ⋮ Synthesizing efficient systems in probabilistic environments ⋮ Performance Model Checking Scenario-Aware Dataflow ⋮ Parameter synthesis for probabilistic timed automata using stochastic game abstractions ⋮ Concavely-Priced Probabilistic Timed Automata ⋮ Strict Divergence for Probabilistic Timed Automata ⋮ A game-based abstraction-refinement framework for Markov decision processes ⋮ Compositional probabilistic verification through multi-objective model checking ⋮ Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata ⋮ Verification and Control of Partially Observable Probabilistic Real-Time Systems ⋮ Value iteration for simple stochastic games: stopping criterion and learning algorithm ⋮ Probabilistic timed automata with clock-dependent probabilities ⋮ Statistical model checking of stochastic component-based systems ⋮ Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties ⋮ Unnamed Item ⋮ Verification and control of partially observable probabilistic systems ⋮ Abstract model repair for probabilistic systems ⋮ Formal verification and quantitative metrics of MPSoC data dynamics ⋮ Local abstraction refinement for probabilistic timed programs ⋮ Verification and control for probabilistic hybrid automata with finite bisimulations ⋮ 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 ⋮ Formal Analysis of Publish-Subscribe Systems by Probabilistic Timed Automata ⋮ Consistency in parametric interval probabilistic timed automata ⋮ Statistical Approximation of Optimal Schedulers for Probabilistic Timed Automata ⋮ Deciding probabilistic bisimilarity distance one for probabilistic automata ⋮ Unnamed Item ⋮ Stochastic Games for Verification of Probabilistic Timed Automata ⋮ Model checking for entanglement swapping

Uses Software

• PRISM
• Kronos
• Rabbit
• Uppaal2k
• Uppaal

Cites Work

• Model-checking in dense real-time
• 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.
• Uppaal in a nutshell
• Timing verification by successive approximation
• Finite state Markovian decision processes
• Model checking of probabilistic and nondeterministic systems
• An Analysis of Stochastic Shortest Path Problems
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Formal Modeling and Analysis of Timed Systems
• Formal Modeling and Analysis of Timed Systems
• Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Performance analysis of probabilistic timed automata using digital clocks