Partial order reduction for state/event LTL with application to component-interaction automata

DOI10.1016/J.SCICO.2010.02.008MaRDI QIDQ549692zbMATH OpenOpenAlexFDO

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

Publication date 18 July 2011

Published in Science of Computer Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.scico.2010.02.008

zbMATH Keywords

component-based systemscomponent-interaction automataformal verificationmodel checkingpartial order reductionstate/event LTL

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Partial Order Reduction for State/Event LTL
• Space effective model checking for component-interaction automata
• Automated recognition of stutter invariance of LTL formulas
• scientific article; zbMATH DE number 1515293
• Transparent partial order reduction

Cites work

• Concurrent software verification with states, events, and deadlocks
• 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 910719 (Why is no real title available?)
• Integrated Formal Methods
• Model Checking Software
• Space effective model checking for component-interaction automata
• Stutter-invariant temporal properties are expressible without the next-time operator
• ZB 2005: Formal Specification and Development in Z and B

Cited in

(5)

• The inconsistent labelling problem of stutter-preserving partial-order reduction
• Space effective model checking for component-interaction automata
• Partial order reduction for checking LTL formulae with the next-time operator
• Partial Order Reduction for State/Event LTL
• Automated recognition of stutter invariance of LTL formulas

Describes a project that uses

Uses Software

• DiVinE
• MAGIC

This page was built for publication: Partial order reduction for state/event LTL with application to component-interaction automata

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