Event clock automata: from theory to practice

DOI10.1007/978-3-642-24310-3_15MaRDI QIDQ3172852zbMATH OpenOpenAlexFDO

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

Publication date 7 October 2011

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

Full work available at URL https://arxiv.org/abs/1107.4138

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Abstract: Event clock automata (ECA) are a model for timed languages that has been introduced by Alur, Fix and Henzinger as an alternative to timed automata, with better theoretical properties (for instance, ECA are determinizable while timed automata are not). In this paper, we revisit and extend the theory of ECA. We first prove that no finite time abstract language equivalence exists for ECA, thereby disproving a claim in the original work on ECA. This means in particular that regions do not form a time abstract bisimulation. Nevertheless, we show that regions can still be used to build a finite automaton recognizing the untimed language of an ECA. Then, we extend the classical notions of zones and DBMs to let them handle event clocks instead of plain clocks (as in timed automata) by introducing event zones and Event DBMs (EDBMs). We discuss algorithms to handle event zones represented as EDBMs, as well as (semi-) algorithms based on EDBMs to decide language emptiness of ECA.

Recommendations

• On regions and zones for event-clock automata
• Event-clock automata: a determinizable class of timed automata
• Event-clock nested automata
• A Logical Characterisation of Event Clock Automata
• Event clock message passing automata: a logical characterization and an emptiness checking algorithm

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
• Event clock automata: from theory to practice
• Event-Clock Visibly Pushdown Automata
• Event-clock automata: a determinizable class of timed automata
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Forward analysis of updatable timed automata
• Safraless Procedures for Timed Specifications

Cited in

(12)

• Adding Invariants to Event Zone Automata
• Event-clock automata: a determinizable class of timed automata
• Event-clock nested automata
• Simulations for event-clock automata
• On regions and zones for event-clock automata
• Memory event clocks
• Event-Clock Visibly Pushdown Automata
• Complexity issues for timeline-based planning over dense time under future and minimal semantics
• Equivalence checking and intersection of deterministic timed finite state machines
• A unified model for real-time systems: symbolic techniques and implementation
• Event clock automata: from theory to practice
• scientific article; zbMATH DE number 1390065 (Why is no real title available?)

Describes a project that uses

Uses Software

• Tempo
• Kronos

This page was built for publication: Event clock automata: from theory to practice

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