Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

1.1k questions

1.2k answers


543 users

0 votes

In global model checking, if we come across AG(all states), the condition is considered satisfied.
Is this always true or only true when there are no dead-end states in the given structure?

in * TF "Emb. Sys. and Rob." by (410 points)

1 Answer

0 votes
You are wondering about the formula AG true, which holds in all states, including the deadend states (since those satisfy every A-formula). AG true can also be expressed in ยต-calculus as nu x.[]x which can also be easily seen to be true, since []true is true and therefore the fixpoint is found after one iteration step.
by (166k points)

Related questions

Imprint | Privacy Policy