Tweaking the odds in probabilistic timed automata

DOI10.1007/978-3-030-85172-9_3MaRDI QIDQ832050zbMATH OpenOpenAlexFDO

Authors Arnd Hartmanns, Joost-Pieter Katoen, Bram Kohlen, Jip Spel

Publication date 24 March 2022

Full work available at URL https://doi.org/10.1007/978-3-030-85172-9_3

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60) Markov and semi-Markov decision processes (90C40)

Recommendations

• Parameter synthesis for probabilistic timed automata using stochastic game abstractions
• Parameter synthesis for probabilistic timed automata using stochastic game abstractions
• An extension of the inverse method to probabilistic timed automata
• \(\mathrm{MDP + TA = PTA}\): probabilistic timed automata, formalized (short paper)
• Model checking for probabilistic timed automata

Cites work

• scientific article; zbMATH DE number 1304998 (Why is no real title available?)
• scientific article; zbMATH DE number 700091 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A compositional modelling and analysis framework for stochastic hybrid systems
• A theory of timed automata
• AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA
• An extension of the inverse method to probabilistic timed automata
• Automatic verification of real-time systems with discrete probability distributions.
• Consistency in parametric interval probabilistic timed automata
• Iterative bounded synthesis for efficient cycle detection in parametric timed automata
• Linear parametric model checking of timed automata
• Model checking for probabilistic timed automata
• Model checking probabilistic real-time properties for service-oriented systems with service level agreements
• Model checking probabilistic systems
• Parameter synthesis for Markov models: faster than ever
• Parametric real-time reasoning
• Performance analysis of probabilistic timed automata using digital clocks
• Probabilistic model checking of AODV
• Statistical approximation of optimal schedulers for probabilistic timed automata
• Stochastic games for verification of probabilistic timed automata
• Strict Divergence for Probabilistic Timed Automata
• Symbolic model checking for probabilistic timed automata
• Synthesis in pMDPs: a tale of 1001 parameters
• The 10,000 facets of MDP model checking
• The complexity of reachability in parametric Markov decision processes
• What good are digital clocks?

Cited in

(8)

• Parameter synthesis for probabilistic timed automata using stochastic game abstractions
• An extension of the inverse method to probabilistic timed automata
• Symbolic minimum expected time controller synthesis for probabilistic timed automata
• \(\mathrm{MDP + TA = PTA}\): probabilistic timed automata, formalized (short paper)
• Parameter synthesis for probabilistic timed automata using stochastic game abstractions
• Parameter synthesis in Markov models: a gentle survey
• Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata
• Merge and conquer: state merging in parametric timed automata

Describes a project that uses

Uses Software

• Jani
• Uppaal
• MoDeST
• PRISM

This page was built for publication: Tweaking the odds in probabilistic timed automata

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