MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs

DOI10.1007/978-3-540-68746-7_20zbMath1143.68455OpenAlexW1607121733MaRDI QIDQ3510873

Denis Poitrenaud, Kais Klai

Publication date: 3 July 2008

Published in: Applications and Theory of Petri Nets (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-68746-7_20

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)

Related Items (3)

LTL under reductions with weaker conditions than stutter invariance ⋮ A novel approach for supervisor synthesis to enforce opacity of discrete event systems ⋮ Component-wise incremental LTL model checking

Uses Software

• NuSMV

Cites Work

• NuSMV: A new symbolic model checker
• Automated Technology for Verification and Analysis
• A space-efficient on-the-fly algorithm for real-time model checking
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs