Static detection of Zeno runs in UPPAAL networks based on synchronization matrices and two data-variable heuristics

DOI10.1007/978-3-642-33365-1_16MaRDI QIDQ4649399zbMATH OpenOpenAlexFDO

Authors Jonas Rinast, S. Schupp

Publication date 21 November 2012

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-33365-1_16

zbMATH Keywords

timed automataUPPAALZeno runs

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Efficient Detection of Zeno Runs in Timed Automata
• Coarse abstractions make Zeno behaviours difficult to detect
• Coarse abstractions make Zeno behaviours difficult to detect
• A tool for the syntactic detection of Zeno-timelocks in timed automata
• How to stop time stopping

Cited in

(5)

• Efficient Detection of Zeno Runs in Timed Automata
• Coarse abstractions make Zeno behaviours difficult to detect
• Coarse abstractions make Zeno behaviours difficult to detect
• A tool for the syntactic detection of Zeno-timelocks in timed automata
• Finding minimum and maximum termination time of timed automata models with cyclic behaviour

Describes a project that uses

Uses Software

• ZenoTool
• Uppaal
• Kronos

This page was built for publication: Static detection of Zeno runs in UPPAAL networks based on synchronization matrices and two data-variable heuristics

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