We’re rewarding the question askers & reputations are being recalculated! Read more.

Questions tagged [model-checking]

The tag has no usage guidance.

5 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
8
votes
0answers
131 views

Practical interactive proof schemes for NP-hard problems

Model-checking (in the sense of reachability in a succinct graph) is PSPACE-complete. SAT is NP-complete. Both problems are considered intractable, yet there exist tools capable of solving them on ...
0
votes
0answers
38 views

Definition of MSO_1 for graph structures

What is the proper definition of MSO$_1$? MSO$_1$ is also called the one-sorted MSO. In contrast, in MSO$_2$, the two-sorted MSO, first order variables and set variables are allowed to be of two ...
0
votes
0answers
102 views

Approximating liveness properties with safety properties

Given a finite alphabet set $\Sigma$, the set $\Sigma^{\omega}$ of infinite words over $\Sigma$ can be topologized with a metric $d: \Sigma^{\omega} \rightarrow \mathbb{R}$ such as: $\forall w_1, w_2 ...
0
votes
0answers
95 views

Hoare program correctness

Which is the easiest way to find a valid Invariant for a While Program in the Hoare program correctness verification? Is there a "guided" way to do that?
0
votes
0answers
133 views

Given a CSL formula, how can we generate an automaton that accepts the formula?

The problem is same as the title, given a Continous Stochastic Logic(CSL) formula how can we create a machine which accepts the formula? Any intuitive ideas or references will be appreciated.