Questions tagged [model-checking]

Model checking refers to the following problem: given a model of a system, test automatically whether this model meets a given specification.

Filter by
Sorted by
Tagged with
4 votes
1 answer
152 views

Is model checking PSpace-hard *in formula size*?

Sistla/Clarke proved [SC82] that the LTL model-checking problem is PSpace-complete. Sometimes people write that this problem is "PSpace-hard in $|\phi|$" (e.g. [LP85]). What does this mean formally? ...
Ayrat's user avatar
  • 1,065
2 votes
0 answers
343 views

Equivalence preserving operator from CTL* to LTL

The question is about an operator that transforms any CTL* formula ${\psi}$ into a (not necessarily equivalent) LTL formula ${A\psi^d}$, where $d$ means syntactically removing all $A,E$ quantifiers ...
tender hopper's user avatar
2 votes
1 answer
612 views

Transition systems that satisfy LTL but not CTL, and vice versa

I am learning about temporal logic and model checking systems. One conceptual exercise that I am struggling with is how to create a transition system which satisfies only one of two given properties, ...
KJ50's user avatar
  • 131
1 vote
2 answers
114 views

How to prove a side effect in a function

I asked a question earlier about Saving to the Database, which was very general and about the requirements for a proof when you go through many layers of non-verified systems such as the network and ...
Lance's user avatar
  • 2,223
1 vote
0 answers
64 views

How to Construct Kripke Structure States from Nested Functions

Say I have these defined functions: ...
Lance's user avatar
  • 2,223
1 vote
1 answer
105 views

Initializing non-deterministic variables in QBF

I'm trying to translate the following pseudocode to QBF. The integers are encoded as simple fixed-width bitvectors, and the entire procedure runs in polynomial space ensuring QBF has enough ...
user avatar