Generalized abstraction-refinement for game-based CTL lifted model checking

DOI10.1016/j.tcs.2020.06.011zbMath1460.68058OpenAlexW3036435269MaRDI QIDQ2193289

Aleksandar S. Dimovski, Axel Legay, Andrzej Wąsowski

Publication date: 25 August 2020

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2020.06.011

zbMATH Keywords

automatic abstraction refinementgame-based model checkinglifted model checkingvariability abstractions

Mathematics Subject Classification ID

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

Related Items (1)

Family-Based SPL Model Checking Using Parity Games with Variability

Uses Software

• SPIN

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Results on the propositional \(\mu\)-calculus
• Compositional verification and 3-valued abstractions join forces
• Abstract family-based model checking using modal featured transition systems: preservation of \(\mathrm{CTL}^{\star}\)
• Finding suitable variability abstractions for lifted analysis
• Variability-Specific Abstraction Refinement for Family-Based Model Checking
• From Transition Systems to Variability Models and from Lifted Model Checking Back to UPPAAL
• A game-based framework for CTL counterexamples and 3-valued abstraction-refinement
• Tools and Algorithms for the Construction and Analysis of Systems
• Software Product Line Engineering
• Verification, Model Checking, and Abstract Interpretation
• Modal I/O Automata for Interface and Product Line Theories
• Decidability of DPDA equivalence
• Feature integration using a feature construct

This page was built for publication: Generalized abstraction-refinement for game-based CTL lifted model checking