In "Calculational Desing of a Regular Model Checker by Abstract Interpretation" (see) Cousot first defines a definition of model checking in his new settings at the page 9 then at the page 11 he says that the previous definition is impractical for structural model checking.

So what is structural model checking?


1 Answer 1


I hadn't seen that term before either. In essence it seems to mean a model checking algorithm taking a program $P$ (with its syntactic structure) and a property that exploits $P$'s structure in the actual model checking as opposed to more traditional algorithms that turn $P$ into a labelled transition system and then go to town on that. Definition 3 in the paper gives the technical details in three installments, by induction on the program structure.

  • $\begingroup$ Thank you very much. What do you mean by "Definition 3"? There is no "Definition 3" in the paper. $\endgroup$
    – Senmorta
    Commented Jan 16, 2023 at 0:35
  • $\begingroup$ Weird. I see that Definition 3 in the PDF you linked in your post beginning at the bottom of page 12 and going all the way to the end of page 16. $\endgroup$
    – Kai
    Commented Jan 16, 2023 at 10:15
  • $\begingroup$ You are right! I'm sorry! I checked another version of the paper with different numbering for definitions! So, why do you think he used the word "structural" for it? Is there any precise mathematical concept behind it or should I just conceive it as a regular word in natural language? Do you think that the second way is mathematically acceptable? Thank you very much. $\endgroup$
    – Senmorta
    Commented Jan 16, 2023 at 15:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.