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

DOI10.1007/978-3-642-33365-1_16zbMATH Open1374.68298OpenAlexW85611312MaRDI QIDQ4649399FDOQ4649399

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

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

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)

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

Uses Software

• Kronos
• Uppaal
• ZenoTool

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)