Improved Algorithms for the Automata-Based Approach to Model-Checking

DOI10.1007/978-3-540-71209-1_34MaRDI QIDQ5758127zbMATH OpenOpenAlexFDO

Authors Laurent Doyen, Jean-François Raskin

Publication date 3 September 2007

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71209-1_34

Mathematics Subject Classification ID

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

Recommendations

• Antichains for the Automata-Based Approach to Model-Checking
• Antichains: A New Algorithm for Checking Universality of Finite Automata
• Efficient Büchi universality checking
• Efficient reduction of nondeterministic automata with application to language inclusion testing
• Advanced automata minimization

Cited in

(19)

• Fixed point guided abstraction refinement for alternating automata
• Coinductive algorithms for Büchi automata
• Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes
• Algorithmic algebraic model checking. III: Approximate methods
• Advanced Ramsey-based Büchi automata inclusion testing
• Efficient Büchi universality checking
• Büchi Complementation and Size-Change Termination
• Antichains for the Automata-Based Approach to Model-Checking
• Fixpoint Guided Abstraction Refinement for Alternating Automata
• Efficient reduction of nondeterministic automata with application to language inclusion testing
• Linear temporal logic symbolic model checking
• Coinductive algorithms for Büchi automata
• Random models for evaluating efficient Büchi universality checking
• Experimental Evaluation of Classical Automata Constructions
• Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking
• Antichains: A New Algorithm for Checking Universality of Finite Automata
• Proving Non-inclusion of Büchi Automata Based on Monte Carlo Sampling
• FORQ-Based Language Inclusion Formal Testing
• Profile trees for Büchi word automata, with application to determinization

Describes a project that uses

Uses Software

• LTL2BA

This page was built for publication: Improved Algorithms for the Automata-Based Approach to Model-Checking

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