Search

• < Previous
• 1
• Next >

---

Coarse abstractions make Zeno behaviours difficult to detect

Frédéric Herbreteau ; B Srivathsan.

An infinite run of a timed automaton is Zeno if it spans only a finite amount of time. Such runs are considered unfeasible and hence it is important to detect them, or dually, find runs that are non-Zeno. Over the years important improvements have been obtained in checking reachability properties&nbsp;[&hellip;]

---

Simulations for Event-Clock Automata

S Akshay ; Paul Gastin ; R Govind ; B Srivathsan.

Event-clock automata (ECA) are a well-known semantic subclass of timed automata (TA) which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for checking&nbsp;[&hellip;]

---