Event Clock Automata: From Theory to Practice
From MaRDI portal
Publication:3172852
DOI10.1007/978-3-642-24310-3_15zbMATH Open1348.68102arXiv1107.4138OpenAlexW1891690172MaRDI QIDQ3172852FDOQ3172852
Nathalie Sznajder, G. Geeraerts, Jean-François Raskin
Publication date: 7 October 2011
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1107.4138
Cites Work
- Title not available (Why is that?)
- A theory of timed automata
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- Forward analysis of updatable timed automata
- Event-clock automata: a determinizable class of timed automata
- Event-Clock Visibly Pushdown Automata
- Title not available (Why is that?)
- Title not available (Why is that?)
- Event Clock Automata: From Theory to Practice
- Safraless Procedures for Timed Specifications
- Title not available (Why is that?)
Cited In (9)
- Event-clock automata: a determinizable class of timed automata
- Event Clock Automata: From Theory to Practice
- Simulations for event-clock automata
- On regions and zones for event-clock automata
- 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
- Title not available (Why is that?)
Uses Software
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)
