Yet another look at LTL model checking

DOI10.1007/3-540-48153-2_25MaRDI QIDQ4494397zbMATH OpenFDO

Authors Klaus Schneider

Publication date 10 August 2000

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

Full work available at URL https://doi.org/10.1007/3-540-48153-2_25

zbMATH Keywords

LTLmodel checking

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1973991
• Improving automata generation for linear temporal logic by considering the automaton hierarchy
• Efficient Büchi automata form LTL formulae
• Fast LTL to Büchi automata translation
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(11)

• LTL semantic tableaux and alternating -automata via linear factors
• A new unfolding approach to LTL model checking
• Analyzing LTL model checking techniques for plan synthesis and controller synthesis (work in progress)
• Improving automata generation for linear temporal logic by considering the automaton hierarchy
• Self-Loop Aggregation Product — A New Hybrid Approach to On-the-Fly LTL Model Checking
• Semi-external LTL Model Checking
• Model Checking LTL Formulae in RAISE with FDR
• scientific article; zbMATH DE number 1982198 (Why is no real title available?)
• Randomization helps in LTL model checking
• LTL-model-checking via model composition
• Synchronous or alternating? LTL black-box checking of Mealy machines by combining the LearnLib and LTSmin

This page was built for publication: Yet another look at LTL model checking

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