Model Checking One-clock Priced Timed Automata

DOI10.2168/LMCS-4(2:9)2008MaRDI QIDQ3518285zbMATH OpenFDO

Authors Patricia Bouyer, Nicolas Markey, Kim G. Larsen

Publication date 7 August 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(2:9)2008

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Model-Checking One-Clock Priced Timed Automata
• Model checking logic WCTL with multi constrained modalities on one clock priced timed automata
• Costs Are Expensive!
• Model checking weighted integer reset timed automata
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems

Cited in

(22)

• Learning deterministic probabilistic automata from a model checking perspective
• Costs and rewards in priced timed automata
• Parameterized model checking of weighted networks
• On model-checking timed automata with stopwatch observers
• Timed automata with observers under energy constraints
• Model Checking Real-Time Systems
• Costs Are Expensive!
• Event-Clock Visibly Pushdown Automata
• One-Clock Deterministic Timed Automata Are Efficiently Identifiable in the Limit
• Model checking logic WCTL with multi constrained modalities on one clock priced timed automata
• Model Checking Metric Temporal Logic over Automata with One Counter
• Costs and rewards in priced timed automata
• Probabilistic timed automata with one clock and initialised clock-dependent probabilities
• Probabilistic timed automata with one clock and initialised clock-dependent probabilities
• On parametric timed automata and one-counter machines
• CONCUR 2004 - Concurrency Theory
• Model checking weighted integer reset timed automata
• MSO logics for weighted timed automata
• Model-Checking One-Clock Priced Timed Automata
• Alternation-free weighted mu-calculus: decidability and completeness
• Design and verification of pipelined circuits with timed Petri nets
• Reachability for multi-priced timed automata with positive and negative rates

This page was built for publication: Model Checking One-clock Priced Timed Automata

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