Efficient emptiness check for timed Büchi automata

DOI10.1007/S10703-011-0133-1zbMATH Open1247.68143arXiv1104.1540OpenAlexW1863919967MaRDI QIDQ453519FDOQ453519

Authors: 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)

Abstract: The B"uchi non-emptiness problem for timed automata refers to deciding if a given automaton has an infinite non-Zeno run satisfying the B"uchi accepting condition. The standard solution to this problem involves adding an auxiliary clock to take care of the non-Zenoness. In this paper, it is shown that this simple transformation may sometimes result in an exponential blowup. A construction avoiding this blowup is proposed. It is also shown that in many cases, non-Zenoness can be ascertained without extra construction. An on-the-fly algorithm for the non-emptiness problem, using non-Zenoness construction only when required, is proposed. Experiments carried out with a prototype implementation of the algorithm are reported.

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

Recommendations

• Efficient on-the-fly emptiness check for timed Büchi automata
• Checking timed Büchi automata emptiness efficiently
• Checking timed Büchi automata emptiness on simulation graphs
• Checking timed Büchi automata emptiness using LU-abstractions
• Model Checking Software

zbMATH Keywords

timed automatanon-Zenonesson-the-fly algorithmBüchi accepting conditions

Mathematics Subject Classification ID

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

Cites Work

• A theory of timed automata
• Formal Methods for the Design of Real-Time Systems
• Checking timed Büchi automata emptiness efficiently
• Forward analysis of updatable timed automata
• Efficient on-the-fly emptiness check for timed Büchi 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
• Model Checking Software
• Tools and Algorithms for the Construction and Analysis of Systems
• How to stop time stopping

Cited In (8)

• Efficient convex zone merging in parametric timed automata
• Checking timed Büchi automata emptiness on simulation graphs
• Efficient on-the-fly emptiness check for timed Büchi automata
• Distributed parametric model checking timed automata under non-zenoness assumption
• On clock-aware LTL parameter synthesis of timed automata
• Checking timed Büchi automata emptiness efficiently
• Checking timed Büchi automata emptiness using LU-abstractions
• A local-time semantics for negotiations

Uses Software

• Kronos
• Uppaal

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q453519)