Incompleteness of States with Respect to Traces in Model Checking of /archleftdownµ⋆-Calculus

Title: Incompleteness of States with Respect to Traces in Model Checking of /archleftdownµ⋆-Calculus

Research Question: Can the standard state-based model checking of the /archleftdownµ⋆-calculus be complete with respect to trace-based model checking?

Methodology: The researchers investigated the /archleftdownµ⋆-calculus, a general past/future-time specification language with a natural time-symmetric trace-based semantics. They studied the standard state-based semantics, which is an abstract interpretation of the trace-based semantics.

Results: The researchers found that the standard state-based model checking of the /archleftdownµ⋆-calculus is incomplete with respect to trace-based model checking. They provided a number of results characterizing the structure of models whose corresponding state-based semantics are trace-complete.

Implications: This research has implications for the field of model checking, as it highlights a limitation of the standard state-based approach. It suggests that more research is needed to develop complete model checking techniques that can handle the /archleftdownµ⋆-calculus and other similar languages. The results also contribute to the ongoing debate about the relationship between linear and branching time languages in automatic verification.

Link to Article: https://arxiv.org/abs/0404048v2 Authors: arXiv ID: 0404048v2