<p>I hadn't seen that term before either. In essence it seems to mean a model checking <em>algorithm</em> taking a program <span class="math-container">$P$</span> (with its syntactic structure) and a property that exploits <span class="math-container">$P$</span>'s structure in the actual model checking as opposed to more traditional algorithms that turn <span class="math-container">$P$</span> 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.</p>

CC BY-SA 4.0
2023-01-16T00:35:33.650Z
Thank you very much. What do you mean by "Definition 3"? There is no "Definition 3" in the paper.
Senmorta
CC BY-SA 4.0
2023-01-16T10:15:21.493Z
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.
Kai
CC BY-SA 4.0
2023-01-16T15:15:01.970Z
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.
Senmorta
CC BY-SA 4.0
2023-01-12T23:35:06.970Z
2023-01-12T23:35:06.970Z
Kai
<p>In &quot;Calculational Desing of a Regular Model Checker by Abstract Interpretation&quot; (<a href="https://www.google.com/url?sa=t&amp;source=web&amp;rct=j&amp;url=https://pcousot.github.io/publications/Cousot-ICTAC-2019.pdf&amp;ved=2ahUKEwie_MXp8KP8AhXjRvEDHbEODfsQFnoECBIQAQ&amp;usg=AOvVaw17j_LVC8hajCQlDqfBVJb5" rel="nofollow noreferrer">see</a>) 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.</p>
<p>So what is structural model checking?</p>

<model-checking><formal-methods>
What is "structural model checking"?
Senmorta
# What is "structural model checking"?

(Asked by: username_0 on 2022-12-31)

In "Calculational Desing of a Regular Model Checker by Abstract Interpretation" ([see](https://www.google.com/url?sa=t&source=web&rct=j&url=https://pcousot.github.io/publications/Cousot-ICTAC-2019.pdf&ved=2ahUKEwie_MXp8KP8AhXjRvEDHbEODfsQFnoECBIQAQ&usg=AOvVaw17j_LVC8hajCQlDqfBVJb5)) 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?

**Tags:** model-checking, formal-methods

---

## 1 answers

### Answer by username_1 on 2023-01-12. Score: 2 | Accepted answer

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.

> **Comments:**
> **username_0**: Thank you very much. What do you mean by "Definition 3"? There is no "Definition 3" in the paper.  
> **username_1**: 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.  
> **username_0**: 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.  

---

