Optimizing Büchi automata

DOI10.1007/3-540-44618-4_13MaRDI QIDQ4536600zbMATH OpenFDO

Authors Kousha Etessami, Gerard J. Holzmann

Publication date 28 November 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44618-4_13

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1973991
• Efficient Büchi automata form LTL formulae
• scientific article; zbMATH DE number 1796123
• Concepts of Automata Construction from LTL
• Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata

Cited in

(40)

• Tool support for learning Büchi automata and linear temporal logic
• Applicability of fair simulation
• From LTL to unambiguous Büchi automata via disambiguation of alternating automata
• Effective reductions of Mealy machines
• LTL under reductions with weaker conditions than stutter invariance
• LTL to self-loop alternating automata with generic acceptance and back
• Transformation from PLTL to automata via NFGs
• From LTL to deterministic automata. A safraless compositional approach
• More efficient on-the-fly LTL verification with Tarjan's algorithm
• Index appearance record with preorders
• Testing Spin's LTL formula conversion into Büchi automata with randomly generated input
• Linking ST_eP with SPIN
• Efficient Büchi automata form LTL formulae
• On the relationship between LTL normal forms and Büchi automata
• The Maude LTL model checker
• Büchi automata optimisations formalised in Isabelle/HOL
• Büchi Store: an open repository of Büchi automata
• Explicit-state model checking
• New optimizations and heuristics for determinization of Büchi automata
• Approximate automata for omega-regular languages
• LTL to deterministic Emerson-Lei automata
• On-the-Fly Stuttering in the Construction of Deterministic ω-Automata
• Efficient State Space Reduction for Automata by Fair Simulation
• Mechanizing the Powerset Construction for Restricted Classes of ω-Automata
• Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata
• scientific article; zbMATH DE number 1973991 (Why is no real title available?)
• scientific article; zbMATH DE number 1982194 (Why is no real title available?)
• scientific article; zbMATH DE number 1796122 (Why is no real title available?)
• scientific article; zbMATH DE number 1903381 (Why is no real title available?)
• scientific article; zbMATH DE number 1418459 (Why is no real title available?)
• Automata-Theoretic Model Checking Revisited
• Markov chains and unambiguous automata
• Bridging the gap between single- and multi-model predictive runtime verification
• Simulation relations and applications in formal methods
• Dissecting \texttt{ltlsynt}
• From Spot 2.0 to Spot 2.10: What’s New?
• Tighter construction of tight Büchi automata
• Organising LTL monitors over distributed systems with a global clock
• Structural reductions and stutter sensitive properties
• Experiments with deterministic -automata for formulas of linear temporal logic

This page was built for publication: Optimizing Büchi automata

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