Truly on-the-fly LTL model checking

DOI10.1007/978-3-540-31980-1_13MaRDI QIDQ5703759zbMATH OpenOpenAlexFDO

Authors Moritz Hammer, Alexander Knapp, Stephan Merz

Publication date 10 November 2005

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

Full work available at URL https://doi.org/10.1007/b107194

Mathematics Subject Classification ID

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

Recommendations

• Fast LTL to Büchi automata translation
• Model Checking Software
• Comparison of algorithms for checking emptiness on Büchi automata
• On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
• Model Checking Software

Cited in

(29)

• Memory-efficient tactics for randomized LTL model checking
• Practical CTL* model checking: Should SPIN be extended?
• On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties
• Automata-driven partial order reduction and guided search for LTL model checking
• LTL to self-loop alternating automata with generic acceptance and back
• Model checking with fairness assumptions using PAT
• More efficient on-the-fly LTL verification with Tarjan's algorithm
• Testing Spin's LTL formula conversion into Büchi automata with randomly generated input
• A new unfolding approach to LTL model checking
• Single-pass testing automata for LTL model checking
• Analyzing LTL model checking techniques for plan synthesis and controller synthesis (work in progress)
• Comparison of algorithms for checking emptiness on Büchi automata
• Self-Loop Aggregation Product — A New Hybrid Approach to On-the-Fly LTL Model Checking
• Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
• Bounded rational search for on-the-fly model checking of LTL properties
• Formal Verification Based on Guided Random Walks
• On-the-fly verification of linear temporal logic
• Yet another look at LTL model checking
• Efficient decision procedures for model checking of linear time logic properties
• Component-wise incremental LTL model checking
• Tools and Algorithms for the Construction and Analysis of Systems
• Automated Technology for Verification and Analysis
• Model Checking Software
• GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic
• A note on on-the-fly verification algorithms
• Model Checking Software
• Flash memory efficient LTL model checking
• Satisfiability checking of multi-variable TPTL with unilateral intervals is PSPACE-complete
• On-the-fly TCTL model checking for time Petri nets

This page was built for publication: Truly on-the-fly LTL model checking

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