Checking timed Büchi automata emptiness on simulation graphs

DOI10.1145/1507244.1507245zbMath1352.68165OpenAlexW2162181585MaRDI QIDQ2946573

Stavros Tripakis

Publication date: 17 September 2015

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1507244.1507245

zbMATH Keywords

timed Büchi automataspecification languagesmodel checkingformal methodsproperty-preserving abstractions

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (11)

Fast zone-based algorithms for reachability in pushdown timed automata ⋮ Model Checking Real-Time Systems ⋮ On clock-aware LTL parameter synthesis of timed automata ⋮ Unnamed Item ⋮ A survey of timed automata for the development of real-time systems ⋮ Efficient emptiness check for timed Büchi automata ⋮ On the timed temporal logic planning of coupled multi-agent systems ⋮ Certifying emptiness of timed Büchi automata ⋮ A menagerie of timed automata ⋮ Coarse Abstractions Make Zeno Behaviours Difficult to Detect ⋮ Checking Timed Büchi Automata Emptiness Using LU-Abstractions

Uses Software

• Kronos
• Uppaal

This page was built for publication: Checking timed Büchi automata emptiness on simulation graphs