Reduced models for efficient CCS verification

DOI10.1007/s10703-005-1634-6zbMath1085.68085OpenAlexW2034611435MaRDI QIDQ816205

Roberto Barbuti, Gigliola Vaglini, Antonella Santone, Nicoletta De Francesco

Publication date: 20 February 2006

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-005-1634-6

zbMATH Keywords

model checkingtransition systemCCSstate explosion problem

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)

Uses Software

• LOTOS
• CADP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formula-dependent equivalence for compositional CTL model checking
• Results on the propositional \(\mu\)-calculus
• Tableau-based model checking in the propositional mu-calculus
• Local model checking in the modal mu-calculus
• Minimal state graph generation
• On reduction of asynchronous systems
• Property preserving abstractions for the verification of concurrent systems
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Selective mu-calculus and formula-based equivalence of transition systems
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Abstract interpretation and application to logic programs
• On model checking for the \(\mu\)-calculus and its fragments