Robust model-checking of timed automata via pumping in channel machines

DOI10.1007/978-3-642-24310-3_8MaRDI QIDQ3172846zbMATH OpenOpenAlexFDO

Authors Patricia Bouyer, Nicolas Markey, Ocan Sankur

Publication date 7 October 2011

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-24310-3_8

Mathematics Subject Classification ID

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

Recommendations

• Robust model checking of timed automata under clock drifts
• Robust Analysis of Timed Automata Via Channel Machines
• Robust safety of timed automata
• Robust Model-Checking of Linear-Time Properties in Timed Automata
• Untimed Language Preservation in Timed Systems

Cites work

• scientific article; zbMATH DE number 2085321 (Why is no real title available?)
• scientific article; zbMATH DE number 5228180 (Why is no real title available?)
• A theory of timed automata
• Almost ASAP semantics: from timed models to timed implementations
• Dynamical properties of timed automata
• Kronos: A verification tool for real-time systems
• Quantitative robustness analysis of flat timed automata
• Robust Analysis of Timed Automata Via Channel Machines
• Robust Model-Checking of Linear-Time Properties in Timed Automata
• Robust safety of timed automata
• Shrinking timed automata
• Uppaal in a nutshell

Cited in

(11)

• Relating syntactic and semantic perturbations of hybrid automata
• Robust safety of timed automata
• Robust model checking of timed automata under clock drifts
• Model measuring for discrete and hybrid systems
• Shrinking timed automata
• Combining free choice and time in Petri nets
• Robust reachability in timed automata and games: a game-based approach
• Symbolic Robustness Analysis of Timed Automata
• Robust Analysis of Timed Automata Via Channel Machines
• Symbolic quantitative robustness analysis of timed automata
• Robust synthesis for real-time systems

Describes a project that uses

Uses Software

• Uppaal
• Kronos

This page was built for publication: Robust model-checking of timed automata via pumping in channel machines

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