Data structures for symbolic multi-valued model-checking

DOI10.1007/s10703-006-0016-zzbMath1109.68063OpenAlexW2059949763MaRDI QIDQ862857

Benet Devereux, Steve Easterbrook, Marsha Chechik, Albert Lai, Arie Gurfinkel

Publication date: 24 January 2007

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

Full work available at URL: https://doi.org/10.1007/s10703-006-0016-z

zbMATH Keywords

Decision diagramsSymbolic model-checkingMulti-valued logic

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) Many-valued logic (03B50)

Related Items (20)

Integrating Topological Proofs with Model Checking to Instrument Iterative Design ⋮ Statistical Model Checking for Variability-Intensive Systems ⋮ Abstraction and Abstraction Refinement ⋮ Data structures for symbolic multi-valued model-checking ⋮ Fuzzy Halpern and Shoham's interval temporal logics ⋮ Model checking computation tree logic over finite lattices ⋮ Multi-valued model checking games ⋮ Quantitative model checking of linear-time properties based on generalized possibility measures ⋮ Symbolic checking of fuzzy CTL on fuzzy program graph ⋮ Computation tree logic model checking based on multi-valued possibility measures ⋮ A Direct Algorithm for Multi-valued Bounded Model Checking ⋮ Model checking fuzzy computation tree logic ⋮ Multi-robot LTL planning under uncertainty ⋮ Model checking of linear-time properties in multi-valued systems ⋮ TOrPEDO : witnessing model correctness with topological proofs ⋮ Statistical model checking for variability-intensive systems: applications to bug detection and minimization ⋮ A verification-driven framework for iterative design of controllers ⋮ Quantitative \(\mu\)-calculus and CTL defined over constraint semirings ⋮ Simulation for lattice-valued doubly labeled transition systems ⋮ Abstraction and approximation in fuzzy temporal logics and models

Uses Software

• SCTL-MUS
• SLAM
• NuSMV

Cites Work

• Data structures for symbolic multi-valued model-checking
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Graph-Based Algorithms for Boolean Function Manipulation
• Binary Decision Diagrams
• Model checking lattices: using and reasoning about information orders for abstraction
• Branching Programs and Binary Decision Diagrams
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation
• CONCUR 2003 - Concurrency Theory
• Computer Aided Verification
• Efficient detection of vacuity in temporal model checking
• SCTL-MUS: A formal methodology for software development of distributed systems. A case study
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Data structures for symbolic multi-valued model-checking