Model Checking Probabilistic Timed Automata with One or Two Clocks
From MaRDI portal
Publication:3535619
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)
68Q25: Analysis of algorithms and problem complexity
68Q45: Formal languages and automata
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Unnamed Item, Unnamed Item, Probabilistic Timed Automata with One Clock and Initialised Clock-Dependent Probabilities, Model Checking Linear-Time Properties of Probabilistic Systems, Unnamed Item, Unnamed Item, Countdown games, and simulation on (succinct) one-counter nets, Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties, Expected reachability-time games, Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems, Reactive synthesis without regret, Probabilistic timed automata with clock-dependent probabilities, Model checking for probabilistic timed automata, Looking at mean-payoff and total-payoff through windows, Average-energy games, Concavely-Priced Probabilistic Timed Automata, Strict Divergence for Probabilistic Timed Automata, The Odds of Staying on Budget