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

model checkingformal verificationpartial order reductioncomponent-based systemscomponent-interaction automatastate/event LTL

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) 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
• Publication:4507826
• Transparent partial order reduction

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 910719 (Why is no real title available?)
• Concurrent software verification with states, events, and deadlocks
• 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)

• Partial Order Reduction for State/Event LTL
• Partial order reduction for checking LTL formulae with the next-time operator
• Automated recognition of stutter invariance of LTL formulas
• Space effective model checking for component-interaction automata
• 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 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)