Symbolic minimum expected time controller synthesis for probabilistic timed automata

DOI10.1007/978-3-319-22975-1_10MaRDI QIDQ2945592zbMATH OpenOpenAlexFDO

Authors Marta Kwiatkowska, Gethin Norman, Aleksandra Ž. Jovanović

Publication date 14 September 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-22975-1_10

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Synthesis problems (93B50)

Recommendations

• Symbolic optimal expected time reachability computation and 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
• Tweaking the odds in probabilistic timed automata
• Symbolic verification and strategy synthesis for linearly-priced probabilistic timed automata

Cites work

• scientific article; zbMATH DE number 3126094 (Why is no real title available?)
• scientific article; zbMATH DE number 3543391 (Why is no real title available?)
• scientific article; zbMATH DE number 1303059 (Why is no real title available?)
• scientific article; zbMATH DE number 1361118 (Why is no real title available?)
• scientific article; zbMATH DE number 1095138 (Why is no real title available?)
• scientific article; zbMATH DE number 1796156 (Why is no real title available?)
• scientific article; zbMATH DE number 1794367 (Why is no real title available?)
• scientific article; zbMATH DE number 7333236 (Why is no real title available?)
• A theory of timed automata
• An Analysis of Stochastic Shortest Path Problems
• An analysis of transient Markov decision processes
• Automatic verification of real-time systems with discrete probability distributions.
• Checking timed Büchi automata emptiness efficiently
• On time with minimal expected cost!
• Performance analysis of probabilistic timed automata using digital clocks
• Stochastic games for verification of probabilistic timed automata
• Symbolic minimum expected time controller synthesis for probabilistic timed automata
• Symbolic model checking for probabilistic timed automata
• Undecidability of Cost-Bounded Reachability in Priced Probabilistic Timed Automata
• Uppaal in a nutshell

Cited in

(5)

• Expected reachability-time games
• Parameter synthesis for probabilistic timed automata using stochastic game abstractions
• Symbolic minimum expected time controller synthesis for probabilistic timed automata
• Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
• Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata

This page was built for publication: Symbolic minimum expected time controller synthesis for probabilistic timed automata

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