Checking timed Büchi automata emptiness efficiently

DOI10.1007/s10703-005-1632-8zbMath1085.68083OpenAlexW2133057837MaRDI QIDQ816203

Sergio Yovine, Ahmed Bouajjani, Stavros Tripakis

Publication date: 20 February 2006

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

Full work available at URL: https://doi.org/10.1007/s10703-005-1632-8

zbMATH Keywords

timed automataverification toolson-the-fly verificationsymbolic model-checking

Mathematics Subject Classification ID

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

Related Items (20)

Expected reachability-time games ⋮ Model Checking Real-Time Systems ⋮ Strict Divergence for Probabilistic Timed Automata ⋮ On clock-aware LTL parameter synthesis of timed automata ⋮ Schedulability of asynchronous real-time concurrent objects ⋮ LTL Parameter Synthesis of Parametric Timed Automata ⋮ Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata ⋮ A survey of timed automata for the development of real-time systems ⋮ Probabilistic timed automata with clock-dependent probabilities ⋮ Distributed parametric model checking timed automata under non-zenoness assumption ⋮ Verification and control of partially observable probabilistic systems ⋮ Efficient emptiness check for timed Büchi automata ⋮ Finding minimum and maximum termination time of timed automata models with cyclic behaviour ⋮ Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata ⋮ Model checking for probabilistic timed automata ⋮ Certifying emptiness of timed Büchi automata ⋮ Iterative bounded synthesis for efficient cycle detection in parametric timed automata ⋮ Coarse Abstractions Make Zeno Behaviours Difficult to Detect ⋮ Stochastic Games for Verification of Probabilistic Timed Automata ⋮ Checking Timed Büchi Automata Emptiness Using LU-Abstractions

Uses Software

• Kronos
• TAXYS
• Uppaal
• Petrify

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Minimum and maximum delay problems in real-time systems
• Model-checking in dense real-time
• The temporal semantics of concurrent programs
• A theory of timed automata
• Symbolic model checking for real-time systems
• Kronos: A verification tool for real-time systems
• Uppaal in a nutshell
• On the learnability of infinitary regular sets
• Three Partition Refinement Algorithms
• Depth-First Search and Linear Graph Algorithms
• Analysis of timed systems using time-abstracting bisimulations

This page was built for publication: Checking timed Büchi automata emptiness efficiently