Incompleteness of States w.r.t. Traces in Model Checking

Details Incompleteness of States w.r.t. Traces in Model Checking Incompleteness of States w.r.t. Traces in Model Checking

2004-04-23

arxiv.org/abs/cs/0404048v2

Computer Science

Logic in Computer Science

Scientific paper

Cousot and Cousot introduced and studied a general past/future-time specification language, called mu*-calculus, featuring a natural time-symmetric trace-based semantics. The standard state-based semantics of the mu*-calculus is an abstract interpretation of its trace-based semantics, which turns out to be incomplete (i.e., trace-incomplete), even for finite systems. As a consequence, standard state-based model checking of the mu*-calculus is incomplete w.r.t. trace-based model checking. This paper shows that any refinement or abstraction of the domain of sets of states induces a corresponding semantics which is still trace-incomplete for any propositional fragment of the mu*-calculus. This derives from a number of results, one for each incomplete logical/temporal connective of the mu*-calculus, that characterize the structure of models, i.e. transition systems, whose corresponding state-based semantics of the mu*-calculus is trace-complete.

Affiliated with

Also associated with

No associations

Rating

Incompleteness of States w.r.t. Traces in Model Checking does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Incompleteness of States w.r.t. Traces in Model Checking, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Incompleteness of States w.r.t. Traces in Model Checking will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-1538