20.3. Feladat kiterjesztése

Legyen az altere, az állapottér és paramétertér felett definiált feladat. Az térre vett kiterjesztése az az feladat, amely a kiegészítő altér változóira nem tesz kikötéseket és az altérre vett vetülete megegyezik -gyel.

Ha szerepel az feladat egy specifikációs feltételében, akkor a kiterjesztett feladat megfelelő specifikációs feltételében egy olyan logikai függvény szerepel, amelynek -re vett vetülete és nem függ a kiegészítő altér változóitól.

20.2. Definíció (Logikai függvény kiterjesztése).

Jelöljük -vel a altéren definiált logikai függvény teljes térre való kiterjesztését. igazsághalmaza az a legbővebb halmaz, amelynek vetülete igazsághalmaza.

20.3. Definíció (Feladat kiterjesztése).

Legyen az altere, az állapottér és paramétertér, az tér és a paramétertér felett definiált feladat. -t az kiterjesztésének nevezzük, ha és specifikációs feltételeiben előforduló logikai függvények az specifikációs feltételeiben adott logikai függvények kiterjesztéseiA . def. a szekvenciális modell [[???Fót 83, ???Fót 88]] kiterjesztési definíciójának általánosítása..