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

DOI10.1016/j.scico.2010.02.008zbMath1220.68048OpenAlexW1976381588MaRDI QIDQ549692

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

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

formal verificationmodel checkingpartial order reductioncomponent-based systemscomponent-interaction automatastate/event LTL

Mathematics Subject Classification ID

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

Related Items

The inconsistent labelling problem of stutter-preserving partial-order reduction

Uses Software

• DiVinE
• MAGIC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Stutter-invariant temporal properties are expressible without the next-time operator
• Concurrent software verification with states, events, and deadlocks
• Space Effective Model Checking for Component-Interaction Automata
• ZB 2005: Formal Specification and Development in Z and B
• Model Checking Software
• Integrated Formal Methods