Partial order reduction
કોમ્પ્યુટર વિજ્ઞાનમાં, આંશિક ક્રમમાં ઘટાડો એ મોડેલ ચેકિંગ અથવા સ્વચાલિત આયોજન અને સમયપત્રક અલ્ગોરિધમ દ્વારા શોધવામાં આવતી રાજ્ય-જગ્યાના કદને ઘટાડવા માટેની એક તકનીક છે. તે એક સાથે ચલાવવામાં આવતા સંક્રમણોની પરિવર્તનશીલતાનો ઉપયોગ કરે છે જે વિવિધ ક્રમમાં ચલાવવામાં આવે ત્યારે સમાન સ્થિતિમાં પરિણમે છે. સ્પષ્ટ સ્થિતિ અવકાશ સંશોધનમાં, આંશિક ક્રમમાં ઘટાડો સામાન્ય રીતે તમામ સક્ષમ સંક્રમણોના પ્રતિનિધિ ઉપગણને વિસ્તૃત કરવાની ચોક્કસ તકનીકનો સંદર્ભ આપે છે. આ તકનીકને પ્રતિનિધિઓ સાથે મોડેલ ચેકિંગ તરીકે પણ વર્ણવવામાં આવી છે. પદ્ધતિની વિવિધ આવૃત્તિઓ છે, કહેવાતી હઠીલી સેટ પદ્ધતિ, પર્યાપ્ત સેટ પદ્ધતિ અને સતત સેટ પદ્ધતિ. એમ્પલ સેટ એ પ્રતિનિધિઓ સાથે મોડેલ ચકાસણીનું ઉદાહરણ છે. તેમની રચના નિર્ભરતાની એક અલગ કલ્પના પર આધારિત છે. બે સંક્રમણોને ત્યારે જ સ્વતંત્ર ગણવામાં આવે છે જ્યારે તેઓ પરસ્પર સક્ષમ હોય ત્યારે બીજાને નિષ્ક્રિય કરી શકતા નથી. જે ક્રમમાં તેમને ચલાવવામાં આવે છે તેને ધ્યાનમાં લીધા વિના બંને પરિણામોનો અમલ એક અનન્ય સ્થિતિમાં થાય છે. જે સંક્રમણો સ્વતંત્ર નથી, તે નિર્ભર છે. વ્યવહારમાં સ્થિર વિશ્લેષણનો ઉપયોગ કરીને નિર્ભરતાનો અંદાજ લગાવવામાં આવે છે. આપેલ સ્થિતિમાં સંક્રમણોનો સમૂહ ક્યારે "પર્યાપ્ત" હોય તેની શરતો આપીને વિવિધ હેતુઓ માટે વિશાળ સમૂહોને વ્યાખ્યાયિત કરી શકાય છે. C0 C1 જો સંક્રમણ કેટલાક સંક્રમણ સંબંધ પર આધાર રાખે છે, તો આ સંક્રમણને ત્યાં સુધી લાગુ કરી શકાતું નથી જ્યાં સુધી પર્યાપ્ત સમૂહમાં કેટલાક સંક્રમણ અમલમાં ન આવે. C0 અને C1 શરતો રાજ્યની જગ્યામાં તમામ ડેડલોક જાળવવા માટે પૂરતી છે. વધુ સૂક્ષ્મ ગુણધર્મોને જાળવવા માટે વધુ પ્રતિબંધોની જરૂર છે. દાખલા તરીકે, રેખીય લૌકિક તર્કના ગુણધર્મોને જાળવી રાખવા માટે, નીચેની બે શરતો જરૂરી છેઃ C2 જો, પર્યાપ્ત સમૂહમાં દરેક સંક્રમણ અદ્રશ્ય હોય. C3 A ચક્રને મંજૂરી નથી જો તેમાં એવી સ્થિતિ હોય જેમાં કેટલાક સંક્રમણ સક્ષમ હોય, પરંતુ ચક્ર પરની કોઈપણ સ્થિતિઓ માટે તે ક્યારેય પર્યાપ્ત (ઓ) માં શામેલ નથી. આ શરતો પૂરતા સમૂહ માટે પૂરતી છે, પરંતુ જરૂરી શરતો માટે નહીં. હઠીલા સેટ હઠીલા સેટ સ્પષ્ટ સ્વતંત્રતા સંબંધનો કોઈ ઉપયોગ કરતા નથી. તેના બદલે તેઓ માત્ર ક્રિયાઓના ક્રમ પર પરિવર્તનશીલતા દ્વારા વ્યાખ્યાયિત કરવામાં આવે છે. એક સમૂહ s પર (નબળો) હઠીલો હોય છે, જો નીચેની પકડ હોય. D0, જો ક્રમનો અમલ શક્ય છે અને સ્થિતિ તરફ દોરી જાય છે, તો ક્રમનો અમલ શક્ય છે અને તે સ્થિતિ તરફ દોરી જશે. D1 કાં તો ડેડલોક છે, અથવા એવું કે, તેનો અમલ શક્ય છે. આ શરતો તમામ ડેડલોક જાળવવા માટે પૂરતી છે, જેમ કે C0 અને C1 પર્યાપ્ત સેટ પદ્ધતિમાં છે. જો કે, તેઓ કંઈક અંશે નબળા છે, અને જેમ કે નાના સમૂહો તરફ દોરી શકે છે. C2 અને C3 શરતો પણ પર્યાપ્ત સેટ પદ્ધતિમાં છે તેનાથી વધુ નબળી પડી શકે છે, પરંતુ હઠીલી સેટ પદ્ધતિ C2 અને C3 સાથે સુસંગત છે. અન્ય આંશિક ક્રમમાં ઘટાડા માટે અન્ય સંકેતો પણ છે. સામાન્ય રીતે ઉપયોગમાં લેવાતા અલ્ગોરિધમ્સમાંથી એક છે પર્સ્ટિસિયન્ટ સેટ/સ્લીપ સેટ અલ્ગોરિધમ. પેટ્રીસ ગોડફ્રોઇડના થીસીસમાં વિગતવાર માહિતી મળી શકે છે. પ્રતિકાત્મક મોડેલ ચકાસણીમાં, વધુ અવરોધો (રક્ષકની મજબૂતાઈ) ઉમેરીને આંશિક ક્રમમાં ઘટાડો પ્રાપ્ત કરી શકાય છે. આંશિક ક્રમમાં ઘટાડાના વધુ ઉપયોગોમાં સ્વચાલિત આયોજનનો સમાવેશ થાય છે. ટાંકણો સંદર્ભો નમૂના ચકાસણી