Efficient emptiness check for timed Büchi automata

DOI10.1007/S10703-011-0133-1MaRDI QIDQ453519zbMATH OpenOpenAlexFDO

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)

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

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)

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.

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

Cites work

• A theory of timed 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
• Coarse abstractions make Zeno behaviours difficult to detect
• Efficient Detection of Zeno Runs in Timed Automata
• Efficient on-the-fly emptiness check for timed Büchi automata
• Formal Methods for the Design of Real-Time Systems
• Forward analysis of updatable timed automata
• How to stop time stopping
• Model Checking Software
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(8)

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

Describes a project that uses

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)