Automated recognition of stutter invariance of LTL formulas

MaRDI QIDQ5170011zbMATH OpenFDO

Authors Jeffrey Dallien, Wendy MacCaull

Publication date 17 July 2014

Mathematics Subject Classification ID

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

Recommendations

• Stutter-invariant languages, -automata, and temporal logic
• On closure under stuttering
• LTL under reductions with weaker conditions than stutter invariance
• Partial Order Reduction for State/Event LTL
• Partial order reduction for state/event LTL with application to component-interaction automata

Cited in

(10)

• On closure under stuttering
• STLInspector: STL validation with guarantees
• LTL under reductions with weaker conditions than stutter invariance
• Action-based model checking: logic, automata, and reduction
• Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications
• The stuttering principle revisited: On the expressiveness of nested X and U operators in the logic LTL
• Stutter-invariant languages, -automata, and temporal logic
• Model Checking Software
• Partial order reduction for state/event LTL with application to component-interaction automata
• Characterization and verification of stuttering equivalence

This page was built for publication: Automated recognition of stutter invariance of LTL formulas

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