On regions and zones for event-clock automata

DOI10.1007/S10703-014-0212-1MaRDI QIDQ487253zbMATH OpenOpenAlexFDO

Authors G. Geeraerts, Jean-François Raskin, Nathalie Sznajder

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

verificationregionsreal-timeformal methodstimed automataDBMsevent-clock automatazones

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Recommendations

• Discretization of timed automata in timed \(\mu\)CRL à la regions and zones
• A Logical Characterisation of Event Clock Automata
• Zone-Based Universality Analysis for Single-Clock Timed Automata
• Event-clock automata: a determinizable class of timed automata
• Event clock automata: from theory to practice
• scientific article; zbMATH DE number 1390065
• Tools and Algorithms for the Construction and Analysis of Systems
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Adding Invariants to Event Zone Automata

Cites work

• scientific article; zbMATH DE number 3126094 (Why is no real title available?)
• scientific article; zbMATH DE number 2102690 (Why is no real title available?)
• scientific article; zbMATH DE number 1390065 (Why is no real title available?)
• scientific article; zbMATH DE number 1400049 (Why is no real title available?)
• A theory of timed automata
• Automated verification of an audio-control protocol using UPPAAL
• Event clock automata: from theory to practice
• Event-Clock Visibly Pushdown Automata
• Event-clock automata: a determinizable class of timed automata
• Formal Modeling and Analysis of Timed Systems
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Formal modeling and analysis of timed systems. Third international conference, FORMATS 2005, Uppsala, Sweden, September 26--28, 2005. Proceedings
• Forward analysis of updatable timed automata
• Model-checking in dense real-time
• Removing \(\epsilon \)-transitions in timed automata
• Safraless Procedures for Timed Specifications
• The octagon abstract domain

Cited in

(6)

• Adding Invariants to Event Zone Automata
• Event-clock nested automata
• Simulations for event-clock automata
• On the determinization of event-clock input-driven pushdown automata
• A unified model for real-time systems: symbolic techniques and implementation
• Event clock automata: from theory to practice

Describes a project that uses

Uses Software

• Tempo
• Kronos

This page was built for publication: On regions and zones for event-clock automata

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