Efficient emptiness check for timed Büchi automata

DOI10.1007/s10703-011-0133-1zbMath1247.68143arXiv1104.1540OpenAlexW1863919967MaRDI QIDQ453519

Frédéric Herbreteau, B. Srivathsan, Igor Walukiewicz

Publication date: 27 September 2012

Published in: Formal Methods in System Design (Search for Journal in Brave)

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

zbMATH Keywords

timed automataBüchi accepting conditionsnon-Zenonesson-the-fly algorithm

Mathematics Subject Classification ID

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

Related Items (3)

On clock-aware LTL parameter synthesis of timed automata ⋮ Distributed parametric model checking timed automata under non-zenoness assumption ⋮ Efficient convex zone merging in parametric timed automata

Uses Software

• Kronos
• Uppaal

Cites Work

• Checking timed Büchi automata emptiness efficiently
• How to stop time stopping
• A theory of timed automata
• Forward analysis of updatable timed automata
• Checking timed Büchi automata emptiness on simulation graphs
• Coarse Abstractions Make Zeno Behaviours Difficult to Detect
• Efficient Detection of Zeno Runs in Timed Automata
• Checking Timed Büchi Automata Emptiness Using LU-Abstractions
• Efficient On-the-Fly Emptiness Check for Timed Büchi Automata
• Model Checking Software
• Formal Methods for the Design of Real-Time Systems
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Efficient emptiness check for timed Büchi automata