Model Checking Probabilistic Timed Automata with One or Two Clocks

DOI10.2168/LMCS-4(3:12)2008zbMath1147.68574MaRDI QIDQ3535619

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

Publication date: 13 November 2008

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

zbMATH Keywords

probabilistic timed automatamodel-checking algorithmsprobabilistic timed temporal logic

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (18)

Countdown games, and simulation on (succinct) one-counter nets ⋮ Expected reachability-time games ⋮ Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities ⋮ The Odds of Staying on Budget ⋮ Concavely-Priced Probabilistic Timed Automata ⋮ Strict Divergence for Probabilistic Timed Automata ⋮ Model Checking Linear-Time Properties of Probabilistic Systems ⋮ Unnamed Item ⋮ Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems ⋮ Average-energy games ⋮ Probabilistic timed automata with clock-dependent probabilities ⋮ Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Model checking for probabilistic timed automata ⋮ Reactive synthesis without regret ⋮ Looking at mean-payoff and total-payoff through windows

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