Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata

DOI10.1016/j.tcs.2017.01.015zbMath1359.68171OpenAlexW2587449885WikidataQ112268306 ScholiaQ112268306MaRDI QIDQ517046

Quentin Peyras, Marta Kwiatkowska, Gethin Norman, Aleksandra Ž. Jovanović

Publication date: 16 March 2017

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: http://eprints.gla.ac.uk/134444/7/134444.pdf

zbMATH Keywords

symbolic model checkingcontroller synthesisprobabilistic timed automataprobabilistic verification

Mathematics Subject Classification ID

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

Related Items (2)

Parameter synthesis for probabilistic timed automata using stochastic game abstractions ⋮ Verification and control for probabilistic hybrid automata with finite bisimulations

Uses Software

• PRISM
• Uppaal
• PPL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Expected reachability-time games
• Model-checking in dense real-time
• Checking timed Büchi automata emptiness efficiently
• Performance analysis of probabilistic timed automata using digital clocks
• A theory of timed automata
• Symbolic model checking for real-time systems
• Automatic verification of real-time systems with discrete probability distributions.
• On probabilistic timed automata.
• Uppaal in a nutshell
• Symbolic model checking for probabilistic timed automata
• Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata
• Verification and Control of Partially Observable Probabilistic Real-Time Systems
• Model checking of probabilistic and nondeterministic systems
• Concavely-Priced Probabilistic Timed Automata
• Reachability in MDPs: Refining Convergence of Value Iteration
• On Time with Minimal Expected Cost!
• Undecidability of Cost-Bounded Reachability in Priced Probabilistic Timed Automata
• Stochastic Games for Verification of Probabilistic Timed Automata
• An Analysis of Stochastic Shortest Path Problems
• An analysis of transient Markov decision processes

This page was built for publication: Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata