On regions and zones for event-clock automata

DOI10.1007/s10703-014-0212-1zbMath1314.68176OpenAlexW2070002955MaRDI QIDQ487253

Jean-François Raskin, Nathalie Sznajder, Gilles Geeraerts

Publication date: 19 January 2015

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://dipot.ulb.ac.be/dspace/bitstream/2013/160783/3/regzonesECA.pdf

zbMATH Keywords

verificationregionstimed automataformal methodsreal-timeDBMsevent-clock automatazones

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Related Items

On the determinization of event-clock input-driven pushdown automata

Uses Software

• Kronos
• Tempo

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model-checking in dense real-time
• The octagon abstract domain
• Event-clock automata: a determinizable class of timed automata
• A theory of timed automata
• Automated verification of an audio-control protocol using UPPAAL
• Forward analysis of updatable timed automata
• Formal modeling and analysis of timed systems. Third international conference, FORMATS 2005, Uppsala, Sweden, September 26--28, 2005. Proceedings
• Event Clock Automata: From Theory to Practice
• Safraless Procedures for Timed Specifications
• Event-Clock Visibly Pushdown Automata
• Removing ε-transitions in timed automata
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Formal Modeling and Analysis of Timed Systems