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

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

Marta Kwiatkowska, Gethin Norman, Quentin Peyras, 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 checking; controller synthesis; probabilistic timed automata; probabilistic verification

Mathematics Subject Classification ID

68Q45: Formal languages and automata

68Q60: Specification and verification (program logics, model checking, etc.)

68Q87: Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)

Uses Software

• PRISM
• Uppaal
• PPL