Model Checking Probabilistic Timed Automata with One or Two Clocks

DOI10.2168/LMCS-4(3:12)2008MaRDI QIDQ3535619zbMATH OpenFDO

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

Publication date 13 November 2008

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

Full work available at URL https://doi.org/10.2168/LMCS-4(3:12)2008

zbMATH Keywords

model-checking algorithmsprobabilistic timed automataprobabilistic 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)

Recommendations

• Model Checking Probabilistic Timed Automata with One or Two Clocks
• CONCUR 2004 - Concurrency Theory
• Model checking for probabilistic timed automata
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Symbolic model checking for probabilistic timed automata

Cited in

(29)

• Polytime model checking for times probabilistic computation tree logic
• On probabilistic timed automata.
• Model checking for probabilistic timed automata
• Looking at mean-payoff and total-payoff through windows
• Symbolic model checking for probabilistic timed automata
• Average-energy games
• Expected reachability-time games
• Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata
• Concavely-Priced Probabilistic Timed Automata
• Strict Divergence for Probabilistic Timed Automata
• The odds of staying on budget
• Synthesis of memory-efficient, clock-memory free, and non-Zeno safety controllers for timed systems
• Average-energy games
• Probabilistic timed automata with one clock and initialised clock-dependent probabilities
• Probabilistic timed automata with one clock and initialised clock-dependent probabilities
• Model checking linear-time properties of probabilistic systems
• Reactive synthesis without regret
• Parity games with weights
• CONCUR 2004 - Concurrency Theory
• Probabilistic and Topological Semantics for Timed Automata
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Model Checking Probabilistic Timed Automata with One or Two Clocks
• Reachability for bounded branching VASS
• Countdown games, and simulation on (succinct) one-counter nets
• Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
• History-deterministic timed automata
• Geography, Kotzig's Nim, and variants
• As soon as possible but rationally
• Limit your consumption! Finding bounds in average-energy games

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3535619)