Computation tree logic and NuSMV model checker

zbMATH Open1240.68134MaRDI QIDQ3170516FDOQ3170516

Authors: Cristina Tudose 

Publication date: 27 September 2011

Recommendations

• scientific article; zbMATH DE number 910719
• Branching-time temporal logic and tree automata
• scientific article; zbMATH DE number 2196601
• scientific article; zbMATH DE number 1746645
• Model checking.

zbMATH Keywords

model checkingcomputation tree logicKripke structure

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cited In (9)

• Title not available (Why is that?)
• Symbolic Fault Tree Analysis for Reactive Systems
• Model Checking Quantified Computation Tree Logic
• Title not available (Why is that?)
• Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs (MDGs)
• Computation tree measurement language (CTML)
• CTL may be ambiguous when model checking Moore machines
• A model checker for linear time temporal logic
• NuSMV: A new symbolic model checker

Uses Software

• NuSMV

This page was built for publication: Computation tree logic and NuSMV model checker

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