Partial Order Reduction for State/Event LTL

DOI10.1007/978-3-642-00255-7_21MaRDI QIDQ3605476zbMATH OpenOpenAlexFDO

Authors Nikola Beneš, Luboš Brim, J. Sochor, P. Vařeková, Barbora Zimmerova, I. Černá

Publication date 24 February 2009

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

Full work available at URL https://doi.org/10.1007/978-3-642-00255-7_21

Mathematics Subject Classification ID

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

Recommendations

• Partial order reduction for state/event LTL with application to component-interaction automata
• scientific article; zbMATH DE number 1361136
• A pragmatic approach to stateful partial order reduction
• scientific article; zbMATH DE number 2087625
• Partial order reduction for checking LTL formulae with the next-time operator
• scientific article; zbMATH DE number 1059330
• Partial-order reduction techniques for real-time model checking
• Automata-driven partial order reduction and guided search for LTL model checking

Cites work

• scientific article; zbMATH DE number 4110131 (Why is no real title available?)
• scientific article; zbMATH DE number 177511 (Why is no real title available?)
• scientific article; zbMATH DE number 177513 (Why is no real title available?)
• scientific article; zbMATH DE number 2080757 (Why is no real title available?)
• Concurrent software verification with states, events, and deadlocks
• Integrated Formal Methods
• Model Checking Software
• Partial Order Reduction for State/Event LTL
• Stutter-invariant temporal properties are expressible without the next-time operator
• ZB 2005: Formal Specification and Development in Z and B

Cited in

(8)

• Context-dependent minimization of state/event systems
• Partial Order Reduction for State/Event LTL
• Partial order reduction for state/event LTL with application to component-interaction automata
• Optimising the ProB model checker for B using partial order reduction
• Automated recognition of stutter invariance of LTL formulas
• Space effective model checking for component-interaction automata
• Application of partial-order methods to reactive programs with event memorization
• The inconsistent labelling problem of stutter-preserving partial-order reduction

Describes a project that uses

Uses Software

• MAGIC
• DiVinE

This page was built for publication: Partial Order Reduction for State/Event LTL

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