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

DOI10.1016/J.SCICO.2010.02.008zbMATH Open1220.68048OpenAlexW1976381588MaRDI QIDQ549692FDOQ549692

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Stutter-invariant temporal properties are expressible without the next-time operator
• Title not available (Why is that?)
• Concurrent software verification with states, events, and deadlocks
• Integrated Formal Methods
• Space effective model checking for component-interaction automata
• Title not available (Why is that?)
• ZB 2005: Formal Specification and Development in Z and B
• Model Checking Software

Cited In (2)

• Partial Order Reduction for State/Event LTL
• The inconsistent labelling problem of stutter-preserving partial-order reduction

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)