Compositionality and locality for improving model checking in the selective mu-calculus

DOI10.1016/J.SCICO.2004.07.002MaRDI QIDQ703588zbMATH OpenOpenAlexFDO

Authors Antonella Santone, Gigliola Vaglini

Publication date 11 January 2005

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

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

zbMATH Keywords

CompositionalityModel checkingSoftware engineeringTableau systemTemporal logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Tableau-based model checking in the propositional mu-calculus
• Local model checking for infinite state spaces
• Compositional and quantitative model checking (extended abstract)
• Local model checking in the modal mu-calculus
• scientific article; zbMATH DE number 4180789

Cited in

(10)

• Tableau-based model checking in the propositional mu-calculus
• Local model checking for infinite state spaces
• Selective mu-calculus and formula-based equivalence of transition systems
• Compositional verification of concurrent systems by combining bisimulations
• Compositional verification and 3-valued abstractions join forces
• scientific article; zbMATH DE number 1670785 (Why is no real title available?)
• Compositional and quantitative model checking (extended abstract)
• scientific article; zbMATH DE number 2080055 (Why is no real title available?)
• Compositional verification of concurrent systems by combining bisimulations
• Abstract reduction in directed model checking CCS processes

This page was built for publication: Compositionality and locality for improving model checking in the selective mu-calculus

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