Symbolic minimum expected time controller synthesis for probabilistic timed automata

DOI10.1007/978-3-319-22975-1_10zbMATH Open1465.68153OpenAlexW1760491810MaRDI QIDQ2945592FDOQ2945592

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

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

Mathematics Subject Classification ID

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

Cites Work

• Uppaal in a nutshell
• Title not available (Why is that?)
• Title not available (Why is that?)
• A theory of timed automata
• Automatic verification of real-time systems with discrete probability distributions.
• Symbolic model checking for probabilistic timed automata
• Symbolic minimum expected time controller synthesis for probabilistic timed automata
• Undecidability of Cost-Bounded Reachability in Priced Probabilistic Timed Automata
• Title not available (Why is that?)
• Checking timed Büchi automata emptiness efficiently
• An Analysis of Stochastic Shortest Path Problems
• Performance analysis of probabilistic timed automata using digital clocks
• Title not available (Why is that?)
• Stochastic games for verification of probabilistic timed automata
• Title not available (Why is that?)
• On time with minimal expected cost!
• Title not available (Why is that?)
• Title not available (Why is that?)
• An analysis of transient Markov decision processes
• Title not available (Why is that?)

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)