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.
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.
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..