# Tag Info

Accepted

• 16.2k
Accepted

### What's the definition of ACTL?

ACTL is the universal fragment of CTL. Thus, existential path quantification is not allowed. So a path formula is of the form $AF\psi$, $AG\psi$, or $AX\psi$ (or a conjunction or disjunction of path ...
• 16.2k
Accepted

### The importance of the language semantics for code generation and frameworks for code generation in model-driven development

In general when we talk about code generation (or model-to-model transformation in general), clearly defined semantics is quite important, since such transformations usually make sense when both the ...
• 540
Accepted

• 80.4k

### An algorithm to compute a set of states that satisfy a specific CTL formula

The set of states satisfying $\exists a U b$ is the smallest set $S$ such that $S$ contains all states satisfying $b$, and $S$ contains all states satisfying $a$ which have a successor in $S$ Note ...
• 2,148
Accepted

• 9,219