Model Checking Probabilistic Timed Automata with One or Two Clocks

DOI10.1007/978-3-540-71209-1_15zbMath1186.68295OpenAlexW1894019848MaRDI QIDQ5758106

Jeremy Sproston, François Laroussinie, Marcin Jurdziński

Publication date: 3 September 2007

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71209-1_15

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (9)

Reachability games with relaxed energy constraints ⋮ Synthesis for Multi-weighted Games with Branching-Time Winning Conditions ⋮ A survey on temporal logics for specifying and verifying real-time systems ⋮ Model checking and synthesis for branching multi-weighted logics ⋮ Controller synthesis for dynamic hierarchical real-time plants using timed automata ⋮ Unnamed Item ⋮ Infinite Runs in Weighted Timed Automata with Energy Constraints ⋮ On timed alternating simulation for concurrent timed games ⋮ Unnamed Item

This page was built for publication: Model Checking Probabilistic Timed Automata with One or Two Clocks